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 Boogie

Exercises

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