Bitvector to Integer Translation

Bitvector to Integer translation

Motivation

Our analysis is more efficient on integers but most programming languages use a bitvector-based semantics. In many cases we can get the integer performance and the bitvector precision if we represent bitvectors as integers and use the integer representation whenever possible.

• We translate 01001 to 9
• We translate x + 1 to (x + 1) % 4294967296 if x is a 32-bit integer variable
• We translate bitshift operations by multiplication resp. division
• We translate bitwise and x & y to function that may return any value and is marked as an overapproximation. Whenever such a marked operation occurs in a counterexample, we redo the analysis using the bitprecise semantics.

In this project we will develop more of these several translations (e.g., use division and modulo to extract certain bits) and evaluate their performance

Introductory Material

Boogie

• Boogie specification This is Boogie 2
• Microsoft's tool for Boogie verificationBoogie @ rise4fun
• A Boogie interpreter Boogaloo
• Verification of safety properties in Ultimate
• Termination analysis in Ultimate (link currently not working, problem with umlauts)
• Synthesis of ranking functions and nontermination arguments in Ultimate

Task 1: Get familiar with Boogie

Exercises

1. Write some (small) Boogie program that is correct.
2. Write some (small) Boogie program that not correct.
3. Write some (small) Boogie program where Ultimate is unable to decide correctness.
4. Write some (small) Boogie program that is nonterminating.
5. Write some (small) Boogie program that is terminating.

SMT-LIB

• SMT at Wikipedia
• SMT-LIB Website
• Webinterface of the Z3 SMT solver

Task 2: Get familiar with SMT-LIB

Exercises

1. Write an SMT script that demonstrates that the formula x * x <= 5 /\ x > 1 is satisfiable. The Sort of the variable x should be Int.
2. What is a satisfiable assignment for x.
3. Add another conjunct such that the formula becomes unsatisfiable.

Task ???: Formulas that define relations

Internally Ultimate does not use program statements (like assignment, assume, havoc..) instead we translate all statements into relations that are represented by SMT formulas over primed and unprimed variables.

(TODO find literature - maybe could be understood without)

Example: Assume a program has variables x, y, z, then x := x + 1 would be translated into the formula x'=x+1 /\ y'=y /\ z'=z

• Translate some of the statements from Sequence below to formulas.
• We can use relations/formulas to represent sequences of statements. Let us assume that formula φ1(x,x') represents statement st1 and that formula φ2(x,x') represents statement st2. How can we combine both formulas in order to obtain a formula that represents the sequence st1;st2. (Hint: quantifier and substitution)
• Find a formula over primed and unprimed variables that does not represent any single statement but only a sequence of statements.

z:= 1; assume x>=7; x := x+1; assume y >= x; havoc x; assume (y < 8 || z >= 5);