Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002278Frama-CPlug-in > wppublic2017-02-06 13:092017-02-06 13:28
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformSilicon-20161101OSUbuntu 16.04.1 LTSOS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002278: problem with Qed's simplification power
DescriptionRunning "frama-c -wp -wp-out wp-out shift.c" on the attached file and inspecting the file "wp-out/typed/foo_post_Alt-Ergo.mlw" shows that lemma "ShiftAssociative" is simplified to "true" (see line 360) by Qed. (The postcondition of foo doesn't matter here, except that it is intentionally unprovable in order to demonstrate the lemma's simplification.)

This situation doesn't change even when all options to disable Qed functionality (i.e. "-wp-no-bits -wp-no-clean -wp-no-core -wp-no-filter -wp-no-init-summarize-array -wp-no-let -wp-no-pruning -wp-no-simpl -wp-no-simplify-forall -wp-no-simplify-is-cint -wp-no-simplify-type") are given. (In contrast, in the somewhat related issue 0001751, providing option "-wp-no-bits" is sufficient to circumvent the problem.)

While Qed's simplification capabilities are appreciated in general, the disappearance of the lemma can be a problem:
* In many Coq proofs related to C address computation, a similar lemma has to be stated and proven again and again. There seems to be no easy way to make Coq see what is considered trivial by Qed.
* Considering the discussion at https://github.com/OCamlPro/alt-ergo/issues/19, [^] if I understood the Alt-Ergo people right, Alt-Ergo isn't complete on linear arithmetic with arrays (except for quantifier-free formulas). Therefore it sometimes needs trivial lemmas. In the particular example, to make Alt-Ergo prove the goal "reverse", a kind of associtivity property (axiom "arith") is needed that Qed would simplify also to "true", and even Alt-Ergo would.

Generally speaking, Qed should be (configurable such that it is) no stronger than any of the external provers, such as Coq and Alt-Ergo. This would enable the user to provide appropriate prover hints that are not simplified away by Qed. Maybe a command line option to completely switch off Qed is sufficient. As an alternative, a command-line switch could reduce the capabilities of Qed when applied to lemmas, assuming that the user is responsible to give them in an optimal form.
TagsNo tags attached.
Attached Filesc file icon shift.c [^] (157 bytes) 2017-02-06 13:09 [Show Content]
? file icon foo_post_Alt-Ergo.mlw [^] (22,728 bytes) 2017-02-06 13:09

- Relationships

-  Notes
(0006355)
correnson (manager)
2017-02-06 13:27
edited on: 2017-02-06 13:28

This is a known problem for lemmas.

Actually, we can *not* tune Qed to not be no stronger than SMTs, because this is *precisely* where Qed comes to rescue. Typically, bitwise simplifications are beyond the scope of SMTs, but we can discharge the proofs thanks to (only) Qed. Another example is associativity (typically list-concat) or function-power (typically list-repeat) that can be handled from Qed side, but not easily from SMT one.

However, it is true that we still need to state lemmas to be used by SMTs or Coq, and those lemmas should not be simplified by Qed ! We are looking forward disabling all simplifications when *exporting* lemmas to external provers, but still use all simplifications for proving the lemmas themselves. Hence, "trivial" lemmas get proved by Qed, but are still usable by SMTs.

Before this feature is available (I can't say when), a workaround is to state SMTs lemmas by hand in side library files, and import them through WP-drivers. Typically, have a look at `$(frama-c -print-share-path)/wp/wp.driver` to see how additional library files are imported by WP itself. Drivers are documented in the WP manual, but do not hesitate to require help if needed.


- Issue History
Date Modified Username Field Change
2017-02-06 13:09 Jochen New Issue
2017-02-06 13:09 Jochen Status new => assigned
2017-02-06 13:09 Jochen Assigned To => correnson
2017-02-06 13:09 Jochen File Added: shift.c
2017-02-06 13:09 Jochen File Added: foo_post_Alt-Ergo.mlw
2017-02-06 13:27 correnson Note Added: 0006355
2017-02-06 13:27 correnson Note Added: 0006356
2017-02-06 13:27 correnson Status assigned => acknowledged
2017-02-06 13:27 correnson Note Deleted: 0006356
2017-02-06 13:28 correnson Note Edited: 0006355 View Revisions


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker