Notes 

(0006492)

Jochen

20171218 12:57


The naming dependance (3) reminds me to the closed issue #2237, where ordering of goals was involved, too. Maybe both issues are related? 


(0006493)

Jochen

20171218 13:28


Trying to track down the naming dependence (3) somewhat further, I ran the above command with "wpout outA" added on the original file "foo.c", and with "wpout outD" on a modification of "foo.c" where "AInit" was renamed to "DInit". Then I renamed the files in "outD/typed" appropriately (e.g. "lemma_DInit.ergo" to "lemma_AInit.ergo"), and ran "diff r outA outD >diff.txt" (attached).
It appears to me the only difference is in file "Axiomatic.why" where the order is "Q_TL_Acc, Q_AInit, Q_Check" in outA/, but "Q_Check, Q_TL_Acc, Q_DInit" in outD/. 



Yes I think the order / dependency problem is harmful here... Thanks for the inputs, it would help to fix the entire problem. 


(0006498)

Jochen

20171218 16:55


I managed to intercept the input given to eprover, and to boil it down to the version in "eprover.input" (attached).
The call "eprover s R xAuto tAuto cpulimit=10 tstpin eprover.input" (options as observed from the call by why3) results in "$false" being proven. None of the axioms can be deleted without losing the provability.
A strange list of predicates is involved in the inconsistency, viz.
base from_int get included infix_ls infix_lseq infix_pl infix_pl1 is_sint32 is_uint32 l_Acc mk_addr mod offset prefix_mn prefix_mn1 separated shift to_sint32 to_uint32 truncate valid_rd valid_rw
(generated from "eprover.input"). Intersting enough, the translation of the lemma "AInit" doesn't appear in the file. It seems that this lemma is needed in the C source only to ensure inclusion of some axioms that participate in the inconsistency. 



If the return value type of Acc will be changed from "int" to "integer" then contradiction disappears. Similar bug https://bts.framac.com/view.php?id=2427
I think that maybe it is possible to extract the exact steps to contradiction with z3, because it's very hard to understand eprover output. 



> "translation of the lemma "AInit" doesn't appear in the file"
For me it seems like the definition of Acc is selfcontradictionary. Definitely Eprover tries to use different values beyond the bounds of the int type. 



The situation is slightly different from the one in 2427. In 2427, we had an axiom that compared an int (implicitly converted into integer) with a (potentially outside of the int range) integer. Here, we explicitly convert an integer into an int, which has a perfectly defined semantics in ACSL. Hence, I'd say there's no inherent contradiction as far as ACSL is concerned (the semantics of Acc might not be the one the user has in mind, but that's a different story). in particular,
/*@ lemma AOne{L}: \forall int* a, init; Acc{L}(a,1,init) == a[0] + init; */
should not be provable, and it appears not to be: in the TIP, we can unfold the definition of L_Acc twice to obtain a goal of the form x = to_sint32(x), for x a sum of two int32 (i.e. potentially outside the range of int32) while the axiomatic of the to_sint32 builtin allows this equality only if x is within bounds (axiom id_sint32 in the WP arithmetic model). 
