2021-03-03 03:19 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002329Frama-CPlug-in > wppublic2017-10-09 17:152019-10-17 18:02
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionno change required 
PlatformPhosphorus-20170501OSOS Versionxubuntu 17.04
Product VersionFrama-C 15-Phosphorus 
Target VersionFixed in Version 
Summary0002329: suggest unique term normalization for lemmas and goals
DescriptionRunning "frama-c -wp -wp-prop g aaa.c" on the attached file fails to prove the assertion "g", although it obviously follows from "f" by applying lemma "lem". One reason for that is of course the inherent incompleteness of SMT provers like Alt-Ergo and Cvc4. However, another reason is that Frama-C's term normalization(1) swaps some arguments of "+", and
(2) performs swaps in the lemma that differ from those performed in the goal.

As a result, in the attached mlw file,
        "(L_Foo(a,b+c)=true) -> (L_Bar(a,c+d)=true)"
appears in the lemma, while "(L_Foo(a,i_1+i_2)=true) -> (L_Bar(a,i+i_1)=true)" appears in the goal. The latter is equivalent to
        "(L_Foo(a,c+b)=true) -> (L_Bar(a,d+c)=true)"
when expressed in a notation closer to the source-code. Variable "c" is common to L_Foo and L_Bar; note its different positions in the lemma vs. in the goal.

If the goal is changed to "(L_Foo(a,i_2+i_1)=true) -> (L_Bar(a,i_1+i)=true)", it syntactically matches the lemma, and Alt-Ergo proves it in a few milliseconds.

Unless there are good reasons to swap the arguments of "+", they should be kept in their source-code order; this way, the user has a chance to control what is given to the provers.

However, if there *are* good reasons to include argument swapping in term normalization, it should be performed in the same way both in lemmas and in goals.

A possible explanation for the above behavior of Frama-C is that, for some
reason, source-code variable names are transformed to unrelated internal names
in goals, but not in lemmas, and that term normalization just orders arguments
of commutative functions lexicographically (cf. issue 0002100).
TagsNo tags attached.
Attached Files
  • c file icon aaa.c (378 bytes) 2017-10-09 17:15 - 
    /*@ axiomatic ax {
	logic boolean Bar{K,L}(int* a, integer l);
	logic boolean Foo{K,L}(int *a, integer l);
} */

/*@ lemma lem{K,L}: \forall int *a, int b, c, d;
	Foo{K,L}(a, c+b) ==> 
	Bar{K,L}(a, c+d);
*/


extern int *a, b, c, d;

void main(void)
{
	//@ ghost K:           
	changeState();
	//@ ghost L:

	//@ assert f: Foo{K,L}(a, c+b);
	//@ assert g: Bar{K,L}(a, c+d);
}
    c file icon aaa.c (378 bytes) 2017-10-09 17:15 +
  • ? file icon main_assert_g_Alt-Ergo.mlw (32,115 bytes) 2017-10-09 17:17

-Relationships
+Relationships

-Notes

~0006467

Jochen (reporter)

2017-10-12 10:21

 On second thought, I guess argument reordering is done as part of Qed simplification, and it *does* make sense: goals like "p(a+b) ==> p(b+a)" can be proven already by Qed, thanks to reordering.

~0006910

correnson (manager)

2019-10-17 17:32

 Yes indeed, it is difficult to not simplify Qed terms in lemma.
+Notes

-Issue History
Date Modified Username Field Change
2017-10-09 17:15 Jochen New Issue
2017-10-09 17:15 Jochen Status new => assigned
2017-10-09 17:15 Jochen Assigned To => correnson
2017-10-09 17:15 Jochen File Added: aaa.c
2017-10-09 17:17 Jochen File Added: main_assert_g_Alt-Ergo.mlw
2017-10-12 10:21 Jochen Note Added: 0006467
2019-10-17 17:32 correnson Status assigned => resolved
2019-10-17 17:32 correnson Resolution open => no change required
2019-10-17 17:32 correnson Note Added: 0006910
2019-10-17 18:02 signoles Status resolved => closed
+Issue History