Skip to content

Commit

Permalink
towards proof obligations for functions
Browse files Browse the repository at this point in the history
  • Loading branch information
mattulbrich committed Aug 27, 2018
1 parent 224e5e0 commit a8e6dd6
Show file tree
Hide file tree
Showing 11 changed files with 181 additions and 29 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
import edu.kit.iti.algover.proof.PVCCollection;
import edu.kit.iti.algover.proof.PVCGroup;
import edu.kit.iti.algover.proof.SinglePVC;
import edu.kit.iti.algover.symbex.FunctionObligationMaker;
import edu.kit.iti.algover.symbex.Symbex;
import edu.kit.iti.algover.symbex.SymbexPath;
import edu.kit.iti.algover.term.builder.TermBuildException;
Expand Down Expand Up @@ -87,12 +88,30 @@ private void giveUniqueIdentifier(SymbexPath path, Set<String> seenNames) {
}

public PVCCollection visitFunction(DafnyFunction f) {
Set<String> seenNames = new HashSet<>();
PVCGroup mGroup = new PVCGroup(f);

// FunctionPVCProducer fop = new FunctionPVCProducer(project);
// fop.producePVCs(f);


FunctionObligationMaker obligationMaker = new FunctionObligationMaker();
List<SymbexPath> paths = obligationMaker.visit(f.getRepresentation());
for (SymbexPath path : paths) {
List<SymbexPath> subpaths = path.split();
for (SymbexPath subpath : subpaths) {
giveUniqueIdentifier(subpath, seenNames);
MethodPVCBuilder builder = new MethodPVCBuilder(project);
builder
.setPathThroughProgram(subpath)
.setDeclaration(f);
PVC pvc;
try {
pvc = builder.build();
SinglePVC sPVC = new SinglePVC(pvc);
mGroup.addChild(sPVC);
} catch (TermBuildException e) {
// FIXME. ... need a concept ofr exception handling here
e.printStackTrace();
}
}
}
return mGroup;
}

Expand Down
4 changes: 2 additions & 2 deletions modules/core/src/edu/kit/iti/algover/parser/Dafny.g
Original file line number Diff line number Diff line change
Expand Up @@ -210,13 +210,13 @@ method:
;

function:
'function'
'function' 'method'?
ID '(' vars? ')' ':' type
( requires | ensures | decreases )*
'{' expression '}'
->
^(FUNCTION ID ^(ARGS vars?) ^(RETURNS type) requires* ensures* decreases*
^(BLOCK expression?))
expression)
;

