Homework 05
Due 15 March, midnight
Your next task is to implement a simple analysis using the Abstract Interpretation framework, where the domain is a conjunction of predicates, one conjunction for each program point. For background, see in particular Exercise 06.
You will find some examples of how to do this in the directories lattice/ and ai/ in the archive below. Notably, have a look at the sign analysis example.
For predicate abstraction, you need to create a lattice whose elements are sets of predicates (formulas on the programs variables). This lattice should be used to abstract the set of reachable states at each program point by a set of predicates. (Note that this is different from the abstract reachability tree approach.)
The predicates to use should be provided in the program text using the @predicates(P1, P2, …) annotation. This annotation should apply to the definition of the function that you are analysing. See example2.scala for an example. The provided predicates are available in the “predicates” member of class CFG.
It is meant that the concretisation function maps a set of predicates to the largest set of program states satisfying the conjunction of the predicates in the set. The abstraction function maps a set of program states to the largest set of predicates whose members are true for all the states in the set of states.
In the directory ai/ you will find the file PredicateAbstraction.scala.
- Complete the PredLattice class. You should use the Princess theorem prover to define the join and meet, which should be sound with respect to the concretisation and abstraction functions as defined above.
- You then need to define the transfer function. You should also use Princess to do this.
- Once the lattice and the transfer function are defined you can instantiate your analysis using the provided AnalysisAlgorithm class (in ai/AI.scala).
- Running the analysis will give you a set of predicates for each program point. Your last task is to check using those predicates that all the asserts in the program are satisfied.
Please find a new version of the project's code in the archive below. Note that you need to populate the lib/ directory with the libs from last time.