gleiss / rapid Goto Github PK

Generalize current implementation, which only allows Var-decls at the beginning of each function

• Generalize Parser
• Generalize semantics: Don't need to add variable-equalities, if the variable is not defined yet.

• generalize the parser to support multiple conjectures
• output one smtlib-encoding of semantics/lemmas/conjecture per conjecture

Advantages:

• It is quite natural to formulate multiple conjectures for the same program, so we want to support it.
• Currently each conjecture we want to prove requires a copy of the program, which is involved (in particular if one discovers a bug in the program and needs to fix it in each copy).

Because of its in that regard stricter interpretation of the C++ standard gcc (together with libstdc++) is currently not able to successfully build the the project. It fails, because of std::vector declarations with const values in the class Problem.

Requires #2 and #3.

Add support for const variables.

• Figure out syntax (probably const vars as default and var keyword for non-const vars)
• Implement parsing
• Implement semantics: Only add value-equalities for non-const vars

Advantages:

• Simplifies semantics
• Simplifies reasoning, removes need for a simple case of induction.

Crashes if loop is nested in other loop, forgot to quantify over enclosingIterator-vars.

Refactor assertion violations into meaningful parser feedback.
Most important in practice: Feedback if term-symbol-argument-sorts and term-subterm-sorts differ.

Refactor 20 of the old benchmarks into the Spectre format.

• Currently, we directly only support if-else.
• We expect to have many programs where we want to use if without else.
• We can also use if-else with a skip statement in the else-branch, but it is inconvenient to do so.

Would be nice to have a command line option to only generate the program semantics and the property as lemmas are not used for trace properties atm.

Adopt the trace lemmas from QuIt to the new Spectre setting: We have a new syntax, but more crucially we support a much more expressive language, with multiple locations and nested program statements.

Should return a copy of the formula, with label as label.

Main goal:

• Allow to write smart-contract-like programs with function calls.