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 { final ForgeProgram program; final InstanceDomain list; final GlobalVariable next, elem; final LocalVariable lst, val, ret; final ForgeProcedure contains; /** * Construct the program, domains, global variables, and local variables * are used by both procedures. */ ListFIR() { program = new ForgeProgram(); list = program.newInstanceDomain("List"); next = program.newGlobalVariable("next", list.product(list)); elem = program.newGlobalVariable("elem", list.product(program.integerDomain())); lst = program.newLocalVariable("lst", list); val = program.newLocalVariable("val", program.integerDomain()); ret = program.newLocalVariable("return", program.booleanDomain()); contains = program.newProcedure("contains", lst.and(val), ret); } /** * Construct the contains implementation with the loop. */ ForgeCFG containsLooping() { // create a new cfg for the looping implementation ForgeCFG.Impl cfg = ForgeCFG.implementation(contains); // 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 = cfg.newBranch(lst.no()); AssignStmt notFound = cfg.newAssign(ret, program.falseLiteral()); BranchStmt checkElem = cfg.newBranch(lst.join(elem).eq(val)); AssignStmt foundElem = cfg.newAssign(ret, program.trueLiteral()); AssignStmt nextList = cfg.newAssign(lst, lst.join(next)); // 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 cfg.setEntry(isEmpty); isEmpty.setThen(notFound); isEmpty.setElse(checkElem); checkElem.setThen(foundElem); checkElem.setElse(nextList); nextList.setNext(isEmpty); return cfg; } /** * Construct the contains implementation with the recursive call. */ ForgeCFG containsRecursive() { // create a new cfg for the recursive implementation ForgeCFG.Impl cfg = ForgeCFG.implementation(contains); BranchStmt isEmpty = cfg.newBranch(lst.no()); AssignStmt notFound = cfg.newAssign(ret, program.falseLiteral()); BranchStmt checkElem = cfg.newBranch(lst.join(elem).eq(val)); AssignStmt foundElem = cfg.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<ForgeExpression> inArgs = Arrays.asList(lst.join(next), val); List<ForgeVariable> outArgs = Arrays.<ForgeVariable>asList(ret); CallStmt callContains = cfg.newCall(cfg, inArgs, outArgs); cfg.setEntry(isEmpty); isEmpty.setThen(notFound); isEmpty.setElse(checkElem); checkElem.setThen(foundElem); checkElem.setElse(callContains); return cfg; } } |
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 final int LIST_SIZE = 5; private static final int BIT_WIDTH = 4; private static final int NUM_UNROLLS = 4; private static final Set<GlobalVariable> NO_GLOBALS = Collections.emptySet(); private static ForgeCFG.Spec checkSpec, runSpec; private static ForgeBounds bounds; private static SolveOptions options; /** * Constructs the FIR and checks both of the contains procedures for * any counterexamples within the bounds described above. */ public static void main(String[] args) { ListFIR fir = new ListFIR(); // 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.list); ForgeExpression validFields = l.join(fir.next).lone().and(l.join(fir.elem).one()).forAll(l); ForgeExpression preCond = 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.next.closure()).union(fir.lst); ForgeExpression postCond = fir.ret.eq(fir.val.in(reachable.join(fir.elem))); // make the check and run specifications checkSpec = ForgeCFG.specification(fir.contains, NO_GLOBALS, preCond.implies(postCond)); runSpec = ForgeCFG.specification(fir.contains, NO_GLOBALS, preCond); // make the bounds on the analysis Map<InstanceDomain, Integer> domBounds = Collections.singletonMap(fir.list, LIST_SIZE); bounds = new ForgeBounds(fir.program, BIT_WIDTH, domBounds); // make the solve options SolveOptions.Builder optionsBuilder = new SolveOptions.Builder(NUM_UNROLLS); // uncomment to use minisat and get coverage analysis if you have binaries //optionsBuilder.satSolver(SatSolver.MINISAT).coverage(true); options = optionsBuilder.build(); // now test each implementation testCode(fir.containsLooping()); System.out.println(); testCode(fir.containsRecursive()); } private static void testCode(ForgeCFG code) { ForgeSolver solver = new ForgeSolver(code, options); System.out.println("===== TESTING THE FOLLOWING CODE ====="); System.out.print(code); // check the code System.out.println("===== CHECKING THE FOLLOWING SPEC ====="); System.out.print(checkSpec); long checkStart = System.currentTimeMillis(); ForgeSolution checkSol = solver.check(checkSpec, bounds); long checkDuration = System.currentTimeMillis() - checkStart; reportSolution(checkSol, checkDuration); // run the code System.out.println("===== RUNNING AGAINST THE FOLLOWING SPEC ====="); System.out.print(runSpec); long runStart = System.currentTimeMillis(); ForgeSolution runSol = solver.run(runSpec, bounds); long runDuration = System.currentTimeMillis() - runStart; reportSolution(runSol, runDuration); System.out.println("===== TEST COMPLETED ====="); } private static void reportSolution(ForgeSolution sol, long duration) { long seconds = (long)(duration / 1000.0); System.out.println("analysis completed in " + seconds + " seconds"); // print results if (sol.satisfiable()) { System.out.println("trace found"); System.out.print(sol.trace()); } else { Coverage coverage = sol.coverage(); if (coverage == null) { System.out.println("no trace found"); } else { System.out.println("no trace found and coverage determined"); System.out.println(sol.coverage()); } } System.out.println(); } } |