field:
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ public class MethodPVCBuilder implements PVCBuilder {
/**
* DafnyMethod to which this PVC belongs
*/
private DafnyMethod declaration;
private DafnyDecl declaration;

private SymbolTable symbolTable;

Expand Down Expand Up @@ -103,7 +103,7 @@ public DafnyDecl getDeclaration() {
return declaration;
}

public MethodPVCBuilder setDeclaration(DafnyMethod decl) {
public MethodPVCBuilder setDeclaration(DafnyDecl decl) {
this.sequent = null;
this.declaration = decl;
return this;
Expand All @@ -120,7 +120,7 @@ private SymbolTable makeSymbolTable() {

Collection<FunctionSymbol> map = new ArrayList<>();

DafnyMethod method = declaration;
DafnyDecl method = declaration;

for (DafnyTree decl : ProgramDatabase.getAllVariableDeclarations(method.getRepresentation())) {
String name = decl.getChild(0).toString();
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
/*
* This file is part of AlgoVer.
*
* Copyright (C) 2015-2018 Karlsruhe Institute of Technology
*
*/

package edu.kit.iti.algover.symbex;

import edu.kit.iti.algover.parser.DafnyParser;
import edu.kit.iti.algover.parser.DafnyTree;
import edu.kit.iti.algover.symbex.PathConditionElement.AssumptionType;

import java.util.Deque;
import java.util.LinkedList;
import java.util.List;

public class FunctionObligationMaker {

SymbexExpressionValidator expressionValidator =
new SymbexExpressionValidator();

public List<SymbexPath> visit(DafnyTree function) {

assert function.getType() == DafnyParser.FUNCTION;

LinkedList<SymbexPath> paths = new LinkedList<>();

SymbexPath path = new SymbexPath(function);

for (DafnyTree req : function.getChildrenWithType(DafnyParser.REQUIRES)) {
path.addPathCondition(req.getLastChild(), req, AssumptionType.PRE);
}

expressionValidator.handleExpression(paths, path, function.getLastChild());

return paths;
}
}
1 change: 0 additions & 1 deletion modules/core/src/edu/kit/iti/algover/symbex/Symbex.java
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@
import edu.kit.iti.algover.util.ASTUtil;
import edu.kit.iti.algover.util.ImmutableList;
import edu.kit.iti.algover.util.Pair;
import nonnull.Nullable;

import java.util.*;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,13 @@

package edu.kit.iti.algover.symbex;

import edu.kit.iti.algover.dafnystructures.TarjansAlgorithm;
import edu.kit.iti.algover.parser.DafnyParser;
import edu.kit.iti.algover.parser.DafnyTree;
import edu.kit.iti.algover.symbex.AssertionElement.AssertionType;
import edu.kit.iti.algover.symbex.PathConditionElement.AssumptionType;
import edu.kit.iti.algover.util.ASTUtil;
import edu.kit.iti.algover.util.Pair;
import nonnull.Nullable;

import java.util.ArrayList;
Expand Down Expand Up @@ -104,8 +106,8 @@ public void handleExpression(Deque<SymbexPath> stack, SymbexPath current,
break;

case DafnyParser.CALL:
System.out.println(">> " + expression.toStringTree());

handleFunctionCall(stack, current, expression);
break;

default:
for (int i = 0; i < expression.getChildCount(); i++) {
Expand All @@ -114,6 +116,69 @@ public void handleExpression(Deque<SymbexPath> stack, SymbexPath current,
}
}

private void handleFunctionCall(Deque<SymbexPath> stack, SymbexPath state, DafnyTree expression) {
DafnyTree callee = expression.getChild(0).getDeclarationReference();
DafnyTree args = expression.getLastChild();
DafnyTree receiver = null;
if(expression.getChildCount() == 3) {
// there is a receiver
receiver = expression.getChild(1);
handleExpression(stack, state, receiver);
addNonNullCheck(stack, state, receiver);
}

for (int i = 0; i < args.getChildCount(); i++) {
handleExpression(stack, state, args.getChild(i));
}

List<Pair<String, DafnyTree>> subs = new ArrayList<>();
if (receiver != null) {
subs.add(new Pair<>("this", receiver));
}
subs.addAll(ASTUtil.methodParameterSubs(callee, args));

// ------------------
// preconditions
List<DafnyTree> preconds = callee.getChildrenWithType(DafnyParser.REQUIRES);
for (DafnyTree precond : preconds) {
SymbexPath reqState = new SymbexPath(state);
reqState.setBlockToExecute(Symbex.EMPTY_PROGRAM);
DafnyTree condition = precond.getLastChild();
// wrap that into a substitution
condition = ASTUtil.letCascade(subs, condition);
reqState.setProofObligation(condition, expression, AssertionType.CALL_PRE);
stack.add(reqState);
}

// ------------------
// variant if in recursion loop.
DafnyTree callerSCC = state.getMethod().getExpressionType();
DafnyTree calleeSCC = callee.getExpressionType();
assert callerSCC.getType() == TarjansAlgorithm.CALLGRAPH_SCC
&& calleeSCC.getType() == TarjansAlgorithm.CALLGRAPH_SCC;
if(callerSCC.getText().equals(calleeSCC.getText())) {
// both in same stron. conn. component ==> potential cycle
DafnyTree decr = callee.getFirstChildWithType(DafnyParser.DECREASES);
if(decr == null) {
decr = ASTUtil.intLiteral(0);
// TODO rather throw an exception?
} else {
decr = decr.getLastChild();
}

decr = ASTUtil.letCascade(subs, decr);
DafnyTree condition = ASTUtil.noetherLess(
ASTUtil.create(DafnyParser.LISTEX, decr),
ASTUtil.create(DafnyParser.LISTEX, ASTUtil.id("$decr")));
// wrap that into a substitution
condition = ASTUtil.letCascade(subs, condition);
SymbexPath decrState = new SymbexPath(state);
decrState.setBlockToExecute(Symbex.EMPTY_PROGRAM);
decrState.setProofObligation(condition, expression, AssertionType.VARIANT_DECREASED);
stack.add(decrState);
}
}

private void addIndexInRangeCheck(Deque<SymbexPath> stack, SymbexPath current,
DafnyTree idx, @Nullable DafnyTree array,
String arrayLengthSuffix) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -183,6 +183,7 @@ public void addDeclaredLocalVar(LocalVarDecl decl) {
*
* @return the function
*/
// TODO Rename getDeclaration()
public DafnyTree getMethod() {
return method;
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -87,4 +87,4 @@
(FUNCTION inImage
(ARGS (VAR i (TYPE int)))
(RETURNS bool)
(BLOCK true)))
true))
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,7 @@ public Void visitID(DafnyTree t, Void a) {
case DafnyParser.FIELD:
case DafnyParser.ALL:
case DafnyParser.EX:
case DafnyParser.TYPE:
case DafnyParser.LABEL:
return null;
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,15 @@

package edu.kit.iti.algover.symbex;

import edu.kit.iti.algover.dafnystructures.DafnyFunction;
import edu.kit.iti.algover.dafnystructures.DafnyMethod;
import edu.kit.iti.algover.dafnystructures.TarjansAlgorithm;
import edu.kit.iti.algover.parser.DafnyException;
import edu.kit.iti.algover.parser.DafnyParser;
import edu.kit.iti.algover.parser.DafnyParserException;
import edu.kit.iti.algover.parser.DafnyTree;
import edu.kit.iti.algover.project.Project;
import edu.kit.iti.algover.util.ASTUtil;
import edu.kit.iti.algover.util.ImmutableList;
import edu.kit.iti.algover.util.TestUtil;
import edu.kit.iti.algover.util.TreeUtil;
import junitparams.JUnitParamsRunner;
Expand All @@ -22,7 +25,6 @@
import org.junit.runner.RunWith;

import java.io.IOException;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Deque;
import java.util.LinkedList;
Expand Down Expand Up @@ -74,6 +76,11 @@ public Object[][] parametersForTestValid() {
new int[]{0, 2, 2, 0},
Arrays.asList()
},
{
"class C { var next:C; method m() ensures next.next == next {} }",
new int[]{0, 2, 2, 0},
Arrays.asList("[][RT_NONNULL:(!= next null)]")
},

// Logical shortcut operators
{
Expand Down Expand Up @@ -108,11 +115,11 @@ public Object[][] parametersForTestValid() {
"[][RT_IN_BOUNDS:(!= a 0)]")
},
{
"method m(a: int) ensures if 1/a==a then 1/a==a+1 else 1/a==2 {}",
"method m(a: int) ensures if 1/a==a then a/2==1 else a/3==1 {}",
new int[]{0, 2, 0},
Arrays.asList(
"[GUARD_IN_EXPRESSION[null]:(not (== (/ 1 a) a))][RT_IN_BOUNDS:(!= a 0)]",
"[GUARD_IN_EXPRESSION[null]:(== (/ 1 a) a)][RT_IN_BOUNDS:(!= a 0)]",
"[GUARD_IN_EXPRESSION[null]:(not (== (/ 1 a) a))][RT_IN_BOUNDS:(!= 3 0)]",
"[GUARD_IN_EXPRESSION[null]:(== (/ 1 a) a)][RT_IN_BOUNDS:(!= 2 0)]",
"[][RT_IN_BOUNDS:(!= a 0)]")
},
{
Expand All @@ -127,16 +134,29 @@ public Object[][] parametersForTestValid() {
"function f(x: int) : int requires x >= 0 decreases x\n" +
"{ if x == 0 then 0 else f(x-1)+1 } ",
new int[]{0, 2, 0},
Arrays.asList("[][PRE_CONDITION: (>= 22 0)]")
Arrays.asList("[][CALL_PRE[f]:(LET (VAR x) 22 (>= x 0))]")
},
{
"method m() ensures f(22)==2 {}\n" +
"function f(x: int) : int requires x >= 0 decreases x\n" +
"{ if x == 0 then 0 else f(x-1)+1 }",
new int[]{0, 2, 0},
Arrays.asList("[][PRE_CONDITION: (>= 22 0)]")
// with decreases.
"function base(x: int) : int requires x >= 0 decreases x\n" +
"{ if x == 0 then 0 else base(x-1)+1 } ",
new int[]{0},
Arrays.asList("[GUARD_IN_EXPRESSION[null]:(not (== x 0))][CALL_PRE[base]:(LET (VAR x) (- x 1) (>= x 0))]",
"[GUARD_IN_EXPRESSION[null]:(not (== x 0))]" +
"[VARIANT_DECREASED[base]:" +
"(LET (VAR x) (- x 1) (NOETHER_LESS (LISTEX (LET (VAR x) (- x 1) x)) (LISTEX $decr)))]")
},
{
"class C { var next:C;\n" +
" function f(x:int) : int requires x>0 {x}\n" +
" method m() ensures f(1) + this.f(2) + next.f(3) > 0 {} }",
new int[]{0, 3, 2},
Arrays.asList(
"[][CALL_PRE[f]:(LET (VAR x) 1 (> x 0))]",
"[][CALL_PRE[f]:(LET (VAR this x) this 2 (> x 0))]",
"[][CALL_PRE[f]:(LET (VAR this x) next 3 (> x 0))]",
"[][RT_NONNULL:(!= next null)]")
},

};
}

Expand All @@ -153,7 +173,15 @@ public void testValid(String code, int[] selectors, List<String> expected) throw

SymbexExpressionValidator expVal = new SymbexExpressionValidator();
Deque<SymbexPath> stack = new LinkedList<>();
SymbexPath path = new SymbexPath(ASTUtil.builtInVar("FAKE!"));
DafnyFunction baseFunction = project.getFunction("base");
DafnyTree caller;
if (baseFunction != null) {
caller = baseFunction.getRepresentation();
} else {
caller = ASTUtil.builtInVar("FAKE!");
caller.setExpressionType(ASTUtil.create(TarjansAlgorithm.CALLGRAPH_SCC, "something"));
}
SymbexPath path = new SymbexPath(caller);
expVal.handleExpression(stack, path, expression);

assertEquals(expected.size(), stack.size());
Expand All @@ -162,7 +190,7 @@ public void testValid(String code, int[] selectors, List<String> expected) throw
String actual = "" +
p.getPathConditions() +
p.getProofObligations();
assertEquals(expected.get(i++), actual);
assertTrue(actual + " not expected", expected.contains(actual));
}

}
Expand Down
4 changes: 2 additions & 2 deletions modules/core/test/edu/kit/iti/algover/symbex/SymbexTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -1057,7 +1057,7 @@ public void testObjectCreation() throws Exception {

assertEquals(0, state.getProofObligations().size());
assertEquals("[IMPLICIT_ASSUMPTION[null]:(not (CALL $isCreated (ARGS $heap $new_1))), " +
"IMPLICIT_ASSUMPTION[null]:(= (Length $new_1) 10)]",
"IMPLICIT_ASSUMPTION[null]:(== (Length $new_1) 10)]",
state.getPathConditions().toString());
assertEquals("[(ASSIGN $heap (CALL $create (ARGS $heap $new_1))), (ASSIGN c4 $new_1)]", state.getAssignmentHistory().map(x -> x.toStringTree()).toString());

Expand All @@ -1079,7 +1079,7 @@ public void testObjectCreation() throws Exception {

assertEquals(0, state.getProofObligations().size());
assertEquals("[IMPLICIT_ASSUMPTION[null]:(not (CALL $isCreated (ARGS $heap $new_1))), " +
"IMPLICIT_ASSUMPTION[null]:(= (Length $new_1) (Length c4))]",
"IMPLICIT_ASSUMPTION[null]:(== (Length $new_1) (Length c4))]",
state.getPathConditions().toString());
assertEquals("[(ASSIGN $heap (CALL $create (ARGS $heap $new_1))), (ASSIGN c5 $new_1)]", state.getAssignmentHistory().map(x -> x.toStringTree()).toString());

Expand Down

0 comments on commit a8e6dd6

Please sign in to comment.