List Example
List Example
CONSTRUCTING THE FIR PROGRAM
/**
* Constructs a FIR program consisting of a list data structure and two
* implementations of the contains method, one that contains a loop and
* the other that contains a recursive call.
*/
class ListFIR {
ForgeProgram program;
InstanceDomain listDomain;
GlobalVariable nextVar;
GlobalVariable elemVar;
LocalVariable lst;
LocalVariable val;
LocalVariable ret;
List<LocalVariable> inParams;
List<LocalVariable> outParams;
/**
* Construct the program, domains, global variables, and local variables
* are used by both procedures.
*/
ListFIR() {
program = new ForgeProgram();
listDomain = program.newInstanceDomain("List");
nextVar = program.newGlobalVariable("next", listDomain.product(listDomain));
elemVar = program.newGlobalVariable("elem", listDomain.product(program.integerDomain()));
lst = program.newLocalVariable("lst", listDomain);
val = program.newLocalVariable("val", program.integerDomain());
ret = program.newLocalVariable("ret", program.booleanDomain());
inParams = Arrays.asList(lst, val);
outParams = Arrays.asList(ret);
}
/**
* Construct the contains implementation with the loop.
*/
ForgeProcedure containsLooping() {
// create a new procedure for the looping implementation
// initially, the procedure's entry statement is its exit statement
ForgeProcedure contains = new ForgeProcedure(program, "contains", inParams, outParams);
// construct the statements in the procedure.
// initially, the exit stmt is the only each successor each stmt
// the implementation presumes the lst variable can be the empty set,
// which we will use to denote the empty list
BranchStmt isEmpty = contains.newBranch(lst.no());
AssignStmt notFound = contains.newAssign(ret, program.falseLiteral());
BranchStmt checkElem = contains.newBranch(lst.join(elemVar).eq(val));
AssignStmt foundElem = contains.newAssign(ret, program.trueLiteral());
AssignStmt nextList = contains.newAssign(lst, lst.join(nextVar));
// make the isEmpty statement the entry point of the procedure
// set the successors of the statements, the successors not set
// are left to be the exit statement of the procedure
isEmpty.setEntry();
isEmpty.setThen(notFound);
isEmpty.setElse(checkElem);
checkElem.setThen(foundElem);
checkElem.setElse(nextList);
nextList.setNext(isEmpty);
return contains;
}
/**
* Construct the contains implementation with the recursive call.
*/
ForgeProcedure containsRecursive() {
// create a new procedure for the recursive implementation
// it is ok for it to have the same name as the looping procedure,
// because program elements are equal by reference; the name is a comment
// it is ok to reuse the in- and out-params, because although they are
// declared globally, each procedure invocation has a fresh copy of them
ForgeProcedure contains = new ForgeProcedure(program, "contains", inParams, outParams);
BranchStmt isEmpty = contains.newBranch(lst.no());
AssignStmt notFound = contains.newAssign(ret, program.falseLiteral());
BranchStmt checkElem = contains.newBranch(lst.join(elemVar).eq(val));
AssignStmt foundElem = contains.newAssign(ret, program.trueLiteral());
// a call statement must include a number of in- and out-arguments
// equal to the called procedures in- and out-parameters, respectively
List |
ANALYZING THE FIR PROGRAM/** * Analyzes the FIR procedures constructed in ListFIR.java. * Loops and recursion in each analysis are unrolled for 4 iterations, * and the analysis sets the bitWidth to 4 and explores all configurations * in which the heap doesn't exceed 5 List instances. * * Running this class should yield a null trace in both cases, indicating * a failure to find any counterexamples within the provided bounds. * Now alter the code in ListFIR to make it incorrect, for example, by * assigning false to the return variable when it should assign true. * You should now get a counterexample trace that violates the specification. */ class ListAnalysis { private static ListFIR fir; private static final int LIST_SIZE = 5; private static final int BIT_WIDTH = 4; private static final int NUM_UNROLLS = 4; /** * Constructs the FIR and checks both of the contains procedures for * any counterexamples within the bounds described above. */ public static void main(String[] args) { fir = new ListFIR(); checkContains(fir.containsLooping()); checkContains(fir.containsRecursive()); } private static void checkContains(ForgeProcedure contains) { System.out.println("original procedure"); System.out.println(contains); System.out.println(); // make a constraint for valid arguments and fields // the list variable is lone (singleton element or the empty set), // and the value we are searching for must be a singleton // nextVar is constrained to be a partial function, and // elemVar is constrained to be a total function ForgeExpression validArgs = fir.lst.lone().and(fir.val.one()); LocalVariable l = fir.program.newLocalVariable("x", fir.listDomain); ForgeExpression validFields = l.join(fir.nextVar).lone().and(l.join(fir.elemVar).one()).forAll(l); ForgeExpression validVars = validArgs.and(validFields); // reachable is the set of all reachable lists from lst, including lst itself // correctReturn is the constraint that the return variable is true iff // given val is in the elem field of the reachable lists. ForgeExpression reachable = fir.lst.join(fir.nextVar.closure()).union(fir.lst); ForgeExpression correctReturn = fir.ret.eq(fir.val.in(reachable.join(fir.elemVar))); // make the specification // only the return variable that may be modified by the procedure Set<ForgeVariable> modified = Collections.<ForgeVariable>singleton(fir.ret); SpecStmt spec = contains.newSpec(validVars.implies(correctReturn), modified); // make the bounds on the analysis Map<InstanceDomain, Integer> domBounds = Collections.singletonMap(fir.listDomain, LIST_SIZE); ForgeBounds bounds = new ForgeBounds(fir.program, BIT_WIDTH, domBounds); // make the solver ForgeSolver solver = new ForgeSolver(contains, NUM_UNROLLS); System.out.println("transformed procedure"); System.out.println(solver.transformed()); System.out.println(); // find a counterexample trace long start = System.currentTimeMillis(); Trace trace = solver.check(spec, bounds); long duration = (System.currentTimeMillis() - start) / 1000; System.out.println("analyzed in " + duration + " seconds"); System.out.println(trace == null ? "no solution" : trace.toString()); System.out.println(); } } |
