Developer Documentation - Edkamb/crowbar-tool GitHub Wiki
General comments
- Always use
appendStmt
to extend the internal AST, as we match on the exact structure of the AST. - The front-end is split in three parts:
Repository.kt
collects information from the ABS AST.ABSInterface.kt
translates the ABS AST into the Crowbar IR.Main.kt
setups theRepository
and extracts all proof obligations. - The back-end is mainly in
SMTInterface.kt
, which translates formulas of the Crowbar IR into SMT-LIB. The counterexample generator is implemented in theorg.abs_models.crowbar.investigator
package. - The middle-end is mainly in the
Rule.kt
(defining rules),Match.kt
(applying one rule) andStrategy.kt
(complete symbolic execution).
Adding a new type
Adding the syntax
First, extend the DeductType
interface and implement the following four methods:
extractMethodNode(classDecl: ClassDecl, name: String, repos: Repository): SymbolicNode
must return the root of a symbolic execution tree for methodname
inclassDelc
.extractInitialNode(classDecl: ClassDecl): SymbolicNode
must return the root of a symbolic execution tree for the initial block ofclassDelc
.exctractMainNode(model: Model): SymbolicNode
must return the root of a symbolic execution tree for the initial block of the program.exctractFunctionNode(fDecl: FunctionDecl): SymbolicNode
must return the root for function declaration
The interface must have an anonymous companion object
If your type is no operating on some of these targets, say functions, return emptySymNode()
If your type is supposed to generate proof obligations at another level, add extract methods here as well and call them from the main block (see below).
Next, implement a schematic syntax and a concrete semantics. The schematic syntax is an abstract variable and is declared as
data class NewAbstractVar(val name : String) : NewType, AbstractVar{ ... }
this class is used to define schematic rules later. The concrete semantics is any implementation for the internal syntax of your specification.
Adding rules
To add rules, extend the Rule
class. The Rule
constructor takes a schematic modality on which it will match.
Matching takes a modality and unifies it with the current modality in the symbolic execution, by assigning concrete value to every instance of AbstractVar
. For example, the following will match on every modality:
class NewRule(val repos: Repository) : Rule(Modality(
SeqStmt(StmtAbstractVar("FIRST"),StmtAbstractVar("CONT")),
NewAbstractVar("TYPE"))) {....
Each rule must override the transform(cond: MatchCondition, input : SymbolicState): List<SymbolicTree>
method.
The MatchCondition
is an assignment from all AbstractVar
instances in the constructor to concrete values. input
is the current state of the symbolic execution.
You can retrieve the concrete values with, e.g.,
val type = cond.map[NewAbstractVar("TYPE")] as NewType
val first = cond.map[StmtAbstractVar("FIRST")] as Stmt
val cont = cond.map[StmtAbstractVar("CONT")] as Stmt
Beware: (1) these casts are not checked statically (2) you must use the correct type for the schematic variable. For example cond.map[NewAbstractVar("FIRST")]
will fail.
Adding the interface
To enable users to invoke your type, extend the deductType
option in Main.kt
by adding another branch "NewType" -> NewType::class
in its convert
call. To connect rules with symbolic execution (1) extend the getStrategy
function in Strategy.kt
with another branch NewType::class -> nextNewStrategy(repos)
and (2) add a new function fun nextNewStrategy(repos: Repository) : Strategy = DefaultStrategy(listOf(...))
, where ...
creates one instance of each rule you added.
Counterexample Generation
In the most abstract terms, Crowbar's counterexample generation works by reconstructing the executed program from the applied symbolic execution rules. To do so, it uses additional information stored in the NodeInfo
object stored in every node of the symbolic execution tree.
Extending CEG
To add support for new rules to the counterexample generator, create a new subtype of NodeInfo
and extend the NodeInfoVisitor
appropriately. The new NodeInfo
subclass can in principle store arbitrary information that is necessary to properly reconstruct the executed statement. The NodeInfo
class already provides the properties smtExpressions
and heapExpressions
, which can be used to pass arbitrary heap expressions and generic SMT expressions to the SMT solver to be evaluated in the counterexample model. Info objects also have to indicate if they are heap-anonymization points (like await statements) or full-anonymization points (like loops).
Info objects for leaves in the symbolic execution tree should also implement the LeafInfo
interface and provide a list of all proof obligations that have to be shown at this point.
With new info objects in place, all that remains to enable counterexample generation is to provide an implementation of the new visit
functions in the NodeInfoRenderer
. These functions render the information from the NodeInfo
objects into reconstructed program code with appropriate simplifications and modifications, using additional state information as well as the evaluated heap and SMT expressions that were 'registered' for evaluation in the NodeInfo
object. Various helper functions are provided for rendering Formulas, Expressions, Terms, Locations, etc. Please refer to the existing rendering functions in NodeInfoRenderer
for some examples.