diff --git a/README.md b/README.md index df40290..f233674 100644 --- a/README.md +++ b/README.md @@ -100,6 +100,16 @@ _invariant: TRUE } while ((r1 % 2) != 0) ``` +### Declassificaton + +To specify the declassification of a predicate it is necessary to specify both the expression being declassified and under what conditions this can happen. For example, + +``` +out = d(sum/cnt, cnt > min) +``` + +specifies that at this particular line the expression `sum/cnt` can be declassified if `cnt > min`. + ### Supported operations * `=` assignment * `==` equal to @@ -124,8 +134,22 @@ _invariant: TRUE ## TODOs ### Unsupported language features Below is an inconclusive list of unsupported language features. - * Pointers + * Dynamic thread creation + * Objects + +### Improve Type System + * Nested arrays + * Arrays/Pointers to Bools + * Arrays of pointers ### Weak memory model The logic for the weak memory model is currently not implemented +## Optimisations +### Passification + +### General Improvemens + * Implement a standard interface for identifiers and remove specific logic where possible + * Objects are implemented, but implementation appears to be incorrect. Treiber stack put does not pass + + diff --git a/tests/declassify/avg b/tests/declassify/avg new file mode 100644 index 0000000..062cf7d --- /dev/null +++ b/tests/declassify/avg @@ -0,0 +1,16 @@ +global var sum: +_L: FALSE + +global var cnt: +_L: TRUE + +global var out: +_L: TRUE + +_Gamma_0: sum -> HIGH +_Rely: TRUE +_Guar: TRUE + +if (cnt > 5) { + out = d(sum/cnt, cnt > 5); +} diff --git a/tests/declassify/if1 b/tests/declassify/if1 new file mode 100644 index 0000000..28333c9 --- /dev/null +++ b/tests/declassify/if1 @@ -0,0 +1,16 @@ +local var pass: + +local var ans: + +global var out: +_L: TRUE + +_Gamma_0: pass -> HIGH +_Rely: TRUE +_Guar: TRUE + +if (d(pass == ans, TRUE)) { + out = 1; +} else { + out = 0; +} diff --git a/tests/declassify/neg/avg1 b/tests/declassify/neg/avg1 new file mode 100644 index 0000000..a370cdb --- /dev/null +++ b/tests/declassify/neg/avg1 @@ -0,0 +1,16 @@ +global var sum: +_L: FALSE + +global var cnt: +_L: TRUE + +global var out: +_L: TRUE + +_Gamma_0: sum -> HIGH +_Rely: TRUE +_Guar: TRUE + +if (cnt > 5) { + out = sum/cnt; +} diff --git a/tests/declassify/neg/avg2 b/tests/declassify/neg/avg2 new file mode 100644 index 0000000..2cde8ff --- /dev/null +++ b/tests/declassify/neg/avg2 @@ -0,0 +1,16 @@ +global var sum: +_L: FALSE + +global var cnt: +_L: TRUE + +global var out: +_L: TRUE + +_Gamma_0: sum -> HIGH +_Rely: TRUE +_Guar: TRUE + +if (cnt >= 5) { + out = d(sum/cnt, cnt > 5); +} diff --git a/tests/declassify/neg/if1 b/tests/declassify/neg/if1 new file mode 100644 index 0000000..c104fa1 --- /dev/null +++ b/tests/declassify/neg/if1 @@ -0,0 +1,16 @@ +local var pass: + +local var ans: + +global var out: +_L: TRUE + +_Gamma_0: pass -> HIGH +_Rely: TRUE +_Guar: TRUE + +if (pass == ans) { + out = 1; +} else { + out = 0; +} diff --git a/tests/declassify/put b/tests/declassify/put new file mode 100644 index 0000000..909e0e9 --- /dev/null +++ b/tests/declassify/put @@ -0,0 +1,51 @@ +global var z: +_L: TRUE + +global var tail: +_L: TRUE + +global var head: +_L: TRUE + +global var L: +_L: TRUE + +global array tasks[1]: +_L: levels[_i] == 1 +_Rely: tasks[_i] == tasks'[_i] +_Guar: TRUE + +global array levels[1]: +_L: TRUE +_Rely: levels[_i] == levels'[_i] +_Guar: (z % 2 == 0 && z' == z) => (levels[_i] == levels'[_i]) + +local var t: + +global var task: +_L: level == 1 + +global var level: +_L: TRUE + +local var dec: + +_Gamma_0: z -> LOW, dec -> LOW +_Rely: z == z' && task == task' && level == level' && L == L' +_Guar: z' >= z + +if (z % 2 == 1) { + z = z + 1; +} + +t = tail; +z = z + 1; +if (dec == 1) { + levels[t % L] = 1; + tasks[t % L] = d(task, dec == 1); +} else { + levels[t % L] = level; + tasks[t % L] = task; +} +z = z + 1; +tail = t + 1; diff --git a/tests/rg/TODO b/tests/rg/_TODO similarity index 100% rename from tests/rg/TODO rename to tests/rg/_TODO diff --git a/tests/rg/caslev/steal_0 b/tests/rg/caslev/steal_ similarity index 90% rename from tests/rg/caslev/steal_0 rename to tests/rg/caslev/steal_ index 718d343..95a6a01 100644 --- a/tests/rg/caslev/steal_0 +++ b/tests/rg/caslev/steal_ @@ -23,7 +23,6 @@ _Guar: levels[_i] == levels'[_i] local var t: local var h: local var r: -local var index: local var level: local var task: @@ -47,10 +46,9 @@ if (h < t) { r = z; } while (r % 2 == 1) - index = h % L; - level = levels[index]; + level = levels[h % L]; if (level == 1) { - task = tasks[index]; + task = tasks[h % L]; } else { task = -1; // fail } diff --git a/tests/rg/caslev/steal_old b/tests/rg/caslev/steal_old deleted file mode 100644 index 95be0d4..0000000 --- a/tests/rg/caslev/steal_old +++ /dev/null @@ -1,70 +0,0 @@ -global var z: -_L: TRUE - -global var tail: -_L: TRUE - -global var head: -_L: TRUE - -global var L: -_L: TRUE - -global array tasks[1]: -_L: levels[_i] == 1 -_Rely: TRUE -_Guar: tasks[_i] == tasks'[_i] - -global array levels[1]: -_L: TRUE -_Rely: (z % 2 == 0 && z' == z) => (levels[_i] == levels'[_i]) -_Guar: levels[_i] == levels'[_i] - -local var t: -local var h: -local var r: -local var level: -local var task: -local var index: - - -global var ret: -_L: TRUE - -_Gamma_0: z -> LOW, r -> LOW -_Rely: z' >= z // && 0 <= h && h <= 2 -_Guar: z == z' - -h = head; -t = tail; -task = 0; - - -if (h < t) { - do - _invariant: Gamma_r && Gamma_h && Gamma_t // && ((r == z) => Gamma_task) - { - r = z; - do - _invariant: Gamma_r && Gamma_h && Gamma_t // && r <= z - - { - r = z; - } while (r % 2 == 1) - - level = levels[h % L]; - if (level == 1) { - task = tasks[h % L]; - } else { - task = -1; // fail - } - } while (z != r) - - if (CAS(head, h, h + 1) == 0) { - task = -1; // fail - } -} else { - task = 0; // empty -} - -ret = task; diff --git a/tests/rg/neg/pointers1 b/tests/rg/neg/pointers1 new file mode 100644 index 0000000..265cef5 --- /dev/null +++ b/tests/rg/neg/pointers1 @@ -0,0 +1,13 @@ +global var a: +_L: FALSE + +global var b: +_L: FALSE + +_Rely: a == a' && b == b' +_Guar: TRUE + +a = 2; +b = &a; +*b = 1; +assert a == 2; diff --git a/tests/rg/neg/pointers2 b/tests/rg/neg/pointers2 new file mode 100644 index 0000000..752bc3b --- /dev/null +++ b/tests/rg/neg/pointers2 @@ -0,0 +1,19 @@ +global var a: +_L: FALSE + +global var b: +_L: FALSE + +global var out: +_L: a % 2 == 0 + +global var secret: +_L: FALSE + +_Rely: a == a' && b == b' +_Guar: TRUE + +a = 1; +b = &a; +*b = 2; +out = secret; diff --git a/tests/rg/neg/pointers3 b/tests/rg/neg/pointers3 new file mode 100644 index 0000000..652feb8 --- /dev/null +++ b/tests/rg/neg/pointers3 @@ -0,0 +1,22 @@ +global var a: +_L: FALSE + +global var *b: +_L: FALSE +_PT: a + +global var out: +_L: a == 2 + +global var secret: +_L: FALSE + +_Gamma_0: out -> LOW +_Rely: a == a' && b == b' +_Guar: TRUE + +a = 2; +b = &a; +*b = 1; +out = secret; // SAFE: a = 1 +*b = 2; // UNSAFE: invalid control diff --git a/tests/rg/neg/pointers4 b/tests/rg/neg/pointers4 new file mode 100644 index 0000000..0ea1beb --- /dev/null +++ b/tests/rg/neg/pointers4 @@ -0,0 +1,21 @@ +global var a: +_L: FALSE +_PT: b + +global var b: +_L: FALSE + +global var c: +_L: *b == 1 + +global var secret: +_L: FALSE + +_Rely: a == a' && b == b' && c == c' +_Guar: TRUE + +a = 1; +b = &a; +a = 1; +c = secret; + diff --git a/tests/rg/neg/pointers5 b/tests/rg/neg/pointers5 new file mode 100644 index 0000000..0681d2c --- /dev/null +++ b/tests/rg/neg/pointers5 @@ -0,0 +1,21 @@ +global var a: +_L: FALSE +_PT: b + +global var b: +_L: FALSE + +global var c: +_L: *b == 1 + +global var secret: +_L: FALSE + +_Rely: a == a' && b == b' && c == c' +_Guar: TRUE + +b = &a; +a = 0; // SAFE +c = secret; +a = 1; // UNSAFE + diff --git a/tests/rg/neg/pointers6 b/tests/rg/neg/pointers6 new file mode 100644 index 0000000..381342a --- /dev/null +++ b/tests/rg/neg/pointers6 @@ -0,0 +1,15 @@ +global var a: +_L: FALSE +_PT: b + +global var b: +_L: FALSE + +global var c: +_L: *b == 1 + +_Rely: a == a' && b == b' && c == c' +_Guar: TRUE + +b = &a; + diff --git a/tests/rg/pointers1 b/tests/rg/pointers1 new file mode 100644 index 0000000..e813729 --- /dev/null +++ b/tests/rg/pointers1 @@ -0,0 +1,13 @@ +global var a: +_L: FALSE + +global var b: +_L: FALSE + +_Rely: a == a' && b == b' +_Guar: TRUE + +a = 1; +b = &a; +*b = 2; +assert a == 2; diff --git a/tests/rg/pointers2 b/tests/rg/pointers2 new file mode 100644 index 0000000..12aac8e --- /dev/null +++ b/tests/rg/pointers2 @@ -0,0 +1,21 @@ +global var a: +_L: FALSE + +global var b: +_L: FALSE + +global var out: +_L: a == 2 + +global var secret: +_L: FALSE + +_Gamma_0: out -> LOW +_Rely: a == a' && b == b' +_Guar: TRUE + +a = 2; +b = &a; +*b = 1; +out = secret; // SAFE: a = 1 +assert a == 1; diff --git a/tests/rg/pointers3 b/tests/rg/pointers3 new file mode 100644 index 0000000..07dc7f2 --- /dev/null +++ b/tests/rg/pointers3 @@ -0,0 +1,21 @@ +global var a: +_L: FALSE + +global var b: +_L: FALSE + +global var c: +_L: FALSE + +_Rely: a == a' && b == b' && c == c' +_Guar: TRUE + +a = 1; +b = &a; +c = &b; + +**c = 2; + +assert a == 2; +assert *b == 2; +assert **c == 2; diff --git a/tests/rg/pointers4 b/tests/rg/pointers4 new file mode 100644 index 0000000..3201afe --- /dev/null +++ b/tests/rg/pointers4 @@ -0,0 +1,21 @@ +global var a: +_L: FALSE +_PT: b + +global var b: +_L: FALSE + +global var c: +_L: *b == 1 + +global var secret: +_L: FALSE + +_Rely: a == a' && b == b' && c == c' +_Guar: TRUE + +a = 0; +b = &a; +a = 0; +c = secret; + diff --git a/tests/rg/seqlock/read b/tests/rg/seqlock/read index f07dfd5..9b03a6d 100644 --- a/tests/rg/seqlock/read +++ b/tests/rg/seqlock/read @@ -17,8 +17,7 @@ _Rely: z' >= z _Guar: (z' == z) do -// _invariant: Gamma_r1 -_invariant: Gamma_r1 && ((z == r1) => Gamma_r2) +_invariant: Gamma_r1 { do _invariant: Gamma_r1 diff --git a/tests/rg/treiber/put b/tests/rg/treiber/put new file mode 100644 index 0000000..55d9610 --- /dev/null +++ b/tests/rg/treiber/put @@ -0,0 +1,39 @@ +// TODO this example fails + +global obj n: +_Field: val + _L: n.level == 1 +_Field: level + _L: TRUE +_Field: next + _L: TRUE + +global var *head: +_L: TRUE +_PT: n + +global var *ss: +_L: TRUE +_PT: head, n + +global var v: +_L: l == 1 + +global var l: +_L: TRUE + +// _Gamma_0: n.val -> HIGH +_Rely: n.level == n'.level && n.val == n'.val && n.next == n'.next +_Guar: (n.level == 1) => (n'.level == 1) + +n.level = l; +n.val = v; + +do +_invariant: TRUE +{ + ss = head; + n.next = ss; +} +while(CAS(head, ss, &n) == 0) + diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 3fdfa7b..e3d2528 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -23,7 +23,7 @@ object Exec { block.children.map(c => { val res = exec(c, state) if (c.atomic) - // TODO change this to R implies + // TODO should there be a guaranttee check? res.copy(Qs = res.Qs.map(q => q.copy(pred = rImplies(q.pred, state)))) else res }), @@ -45,7 +45,7 @@ object Exec { new PredInfo( stableR(assert.expression, state), assert, - "StableR" + "Assert" ) ) .incPrimeIndicies @@ -53,14 +53,14 @@ object Exec { _state .addQs( new PredInfo( - eval(assert.expression, state), + eval(assert.expression, state, true), assert, "Assert" ) ) .incPrimeIndicies case havoc: Havoc => - val _state = checkVcs(state.Qs, state.debug, state.simplify) match { + val _state = checkVcs(state.Qs, state.debug, state.simplify, state) match { case Some(p) => if (!state.silent) printFalseVcs(p) if (state.debug) println("error found at havoc") @@ -76,6 +76,7 @@ object Exec { if (RG) { val gamma = computeGamma(guard.test, state) val stabR = stableR(gamma, state) + _state .addQs( new PredInfo(gamma, guard, "Gamma"), @@ -85,25 +86,24 @@ object Exec { } else { _state.incPrimeIndicies } - case ass: Assignment => - val assign = ass.asInstanceOf[Assignment] + case assign @ Assignment(lhs: Identifier, _, _) => val globalPred = - if (state.globals.contains(assign.lhs)) + if (state.globals.contains(lhs.ident)) BinOp.pred( "=>", - getL(assign.lhs, state), + getL(lhs, state), computeGamma(assign.expression, state) ) else Const._true - val controlPred = if (state.controls.contains(assign.lhs)) { + val controlPred = if (state.controls.contains(lhs)) { constructForall( state.controlledBy - .getOrElse(assign.lhs, Set()) + .getOrElse(lhs, Set()) .map(contr => { BinOp.pred( "=>", - eval(getL(contr, state).subst(Map(assign.lhs.toVar(state) -> Left(assign.expression))), state), // TODO - BinOp.pred("||", eval(contr.toGamma, state), getL(contr, state)) + eval(getL(contr, state).subst((Map(lhs.toVar(state) -> Left(assign.expression)), state)), state, true), + BinOp.pred("||", eval(contr.toGamma, state, true), getL(contr, state)) ) }) .toList @@ -118,20 +118,76 @@ object Exec { _state .addQs( new PredInfo(rImplies(guarantee, state), assign, "Guarantee"), - new PredInfo(rImplies(globalPred, state), assign, "Global"), - new PredInfo(rImplies(controlPred, state), assign, "Control") + new PredInfo(rImplies(globalPred, state), assign, "L => G"), + new PredInfo(rImplies(controlPred, state), assign, "secUpd") ) .incPrimeIndicies } else { _state .addQs( - new PredInfo(globalPred, assign, "Global"), - new PredInfo(controlPred, assign, "Control") + new PredInfo(globalPred, assign, "L => G"), + new PredInfo(controlPred, assign, "secUpd") + ) + .incPrimeIndicies + } + case assign @ Assignment(Dereference(id), _, _) => + var globalPred: Expression = null + var controlPred: Expression = null + id match { + case id: Id => + // Must be global + globalPred = BinOp.pred( + "=>", + getL(id, state), + computeGamma(assign.expression, state) + ) + + // Check if anything that b points to is a control variable + controlPred = constructForall( + state.pointsTo + .get(id) + .get + .filter(i => state.controls.contains(i)) + .map(i => { + state.controlledBy + .getOrElse(i, Set()) + .map(contr => + BinOp.pred( + "=>", + eval(getL(contr, state).subst((Map(i.toVar(state) -> Left(assign.expression)), state)), state, true), + BinOp.pred("||", eval(contr.toGamma, state, true), getL(contr, state)) + ) + ) + }) + .flatten + .toList + ) + case _ => throw new Error("Expected id") + + } + + val _state = evalWp(assign, state, RG) + + if (RG) { + val guarantee = guar(assign, state) + + _state + .addQs( + new PredInfo(rImplies(guarantee, state), assign, "Guarantee"), + new PredInfo(rImplies(globalPred, state), assign, "L => G"), + new PredInfo(rImplies(controlPred, state), assign, "secUpd") + ) + .incPrimeIndicies + } else { + _state + .addQs( + new PredInfo(globalPred, assign, "L => G"), + new PredInfo(controlPred, assign, "secUpd") ) .incPrimeIndicies } - case ass: ArrayAssignment => - val assign = ass.asInstanceOf[ArrayAssignment] + + case assign: ArrayAssignment => val indexSub = Map(Id.indexId.toVar(state) -> assign.lhs.ident) val globalPred = @@ -150,14 +206,19 @@ object Exec { BinOp.pred( "=>", eval( - getL(contr, state).subst(Map(assign.lhs.ident.toVar(state) -> Right((assign.lhs.index, assign.expression)))), - state - ), // TODO + eval( + getL(contr, state).subst((Map(assign.lhs.ident.toVar(state) -> Right((assign.lhs.index, assign.expression))), state)), + state, + true + ), + state, + true + ), BinOp.pred( "||", - eval(contr.toGamma, state), - getL(contr, state).subst(Map(Id.indexId.toVar(state) -> Left(assign.lhs.index))) - ) // TODO check subst is correct + eval(contr.toGamma, state, true), + eval(getL(contr, state).subst((Map(Id.indexId.toVar(state) -> Left(assign.lhs.index)), state)), state, true) + ) ) }) .toList @@ -209,106 +270,253 @@ object Exec { } def evalWp(stmt: Stmt, state: State, RG: Boolean) = { - // if (RG) state.copy(Qs = state.Qs.map(Q => Q.copy(pred = BinOp("&&", wp(Q.pred, stmt, state), stableR(wp(Q.pred, stmt, state), state))))) - // TODO should use rImplies - // is this even possible? if the rely is false then the whole expression becomes true if (RG) state.copy(Qs = state.Qs.map(Q => Q.copy(pred = rImplies(wp(Q.pred, stmt, state), state)))) else state.copy(Qs = state.Qs.map(Q => Q.copy(pred = wp(Q.pred, stmt, state)))) - // state.copy(Qs = state.Qs.map(Q => Q.copy(pred = wp(Q.pred, stmt, state)))) } def wp(Q: Expression, stmt: Stmt, state: State): Expression = { stmt match { - case Assume(exp, _) => BinOp.pred("=>", eval(exp, state), Q) + case Assume(exp, _) => BinOp.pred("=>", eval(exp, state, true), Q) case Guard(exp, _) => val stabRB = stableR(exp, state) BinOp.pred( "&&", - BinOp.pred("=>", BinOp.pred("&&", eval(exp, state), stabRB), Q), - BinOp.pred("=>", PreOp("!", Type.TBool, Type.TBool, stabRB), eval(exp, state)) + BinOp.pred("=>", BinOp.pred("&&", eval(exp, state, true), stabRB), Q), + BinOp.pred("=>", PreOp("!", TBool, TBool, stabRB), eval(exp, state, true)) ) case Assert(exp, checkStableR, _) => - /* BinOp( - "&&", - eval(exp, state), - Q - ) // Potentially move to exec to evaluate separately - */ Q case havoc: Havoc => Q - case ass: Assignment => - val assign = ass.asInstanceOf[Assignment] + case assign @ Assignment(lhs: Id, _, _) => val rhsGamma = computeGamma(assign.expression, state) - Q.subst( - Map( - (assign.lhs.toGamma.toVar(state) -> Left(rhsGamma)), - (assign.lhs.toVar(state) -> Left(eval(assign.expression, state))) - ) + eval( + Q.subst( + ( + Map( + (lhs.toGamma.toVar(state) -> Left(rhsGamma)), + (lhs.toVar(state) -> Left(eval(assign.expression, state, false))) + ), + state + ) + ), + state, + false ) - case ass: ArrayAssignment => - val assign = ass.asInstanceOf[ArrayAssignment] + case assign @ Assignment(Dereference(id), _, _) => val rhsGamma = computeGamma(assign.expression, state) + val lhs = eval(assign.lhs, state, false) match { + case Dereference(v: Var) => v + case _ => throw new Error("Unexpected dereference") + } - Q.subst( - Map( - (assign.lhs.ident.toGamma.toVar(state) -> Right( - (eval(assign.lhs.index, state), rhsGamma) - )), - (assign.lhs.ident.toVar(state) -> Right( - eval(assign.lhs.index, state), - eval(assign.expression, state) - )) - ) + eval( + Q.subst( + ( + Map( + (Dereference(lhs) -> Left(eval(assign.expression, state, true))), + (Dereference(lhs.toGamma(state)) -> Left(rhsGamma)) + ), + state + ) + ), + state, + false + ) + case assign @ Assignment(o @ ObjIdAccess(id, field), _, _) => + val rhsGamma = computeGamma(assign.expression, state) + val lhs = eval(o, state, false) match { + case lhs: ObjVarAccess => lhs + case lhs => throw new Error(s"Unexpected object $lhs (${lhs.getClass})") + } + + eval( + Q.subst( + Map( + (o.toVar(state) -> Left(eval(assign.expression, state, true))), + (o.toGamma.toVar(state) -> Left(rhsGamma)) + ), + state + ), + state, + false + ) + case assign: ArrayAssignment => + val rhsGamma = computeGamma(assign.expression, state) + + eval( + Q.subst( + ( + Map( + (assign.lhs.ident.toGamma.toVar(state) -> Right( + (eval(assign.lhs.index, state, true), rhsGamma) + )), + (assign.lhs.ident.toVar(state) -> Right( + eval(assign.lhs.index, state, true), + eval(assign.expression, state, true) + )) + ), + state + ) + ), + state, + false ) case stmt => - println("Unhandled statement(wp exec): " + stmt) + println(s"Unhandled statement(wp exec): $stmt (${stmt.getClass})") Q } } - def eval(expr: Expression, state: State): Expression = expr match { - case id: Id => id.toVar(state) - case id: IdAccess => id.toVar(state).copy(index = eval(id.index, state)) - case BinOp(op, t1, t2, arg1, arg2) => - BinOp(op, t1, t2, eval(arg1, state), eval(arg2, state)) - case PreOp(op, t1, t2, arg) => PreOp(op, t1, t2, eval(arg, state)) - case s: VarStore => - s.copy( - array = eval(s.array, state), - index = eval(s.index, state), - exp = eval(s.exp, state) - ) - case a: VarAccess => a.copy(index = eval(a.index, state)) - case forall: ForAll => - forall.copy( - bound = forall.bound.map(b => eval(b, state)), - body = eval(forall.body, state) - ) - case _: Lit | _: Const | _: Var => expr - case expr => - println(s"Unhandled expression(eval): [${expr.getClass()}] $expr") - expr + def eval(expr: Expression, state: State, memAccess: Boolean): Expression = + expr match { + case id: Id if (id.memLoc) => id.toVar(state) + case va: Var if (va.ident.memLoc) => va + case id: Id if (state.globals.contains(id.getBase)) => + val mem = + (if (id.prime) Id.memId.toPrime.toVar(state) else if (id.nought) Id.memId.toVar(state).toNought else Id.memId.toVar(state)) + if (id == Id.indexId) id.toVar(state) + else if (id.memLoc) id.toVar(state) + else if (memAccess && !id.gamma) + VarAccess(mem, eval(Id.getAddr(id, state), state, true)) + else if (memAccess && id.gamma) + VarAccess(mem.toGamma(state), eval(Id.getAddr(id, state), state, true)) + else + id.toVar(state) + case id: Id => id.toVar(state) + case v: Var if (state.globals.contains(v.ident.getBase)) => + val mem = + (if (v.ident.prime) Id.memId.toPrime.toVar(state) + else if (v.ident.nought) Id.memId.toVar(state).toNought + else Id.memId.toVar(state)) + if (v.ident == Id.indexId) v + else if (memAccess && !v.ident.gamma) + VarAccess(mem, eval(Id.getAddr(v.ident, state), state, true)) + else if (memAccess && v.ident.gamma) + VarAccess(mem.toGamma(state), eval(Id.getAddr(v.ident, state), state, true)) + else v + case id: IdAccess => id.toVar(state).copy(index = eval(id.index, state, memAccess)) + case idObj: ObjIdAccess => + val mem = + (if (idObj.ident.prime) Id.memId.toPrime.toVar(state) + else if (idObj.ident.nought) Id.memId.toVar(state).toNought + else Id.memId.toVar(state)) + if (memAccess) VarAccess(mem, eval(idObj.getAddr(state), state, true)) + else idObj.toVar(state) + case varObj: ObjVarAccess => + val mem = + (if (varObj.ident.prime) Id.memId.toPrime.toVar(state) + else if (varObj.ident.nought) Id.memId.toVar(state).toNought + else Id.memId.toVar(state)) + if (memAccess) VarAccess(mem, eval(varObj.getAddr(state), state, true)) + else varObj + case deref @ Dereference(id) => + deref.copy(ident = eval(deref.ident, state, false)) match { + case Dereference(v: Var) if (memAccess) => + val memId = v.copy(ident = v.ident.copy(name = Id.memId.name)) + VarAccess(memId, eval(VarAccess(memId, state.addrs.get(v.ident).get), state, true)) + case d @ _ => d + } + case r @ Reference(id) => + r.copy(ident = eval(r.ident, state, false)) match { + case Reference(v: Var) => eval(state.addrs.get(v.ident).get, state, true) + case r @ _ => r + } + case BinOp(op, t1, t2, arg1, arg2) => + BinOp(op, t1, t2, eval(arg1, state, memAccess), eval(arg2, state, memAccess)) + case PreOp(op, t1, t2, arg) => PreOp(op, t1, t2, eval(arg, state, memAccess)) + case Declassify(e, d) => eval(e, state, memAccess) + case s: VarStore => + s.copy( + array = eval(s.array, state, memAccess), + index = eval(s.index, state, memAccess), + exp = eval(s.exp, state, memAccess) + ) + case a: VarAccess => a.copy(index = eval(a.index, state, memAccess)) + case forall: ForAll => + forall.copy( + bound = forall.bound.map(b => eval(b, state, memAccess)), + body = eval(forall.body, state, memAccess) + ) + case _: Lit | _: Const | _: Var => expr + case expr => + println(s"Unhandled expression(eval): [${expr.getClass()}] $expr") + expr + } + + private def skipMemLocs(v: Variable) = v match { + case v: Var if (v.ident.memLoc) => false + case v => true } - def getBaseVars(vars: Set[Var]): Set[Var] = vars.map(v => v.getBase.resetIndex) - def getBaseArrays(vars: Set[VarAccess]): Set[VarAccess] = vars.map(v => v.getBase.resetIndex) + def getBaseVars(vars: Set[Variable]): Set[Variable] = vars + .filter(skipMemLocs) + .map(v => + v.getBase.resetIndex match { + case v: VarAccess => v.name + case v @ _ => v + } + ) + def getBaseVariables(vars: Set[Variable]): Set[Variable] = vars.filter(skipMemLocs).map(v => v.getBase.resetIndex) def getRely(exp: Expression, state: State) = { - val evalExp = eval(exp, state) + val evalExp = eval(exp, state, false) + + val p = + constructForall( + getBaseVariables(evalExp.vars - Id.indexId.toVar(state)) + .map(v => { + val pred = if (state.globals.contains(v.ident) || v.ident.getBase == Id.memId) { + // BinOp( + // "&&", + BinOp.pred( + "=>", + BinOp("==", TInt, TBool, v, v.toPrime(state)), + BinOp.pred("==", v.toGamma(state), v.toPrime(state).toGamma(state)) + ) // , + // BinOp("=>", primed(getL(v.ident, state), state), v.toPrime(state).toGamma(state)) + // ) + } else { + BinOp.pred( + "&&", + BinOp("==", TInt, TBool, v, v.toPrime(state)), + BinOp.pred("==", v.toGamma(state), v.toPrime(state).toGamma(state)) + ) + + } + + v match { + case m: VarAccess if (m.ident == Id.memId) => pred + case v: VarAccess => + BinOp.pred( + "&&", + pred, + eval( + eval(state.arrRelys.getOrElse(v.ident, Const._true), state, false) + .subst((Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, false))), state)), + state, + false + ) + ) + + case _ => pred + } + }) + .toList + ) eval( BinOp.pred( "&&", constructForall( - getBaseVars(evalExp.vars - Id.indexId.toVar(state)) + getBaseVariables(evalExp.vars - Id.indexId.toVar(state)) .map(v => { - if (state.globals.contains(v.ident)) { + val pred = if (state.globals.contains(v.ident) || v.ident.getBase == Id.memId) { // BinOp( // "&&", BinOp.pred( "=>", - BinOp("==", Type.TInt, Type.TBool, v, v.toPrime(state)), + BinOp("==", TInt, TBool, v, v.toPrime(state)), BinOp.pred("==", v.toGamma(state), v.toPrime(state).toGamma(state)) ) // , // BinOp("=>", primed(getL(v.ident, state), state), v.toPrime(state).toGamma(state)) @@ -316,83 +524,87 @@ object Exec { } else { BinOp.pred( "&&", - BinOp("==", Type.TInt, Type.TBool, v, v.toPrime(state)), + BinOp("==", TInt, TBool, v, v.toPrime(state)), BinOp.pred("==", v.toGamma(state), v.toPrime(state).toGamma(state)) ) } - }) - .toList - ++ - getBaseArrays(evalExp.arrays) - .map(v => { - val pred = if (state.globals.contains(v.ident)) { - // BinOp( - // "&&", - BinOp.pred( - "=>", - BinOp("==", Type.TInt, Type.TBool, v, v.toPrime(state)), - BinOp.pred("==", v.toGamma(state), v.toPrime(state).toGamma(state)) - ) //, - // BinOp("=>", primed(getL(v, state), state), v.toPrime(state).toGamma(state)) - // ) - } else { - BinOp.pred( - "&&", - BinOp("==", Type.TInt, Type.TBool, v, v.toPrime(state)), - BinOp.pred("==", v.toGamma(state), v.toPrime(state).toGamma(state)) - ) - } + v match { + case m: VarAccess if (m.ident == Id.memId) => pred + case v: VarAccess => BinOp.pred( "&&", pred, - eval(state.arrRelys.getOrElse(v.ident, Const._true), state) - .subst(Map(Id.indexId.toVar(state) -> Left(eval(v.index, state)))) + eval(state.arrRelys.getOrElse(v.ident, Const._true), state, false) + .subst((Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, false))), state)) ) - }) - .toList + case _ => pred + } + }) + .toList ), - eval(state.rely, state) + eval(state.rely, state, false) ), - state + state, + true ) } - def getL(id: Id, state: State): Expression = { - if (id == Id.tmpId) Const._true - else + def getL(id: Identifier, state: State): Expression = id match { + case Id.tmpId => Const._true + case id: Id if (id.memLoc) => Const._true + case _: IdAccess | _: VarAccess => + id match { + case id: IdAccess => + eval( + getL(id.ident, state).subst( + (Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true))), state) + ), + state, + true + ) + case id: VarAccess => + eval( + getL(id.ident, state).subst( + (Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true))), state) + ), + state, + true + ) + } + case id: Identifier => eval( state.L.getOrElse(id, throw new Error("L not defined for " + id)), - state + state, + true ) } - def getL(id: IdAccess, state: State): Expression = - getL(id.ident, state) - .subst(Map(Id.indexId.toVar(state) -> Left(eval(id.index, state)))) - - def getL(v: VarAccess, state: State): Expression = - getL(v.ident, state) - .subst(Map(Id.indexId.toVar(state) -> Left(eval(v.index, state)))) - def primed(p: Expression, state: State) = - eval(p, state).subst( - (state.ids ++ state.arrayIds) - .map(id => id.toVar(state) -> Left(id.toPrime.toVar(state))) - .toMap + eval( + eval(p, state, false).subst( + ( + (state.arrayIds + Id.memId) + .map(id => id.toVar(state) -> Left(id.toPrime.toVar(state))) + .toMap, + state + ) + ), + state, + false ) - // TODO take havoc statements into account def stableR(p: Expression, state: State) = eval( BinOp.pred("=>", BinOp.pred("&&", getRely(p, state), p), primed(p, state)), - state + state, + true ) def rImplies(p: Expression, state: State) = { - eval(BinOp.pred("=>", getRely(p, state), primed(p, state)), state) + eval(BinOp.pred("=>", getRely(p, state), primed(p, state)), state, true) } def stableR(p: Expression, index: Expression, state: State) = @@ -401,31 +613,33 @@ object Exec { "=>", BinOp.pred( "&&", - getRely(p, state).subst(Map(Id.indexId.toVar(state) -> Left(index))), + getRely(p, state).subst((Map(Id.indexId.toVar(state) -> Left(index)), state)), p ), primed(p, state) ), - state + state, + true ) def rImplies(p: Expression, index: Expression, state: State) = eval( BinOp.pred( "=>", - getRely(p, state).subst(Map(Id.indexId.toVar(state) -> Left(index))), + getRely(p, state).subst((Map(Id.indexId.toVar(state) -> Left(index)), state)), primed(p, state) ), - state + state, + true ) def guar(a: Assignment, state: State) = { - val guar = eval(state.guar, state) - val vars = getBaseVars(guar.vars ++ guar.arrays.map(a => a.name)) - val subst = vars.map(v => List(v -> Left(v.toNought), v.toPrime(state) -> Left(v))).flatten.toMap - val gPrime = guar.subst(subst) - val _subst = vars.map(v => v.toNought.asInstanceOf[Var] -> Left(v)).toMap - wp(gPrime, a, state).subst(_subst) + val guar = eval(state.guar, state, false) + val vars = getBaseVars(guar.vars) + val subst = vars.map(v => List(v -> Left(v.toNought), v.toPrime(state) -> Left(v))).flatten.toMap[Expression, Left[Expression, Nothing]] + val gPrime = guar.subst((subst, state)) + val _subst = Map[Expression, Left[Expression, Nothing]](Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) + eval(wp(eval(gPrime, state, true), a, state).subst((_subst, state)), state, true) } def guar(a: ArrayAssignment, state: State) = { @@ -434,38 +648,40 @@ object Exec { BinOp.pred( "&&", state.guar, - eval(state.arrGuars.getOrElse(a.lhs.ident, Const._true), state).subst(Map(Id.indexId.toVar(state) -> Left(a.lhs.index))) + eval(state.arrGuars.getOrElse(a.lhs.ident, Const._true), state, true) + .subst((Map(Id.indexId.toVar(state) -> Left(a.lhs.index)), state)) ), - state + state, + true ) - val vars = getBaseVars(guar.vars ++ guar.arrays.map(a => a.name)) - val subst = vars.map(v => List(v -> Left(v.toNought), v.toPrime(state) -> Left(v))).flatten.toMap - val gPrime = guar.subst(subst) - val _subst = vars.map(v => v.toNought.asInstanceOf[Var] -> Left(v)).toMap - wp(gPrime, a, state).subst(_subst) + val vars = getBaseVars(guar.vars) + val subst = vars.map(v => List(v -> Left(v.toNought), v.toPrime(state) -> Left(v))).flatten.toMap[Expression, Left[Expression, Nothing]] + val gPrime = eval(guar.subst((subst, state)), state, true) + val _subst = vars.map(v => v.toNought.asInstanceOf[Var] -> Left(v)).toMap[Expression, Left[Expression, Nothing]] + eval(wp(gPrime, a, state).subst((_subst, state)), state, true) } def computeGamma(exp: Expression, state: State): Expression = { - val expEval = eval(exp, state) - constructForall( + val expEval = eval(exp, state, false) + val basePred = constructForall( expEval.vars - .map(v => + .map(v => { eval( BinOp.pred("||", v.toGamma(state), getL(v.ident, state)), - state + // BinOp.pred("||", VarAccess(Id.memId.toGamma.toVar(state), Id.getAddr(v.ident, state)), getL(v.ident, state)), + state, + true ) // Default to high - ) - .toList ++ - expEval.arrays - .map(a => { - val subst = Map[Var, Left[Expression, Nothing]](Id.indexId.toVar(state) -> Left(eval(a.index, state))) - eval( - BinOp.pred("||", a.toGamma(state), getL(a.ident, state)).subst(subst), - state - ) // Default to high - }) - .toList + + }) + .toList ) + + exp match { + case Declassify(_, d) => BinOp.pred("||", d, basePred) + case PreOp("!", TBool, TBool, Declassify(_, d)) => BinOp.pred("||", d, basePred) // TODO there should be a better way to do this + case _ => basePred + } } def joinStates(states: List[State], state: State, blockName: String) = { diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index ad5be1f..a22beff 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -1,30 +1,25 @@ package wptool -import scala.reflect.runtime.universe.{TypeTag, typeOf} - -object Type extends Enumeration { - type Type = Value - val TBool, TInt = Value -} +sealed abstract class Type +case class TPointer(pointerType: Type) extends Type +case object TBool extends Type { def instance = this } +case object TInt extends Type { def instance = this } trait Expression extends beaver.Symbol { // returns all vars in the expression, does NOT include array indices - def vars: Set[Var] + def vars: Set[Variable] // returns all vars in the expression, does NOT include array indices - def ids: Set[Id] + def ids: Set[Identifier] def subst(su: Subst): Expression - def arrays: Set[VarAccess] - - def expType: Type.Type + def expType: Type } case class Lit(arg: Int) extends Expression { override def toString: String = arg.toString override def vars = Set() override def ids = Set() - override def arrays = Set() - override def subst(su: Subst): Lit = this - override def expType = Type.TInt + override def subst(su: Subst) = this + override def expType = TInt } trait Identifier extends Expression { @@ -32,6 +27,7 @@ trait Identifier extends Expression { def toGamma: Identifier def toVar(state: State): Variable def getBase: Identifier + def ident: Id } trait Variable extends Expression { @@ -44,38 +40,41 @@ trait Variable extends Expression { } // id parsed from input - need to convert to Var before use in predicates etc. -case class Id(name: String, override val expType: Type.Type, prime: Boolean, gamma: Boolean, nought: Boolean) extends Identifier { +case class Id(name: String, override val expType: Type, prime: Boolean, gamma: Boolean, nought: Boolean, memLoc: Boolean) + extends Identifier { override def toString: String = - (if (gamma) "Gamma_" else "") + name + (if (prime) "'" else "") + (if (nought) "⁰" else "") + (if (gamma) "Gamma_" else "") + (if (memLoc) "memL_" else "") + name + (if (prime) "'" else "") + (if (nought) "⁰" else "") override def vars = throw new Error("Tried to get var from id") override def ids = Set(this) - override def arrays = Set() override def subst(su: Subst) = throw new Error(s"tried to subst id $this") def toVar(state: State) = Var(this, getIndex(state)) def toPrime = this.copy(prime = true) // TODO change type - def toGamma = Id(name, Type.TBool, prime, true, nought) + def toGamma = Id(name, TBool, prime, true, nought, false) def getIndex(state: State) = { - // println(state.indicies.map { case (k, v) => (k, k == this.copy(gamma = false, expType = Type.TInt)) }) - // println(this.copy(gamma = false, expType = Type.TInt)) - if (!gamma) state.indicies.getOrElse(this, throw new Error(s"Index not found for var $this with type $expType")) - // TODO change Type.TInt + if (!gamma) state.indicies.getOrElse(this.copy(memLoc = false), throw new Error(s"Index not found for var $this with type $expType")) else state.indicies.getOrElse( - this.copy(gamma = false, expType = Type.TInt), + this.copy(gamma = false, expType = TInt), // TODO change TInt throw new Error(s"Index not found for gamma var $this with type $expType") ) } + override def ident = this + // TODO use actual type - override def getBase = Id(name, Type.TInt, false, false, false) + override def getBase = Id(name, TInt, false, false, false, false) } object Id { - // TODO change to bool - val tmpId = Id("tmp", Type.TInt, false, false, false) - val indexId = Id("_i", Type.TInt, false, false, false) + val tmpId = Id("tmp", TInt, false, false, false, false) + val indexId = Id("_i", TInt, false, false, false, false) + val memId = Id("mem", TInt, false, false, false, false) + + def getAddr(id: Id, state: State): Expression = { + state.addrs.getOrElse(id.getBase, throw new Error("Couldn't resolve memeory address")) + } } case class Var(ident: Id, index: Int, tmp: Boolean = false) extends Variable { @@ -83,8 +82,7 @@ case class Var(ident: Id, index: Int, tmp: Boolean = false) extends Variable { (if (tmp) "tmp_" else "") + ident.toString __ index override def vars = Set(this) override def ids = Set(this.ident) - override def arrays = Set() - override def subst(su: Subst) = su.get(this) match { + override def subst(su: Subst) = su._1.get(this) match { case Some(Left(e: Expression)) => e case Some(Right(_)) => throw new Error(s"Tried to subst var $this with index") @@ -105,11 +103,10 @@ case class Var(ident: Id, index: Int, tmp: Boolean = false) extends Variable { } case class IdAccess(ident: Id, index: Expression) extends Expression with Identifier { - def this(name: String, index: Expression) = this(Id(name, Type.TInt, false, false, false), index) - def this(name: String, prime: Boolean, gamma: Boolean, index: Expression) = this(Id(name, Type.TInt, prime, gamma, false), index) - def vars = index.vars - def ids = index.ids - def arrays = throw new Error("tried to get array from IdAccess") + def this(name: String, index: Expression) = this(Id(name, TInt, false, false, false, false), index) + def this(name: String, prime: Boolean, gamma: Boolean, index: Expression) = this(Id(name, TInt, prime, gamma, false, false), index) + def vars = index.vars // TODO throw error? + def ids = index.ids + this def subst(su: Subst) = throw new Error("tried to subst var id") override def toString = ident + "[" + index + "]" def toGamma = this.copy(ident = ident.toGamma) @@ -122,27 +119,91 @@ case class IdAccess(ident: Id, index: Expression) extends Expression with Identi // array access with Var for use in logical predicates case class VarAccess(name: Var, index: Expression) extends Variable { - def vars = index.vars - def ids = index.ids - def arrays = Set(this) + def vars = index.vars + this + def ids = index.ids + this.ident + // TODO document/comment def subst(su: Subst) = { - val updatedArr = this.copy(index = index.subst(su)) - su.get(name) match { - case Some(Right((i: Expression, e: Expression))) => - VarStore(updatedArr, i, e) - case Some(Left(v: Var)) => updatedArr.copy(name = v) // to handle priming - case Some(Left(_)) => - throw new Error("Tried to subst varaccess without index") - case None => updatedArr + val updatedArr = this.copy(index = index.subst((su._1.filter { case (v, _) => v.expType == TInt }, su._2))) + if (name.ident.getBase != Id.memId) { + su._1.get(name) match { + case Some(Right((i: Expression, e: Expression))) => + VarStore(updatedArr, i, e) + case Some(Left(v: Var)) => updatedArr.copy(name = v) // to handle priming + case Some(Left(_)) => + throw new Error("Tried to subst varaccess without index") + case None => updatedArr + } + } else { + val memId = + ( + if (su._1.contains(this.name)) updatedArr.copy(name = su._1.get(this.name).get.left.get.asInstanceOf[Var]) + else updatedArr + ) + + su._1 + .filter { + case (v: Var, Left(_)) => + !su._2.arrayIds.contains( + v.ident.getBase + ) && this.ident.gamma == v.ident.gamma && this.ident.prime == v.ident.prime && this.ident.nought == v.ident.nought && su._2.globals + .contains(v.ident.getBase) + case (v, Right(_)) => false + case (d @ Dereference(v: Var), _) => + !su._2.arrayIds.contains( + v.ident.getBase + ) && this.ident.gamma == v.ident.gamma && this.ident.prime == v.ident.prime && this.ident.nought == v.ident.nought && su._2.globals + .contains(v.ident.getBase) + case (v: ObjVarAccess, _) => + !su._2.arrayIds.contains( + v.ident.getBase + ) && this.ident.gamma == v.ident.gamma && this.ident.prime == v.ident.prime && this.ident.nought == v.ident.nought && su._2.globals + .contains(v.ident.getBase) + case s @ _ => throw new Error(s"Unexpected subst ($s, ${s._1.getClass})") + } + .foldLeft(memId: Expression) { + case (p, (v: Var, Left(e))) => { + // TODO handle _i + this.index match { + case _ if v.ident == Id.indexId => p + case i: Var if (su._2.addrs.get(v.ident.getBase).get != i.ident) => p + case _ if (name.index != v.index) => p + case _ => + VarStore(p, eval(su._2.addrs.get(v.ident.getBase).get, su._2), e) + } + } + case (p, (Dereference(v: Var), Left(e))) => + this.index match { + case _ if v.ident == Id.indexId => p + case _ if (name.index != v.index) => p + case _ => + val memId = v.ident.copy(name = Id.memId.name).toVar(su._2) + VarStore( + p, + VarAccess(memId.copy(ident = memId.ident.copy(gamma = false)), eval(su._2.addrs.get(v.ident.getBase).get, su._2)), + e + ) + } + case (p, (o: ObjVarAccess, Left(e))) => + this.index match { + case _ if (name.index != o.name.index) => p + case _ => VarStore(p, o.getAddr(su._2), e) + } + } + } } + private def eval(exp: Expression, state: State) = exp match { + case i: Id => i.toVar(state) + case _ => exp // TODO + } + override def toString = name + "[" + index + "]" def toGamma(state: State) = this.copy(name = name.toGamma(state)) def toPrime(state: State) = this.copy(name = name.toPrime(state)) def toNought = this.copy(name = name.toNought) - def ident = name.ident + def ident = name.ident // TODO why not IdAccess override def expType = ident.expType override def getBase = this.copy(name = name.getBase) override def resetIndex = this.copy(name = name.resetIndex) @@ -151,47 +212,68 @@ case class VarAccess(name: Var, index: Expression) extends Variable { case class VarStore(array: Expression, index: Expression, exp: Expression) extends Expression { def vars = array.vars ++ index.vars ++ exp.vars def ids = array.ids ++ index.ids ++ exp.ids - def arrays = array.arrays ++ index.arrays ++ exp.arrays def subst(su: Subst) = VarStore(array.subst(su), index.subst(su), exp.subst(su)) override def expType = array.expType } -/* -case class ArrayConstDefault(name: Var, const: Expression) extends Expression { - def vars = const.vars - def ids = const.ids ++ name.ids - def arrays = const.arrays ++ name.arrays - def subst(su: Subst) = ArrayConstDefault(name, const.subst(su)) - override def expType = name.expType +case class ObjIdAccess(ident: Id, field: String) extends Expression with Identifier { + def this(name: String, field: String) = this(Id(name, TInt, false, false, false, false), field) + def vars = throw new Error("expected var") + def ids = Set(this) + def subst(su: Subst) = throw new Error("tried to subst var id") + override def toString = ident + "." + field + def toGamma = this.copy(ident = ident.toGamma) + def toPrime = this.copy(ident = ident.toPrime) + override def expType = ident.expType + def getAddr(state: State) = BinOp("+", TInt, TInt, state.addrs.get(ident.getBase).get, Lit(0)) // TODO + + def toVar(state: State) = ObjVarAccess(ident.toVar(state), field) + def getBase = this.copy(ident = ident.getBase) } - */ -case class PreOp(op: String, override val expType: Type.Type, argType: Type.Type, arg: Expression) extends Expression { +case class ObjVarAccess(name: Var, field: String) extends Expression with Variable { + def vars = Set(this) + def ids = Set(this.ident) + def subst(su: Subst) = + if (su._1.contains(this)) su._1.get(this).get.left.get + else this + override def toString = ident + "." + field + def toGamma(state: State) = this.copy(name = name.toGamma(state)) + def toPrime(state: State) = this.copy(name = name.toPrime(state)) + override def expType = ident.expType + + def getBase = this.copy(name = name.getBase) + + def getAddr(state: State) = ObjIdAccess(name.ident, field).getAddr(state) + + def ident = name.ident + def toNought = this.copy(name = name.toNought) + def resetIndex = this.copy(name = name.resetIndex) +} + +case class PreOp(op: String, override val expType: Type, argType: Type, arg: Expression) extends Expression { override def toString: String = "(" + op + " " + arg + ")" override def vars = arg.vars override def ids = arg.ids - def arrays = arg.arrays def subst(su: Subst) = this.copy(arg = arg.subst(su)) } -case class PostOp(op: String, override val expType: Type.Type, argType: Type.Type, arg: Expression) extends Expression { +case class PostOp(op: String, override val expType: Type, argType: Type, arg: Expression) extends Expression { override def toString: String = "(" + arg + " " + op + ")" override def vars = arg.vars override def ids = arg.ids - def arrays = arg.arrays def subst(su: Subst) = this.copy(arg = arg.subst(su)) } -case class BinOp(op: String, override val expType: Type.Type, argType: Type.Type, arg1: Expression, arg2: Expression) extends Expression { +case class BinOp(op: String, override val expType: Type, argType: Type, arg1: Expression, arg2: Expression) extends Expression { override def toString: String = "(" + arg1 + " " + op + " " + arg2 + ")" override def vars = arg1.vars ++ arg2.vars override def ids = arg1.ids ++ arg2.ids - def arrays = arg1.arrays ++ arg2.arrays def subst(su: Subst) = this.copy(arg1 = arg1.subst(su), arg2 = arg2.subst(su)) } object BinOp { - def pred(op: String, arg1: Expression, arg2: Expression) = BinOp(op, Type.TBool, Type.TBool, arg1, arg2) + def pred(op: String, arg1: Expression, arg2: Expression) = BinOp(op, TBool, TBool, arg1, arg2) } object Const { @@ -203,28 +285,57 @@ case class Const(name: String) extends Expression { override def toString: String = name.toString override def vars = Set() override def ids = Set() - override def arrays = Set() override def subst(su: Subst): Const = this - override def expType = Type.TBool + override def expType = TBool } // TODO change to bool expression case class CompareAndSwap(x: Id, e1: Expression, e2: Expression) extends Expression { - def this(x: String, e1: Expression, e2: Expression) = this(new Id(x, Type.TInt, false, false, false), e1, e2) + def this(x: String, e1: Expression, e2: Expression) = this(new Id(x, TInt, false, false, false, false), e1, e2) override def toString: String = "CAS(" + x + ", " + e1 + ", " + e2 + ")" override def vars = e1.vars ++ e2.vars override def ids = e1.ids ++ e2.ids - def arrays = e1.arrays ++ e2.arrays override def subst(su: Subst) = this - override def expType = Type.TInt // TODO + override def expType = TInt // TODO +} + +case class Declassify(e: Expression, d: Expression) extends Expression { + override def toString: String = "d(" + e + ", " + d + ")" + override def vars = e.vars + override def ids = e.ids + override def subst(su: Subst) = this.copy(e.subst(su)) + override def expType = TInt // TODO } case class ForAll(bound: Set[_ <: Expression], body: Expression) extends Expression { def this(bound: Array[Expression], body: Expression) = this(bound.toSet, body) override def ids = body.ids -- (bound.map(id => id.ids).flatten) override def vars = body.vars -- (bound.map(v => v.vars).flatten) - def arrays = body.arrays -- bound.map(a => a.arrays).flatten override def subst(su: Subst) = ForAll(bound, body.subst(su)) override def toString = s"∀ ${bound.mkString(", ")} : $body" - override def expType = Type.TBool + override def expType = TBool +} + +case class Dereference(ident: Expression) extends Expression { + def this(x: String) = this(Id(x, TInt, false, false, false, false)) + override def toString = s"*$ident" + override def vars = ident.vars + override def ids = ident.ids + override def subst(su: Subst) = Dereference(ident.subst(su)) + + // TODO + override def expType = ident.expType match { + case TPointer(t) => t + case TInt | TBool => ident.expType + case _ => throw new Error("Invalid pointer type") + } +} + +case class Reference(ident: Expression) extends Expression { + def this(x: String) = this(Id(x, TInt, false, false, false, false)) + override def toString = s"&$ident" + override def vars = ident.vars + override def ids = ident.ids + override def subst(su: Subst) = Reference(ident.subst(su)) + override def expType = TPointer(ident.expType) } diff --git a/wptool/src/wptool/Parser.grammar b/wptool/src/wptool/Parser.grammar index 9ad2307..41dc8f7 100644 --- a/wptool/src/wptool/Parser.grammar +++ b/wptool/src/wptool/Parser.grammar @@ -3,6 +3,8 @@ %terminals GLOBALVAR, LOCALVAR; %terminals GLOBALARRAY, LOCALARRAY; +%terminals GLOBALOBJ; +%terminals FIELD; //%terminals RETURN, BREAK, CONTINUE; %terminals IF, ELSE, WHILE, DO; @@ -26,14 +28,18 @@ %terminals AND; %terminals OR; %terminals COLON; +%terminals DOT; %terminals ASG; %terminals COMMA, SEMICOLON; %terminals FORALL; %terminals ASSERT; %terminals CAS; +%terminals DECLASSIFY; + %terminals INVARIANT, GAMMA, GAMMA_0, RELY, GUAR; %terminals LPRED; +%terminals PT; %terminals MAPSTO; %terminals PRIMEGAMMAID; %terminals PRIMEID; @@ -65,8 +71,12 @@ %typeof NUM = "Integer"; +%typeof ptrdef = "VarDef"; + %typeof boolexpr = "Expression"; %typeof intexpr = "Expression"; +%typeof ptrexpr = "Expression"; +%typeof intid = "Id"; %typeof local = "Stmt"; @@ -81,6 +91,7 @@ %typeof arrrely = "Rely"; %typeof arrguar = "Guar"; %typeof security = "Security"; +%typeof fielddef = "Field"; %goal unit; @@ -90,16 +101,38 @@ unit = defs.v locals.s {: return new Global(v, s); :} | defs.v GAMMA_0 COLON gamma_mappings.f rely.r guar.g locals.s {: return new Global(v, f, r, g, s); :}; +// TODO typing +ptrdef + = STAR ID.n {: return new VarDef(n, GlobalVar.instance()); :} + | STAR ptrdef.n {: return new VarDef(n.name().name(), GlobalVar.instance()); :} + ; + + + +fielddef + = FIELD COLON ID.i lpred.l {: return new Field(i, l); :} + ; +fielddefs + = fielddef + | fielddefs fielddef + ; + +vardef + = GLOBALVAR ID.n COLON lpred.l {: return new VarDef(n, l, GlobalVar.instance()); :} + | GLOBALVAR ID.n COLON {: return new VarDef(n, GlobalVar.instance()); :} + | LOCALVAR ID.n COLON {: return new VarDef(n, LocalVar.instance()); :} + | GLOBALVAR ptrdef.n COLON PT COLON id_list.p {: return new VarDef(n.name().name(), p, GlobalVar.instance()); :} // TODO + | GLOBALVAR ptrdef.n COLON lpred.l PT COLON id_list.p {: return new VarDef(n.name().name(), l, p, GlobalVar.instance()); :} // TODO + ; definition - = GLOBALVAR ID.n COLON lpred.l {: return new VarDef(n, l, GlobalVar.instance()); :} // TODO: does this make them appear as global (i.e. are vars without right permissions global) - | GLOBALVAR ID.n COLON {: return new VarDef(n, GlobalVar.instance()); :} - | LOCALVAR ID.n COLON {: return new VarDef(n, LocalVar.instance()); :} + = vardef | GLOBALARRAY ID.n LBRACK intexpr.s RBRACK COLON lpred.l arrrely.r arrguar.g {: return new ArrayDef(n, s, l, GlobalVar.instance(), r, g); :} | GLOBALARRAY ID.n LBRACK intexpr.s RBRACK COLON arrrely.r arrguar.g {: return new ArrayDef(n, s, GlobalVar.instance(), r, g); :} | LOCALARRAY ID.n LBRACK intexpr.s RBRACK COLON lpred.l arrrely.r arrguar.g {: return new ArrayDef(n, s, l, LocalVar.instance(), r, g); :} | LOCALARRAY ID.n LBRACK intexpr.s RBRACK COLON arrrely.r arrguar.g {: return new ArrayDef(n, s, LocalVar.instance(), r, g); :} + | GLOBALOBJ ID.n COLON fielddefs.f {: return new ObjDef(n, f, GlobalVar.instance()); :} ; arrrely = RELY COLON boolexpr.a {: return new Rely(a); :}; @@ -111,7 +144,11 @@ block = LBRACE locals.ss RBRACE {: return new Block("unprocessed", ss); :}; local = ID.n ASG intexpr.b SEMICOLON {: return new Assignment(n, b); :} // TODO boolexpr + | ID.n ASG ptrexpr.b SEMICOLON {: return new Assignment(n, b); :} | ID.n LBRACK intexpr.i RBRACK ASG intexpr.b SEMICOLON {: return new ArrayAssignment(n, i, b); :} + | ID.n DOT ID.f ASG intexpr.b SEMICOLON {: return new Assignment(new ObjIdAccess(n, f), b); :} + | ID.n DOT ID.f ASG ptrexpr.b SEMICOLON {: return new Assignment(new ObjIdAccess(n, f), b); :} + | STAR ID.n ASG intexpr.b SEMICOLON {: return new Assignment(new Dereference(n), b); :} | IF LPAREN boolexpr.a RPAREN block.b {: return new If(a, b); :} | IF LPAREN boolexpr.a RPAREN block.b ELSE block.c {: return new If(a, b, c); :} | WHILE LPAREN boolexpr.a RPAREN INVARIANT COLON boolexpr.i block.b {: return new While(a, i, b); :} @@ -125,52 +162,68 @@ local locals = local *; boolexpr - = PRIMEGAMMAID.n {: return new Id(n, Type.TBool(), true, true, false); :} - | GAMMAID.n {: return new Id(n, Type.TBool(), false, true, false); :} - // | PRIMEID.n {: return new Id(n, Type.TBool(), true, false, false); :} - // TODO | ID.n {: return new Id(n, Type.TBool(), false, false, false); :} + = PRIMEGAMMAID.n {: return new Id(n, TBool.instance(), true, true, false, false); :} + | GAMMAID.n {: return new Id(n, TBool.instance(), false, true, false, false); :} + // | PRIMEID.n {: return new Id(n, TBool.instance(), true, false, false, false); :} + // TODO | ID.n {: return new Id(n, TBool.instance(), false, false, false); :} // | PRIMEID.n LBRACK intexpr.i RBRACK {: return new IdAccess(n, true, false, i); :} | GAMMAID.n LBRACK intexpr.i RBRACK {: return new IdAccess(n, false, true, i); :} | PRIMEGAMMAID.n LBRACK intexpr.i RBRACK {: return new IdAccess(n, true, true, i); :} // | ID.n LBRACK intexpr.i RBRACK {: return new IdAccess(n, i); :} // | CAS LPAREN ID.x COMMA intexpr.y COMMA intexpr.z RPAREN {: return new CompareAndSwap(x, y, z); :} - | BANG boolexpr.a @ PREFIX {: return new PreOp("!", Type.TBool(), Type.TBool(), a); :} - | boolexpr.a IMPLIES boolexpr.b {: return new BinOp("=>", Type.TBool(), Type.TBool(), a, b); :} - | boolexpr.a EQ boolexpr.b {: return new BinOp("==", Type.TBool(), Type.TBool(),a, b); :} // TODO this is incorrect - | boolexpr.a NEQ boolexpr.b {: return new BinOp("!=", Type.TBool(), Type.TBool(),a, b); :} - | boolexpr.a AND boolexpr.b {: return new BinOp("&&", Type.TBool(), Type.TBool(),a, b); :} - | boolexpr.a OR boolexpr.b {: return new BinOp("||", Type.TBool(), Type.TBool(),a, b); :} - | intexpr.a LT intexpr.b {: return new BinOp("<", Type.TInt(), Type.TBool(), a, b); :} - | intexpr.a LE intexpr.b {: return new BinOp("<=",Type.TInt(), Type.TBool(),a, b); :} - | intexpr.a GE intexpr.b {: return new BinOp(">=",Type.TInt(), Type.TBool(),a, b); :} - | intexpr.a GT intexpr.b {: return new BinOp(">", Type.TInt(), Type.TBool(), a, b); :} - | intexpr.a EQ intexpr.b {: return new BinOp("==", Type.TInt(), Type.TBool(),a, b); :} - | intexpr.a NEQ intexpr.b {: return new BinOp("!=", Type.TInt(), Type.TBool(),a, b); :} + | DECLASSIFY LPAREN boolexpr.e COMMA boolexpr.b RPAREN {: return new Declassify(e, b); :} + | BANG boolexpr.a @ PREFIX {: return new PreOp("!", TBool.instance(), TBool.instance(), a); :} + | boolexpr.a IMPLIES boolexpr.b {: return new BinOp("=>", TBool.instance(), TBool.instance(), a, b); :} + | boolexpr.a EQ boolexpr.b {: return new BinOp("==", TBool.instance(), TBool.instance(),a, b); :} // TODO this is incorrect + | boolexpr.a NEQ boolexpr.b {: return new BinOp("!=", TBool.instance(), TBool.instance(),a, b); :} + | boolexpr.a AND boolexpr.b {: return new BinOp("&&", TBool.instance(), TBool.instance(),a, b); :} + | boolexpr.a OR boolexpr.b {: return new BinOp("||", TBool.instance(), TBool.instance(),a, b); :} + | intexpr.a LT intexpr.b {: return new BinOp("<", TInt.instance(), TBool.instance(), a, b); :} + | intexpr.a LE intexpr.b {: return new BinOp("<=",TInt.instance(), TBool.instance(),a, b); :} + | intexpr.a GE intexpr.b {: return new BinOp(">=",TInt.instance(), TBool.instance(),a, b); :} + | intexpr.a GT intexpr.b {: return new BinOp(">", TInt.instance(), TBool.instance(), a, b); :} + | intexpr.a EQ intexpr.b {: return new BinOp("==", TInt.instance(), TBool.instance(),a, b); :} + | intexpr.a NEQ intexpr.b {: return new BinOp("!=", TInt.instance(), TBool.instance(),a, b); :} // | FORALL LPAREN exprl.l COLON boolexpr.e RPAREN {: return new ForAll(l, e); :} + | ptrexpr.a EQ ptrexpr.b {: return new BinOp("==", new TPointer(TInt.instance()), TBool.instance(),a, b); :} + | ptrexpr.a NEQ ptrexpr.b {: return new BinOp("!=", new TPointer(TInt.instance()), TBool.instance(),a, b); :} | LPAREN boolexpr.e RPAREN {: return (Symbol) e; :} | TRUE {: return new Const("True"); :} | FALSE {: return new Const("False"); :} ; +intid + = PRIMEID.n {: return new Id(n, TInt.instance(), true, false, false, false); :} + | ID.n {: return new Id(n, TInt.instance(), false, false, false, false); :} + ; + intexpr = PREFIX | POSTFIX /* unused */ - | PRIMEID.n {: return new Id(n, Type.TInt(), true, false, false); :} - | ID.n {: return new Id(n, Type.TInt(), false, false, false); :} + | intid | PRIMEID.n LBRACK intexpr.i RBRACK {: return new IdAccess(n, true, false, i); :} | ID.n LBRACK intexpr.i RBRACK {: return new IdAccess(n, i); :} // TODO rm | CAS LPAREN ID.x COMMA intexpr.y COMMA intexpr.z RPAREN {: return new CompareAndSwap(x, y, z); :} + | CAS LPAREN ID.x COMMA intexpr.y COMMA ptrexpr.z RPAREN {: return new CompareAndSwap(x, y, z); :} + | DECLASSIFY LPAREN intexpr.e COMMA boolexpr.b RPAREN {: return new Declassify(e, b); :} | NUM.n {: return new Lit(n); :} - | PLUS intexpr.a @ PREFIX {: return new PreOp("+", Type.TInt(), Type.TInt(), a); :} - | MINUS intexpr.a @ PREFIX {: return new PreOp("-", Type.TInt(), Type.TInt(), a); :} - | intexpr.a STAR intexpr.b {: return new BinOp("*", Type.TInt(), Type.TInt(), a, b); :} - | intexpr.a DIV intexpr.b {: return new BinOp("/", Type.TInt(), Type.TInt(), a, b); :} - | intexpr.a PLUS intexpr.b {: return new BinOp("+", Type.TInt(), Type.TInt(), a, b); :} - | intexpr.a MINUS intexpr.b {: return new BinOp("-", Type.TInt(), Type.TInt(), a, b); :} - | intexpr.a MOD intexpr.b {: return new BinOp("%", Type.TInt(), Type.TInt(),a, b); :} + | PLUS intexpr.a @ PREFIX {: return new PreOp("+", TInt.instance(), TInt.instance(), a); :} + | MINUS intexpr.a @ PREFIX {: return new PreOp("-", TInt.instance(), TInt.instance(), a); :} + | intexpr.a STAR intexpr.b {: return new BinOp("*", TInt.instance(), TInt.instance(), a, b); :} + | intexpr.a DIV intexpr.b {: return new BinOp("/", TInt.instance(), TInt.instance(), a, b); :} + | intexpr.a PLUS intexpr.b {: return new BinOp("+", TInt.instance(), TInt.instance(), a, b); :} + | intexpr.a MINUS intexpr.b {: return new BinOp("-", TInt.instance(), TInt.instance(), a, b); :} + | intexpr.a MOD intexpr.b {: return new BinOp("%", TInt.instance(), TInt.instance(),a, b); :} | LPAREN intexpr.e RPAREN {: return (Symbol) e; :} + | STAR ID.n {: return new Dereference(n); :} + | intid.n DOT ID.f {: return new ObjIdAccess(n, f); :} ; +ptrexpr + // TODO = ID.n {: return new Id(n, new TPointer(TInt.instance()), false, false, false) :} + = AMP ID.n {: return new Reference(n); :} + ; + // for _L(x): pred construction to set predicate for variable security level lpred = LPRED COLON boolexpr.a {: return (Symbol) a; :}; @@ -192,3 +245,7 @@ security = LOW {: return Low.instance(); :} | HIGH {: return High.instance(); :} ; + +id_list + = ID + | id_list COMMA ID; diff --git a/wptool/src/wptool/Preprocess.scala b/wptool/src/wptool/Preprocess.scala index cfed0bd..a999683 100644 --- a/wptool/src/wptool/Preprocess.scala +++ b/wptool/src/wptool/Preprocess.scala @@ -57,18 +57,18 @@ object PreProcess { val right = ifStmt.right match { case Some(s) => exec(s, state, Block("if right", List(), List(currBlock))) - .prepend(Guard(PreOp("!", Type.TBool, Type.TBool, test))) + .prepend(Guard(PreOp("!", TBool, TBool, test))) case None => Block( "if empty", - List(Guard(PreOp("!", Type.TBool, Type.TBool, test))), + List(Guard(PreOp("!", TBool, TBool, test))), List(currBlock) ) } evalBlock(ifStmt.test, Block("pre if", List(), List(left, right))) case whileStmt: While => val after = - currBlock.prepend(Assume(PreOp("!", Type.TBool, Type.TBool, evalExp(whileStmt.test)))) + currBlock.prepend(Assume(PreOp("!", TBool, TBool, evalExp(whileStmt.test)))) // TODO why does the body not go to after ?? (as per paper/PASTE05) val body = Block("while body", List(Assert(whileStmt.invariant)), List()) @@ -85,11 +85,14 @@ object PreProcess { // Assert(branchGamma) head case doWhile: DoWhile => - val after = currBlock.prepend(Assume(PreOp("!", Type.TBool, Type.TBool, evalExp(doWhile.test)))) - val repeat = Block( - "do-while repeat", - List(Guard(doWhile.test), Assert(doWhile.invariant, true)), - List() + val after = currBlock.prepend(Assume(PreOp("!", TBool, TBool, evalExp(doWhile.test)))) + val repeat = evalBlock( + doWhile.test, + Block( + "do-while repeat", + List(Assert(doWhile.invariant, true)), + List() + ) ) val block = Block("do-while block", List(), List(after, repeat)) exec(doWhile.body, state, block) @@ -106,7 +109,7 @@ object PreProcess { val left = Block( "cas left", List( - Guard(BinOp("==", Type.TInt, Type.TBool, cas.x, cas.e1)), + Guard(BinOp("==", TInt, TBool, cas.x, cas.e1)), Assignment(cas.x, cas.e2), Assignment(Id.tmpId, Lit(1)) ), @@ -116,7 +119,7 @@ object PreProcess { val right = Block( "cas right", List( - Guard(BinOp("!=", Type.TInt, Type.TBool, cas.x, cas.e1)), + Guard(BinOp("!=", TInt, TBool, cas.x, cas.e1)), Assignment(Id.tmpId, Lit(0)) ), List(currBlock), diff --git a/wptool/src/wptool/SMT.scala b/wptool/src/wptool/SMT.scala index 6f195aa..233e356 100644 --- a/wptool/src/wptool/SMT.scala +++ b/wptool/src/wptool/SMT.scala @@ -25,13 +25,16 @@ object SMT { simplify: Boolean, expectIds: Boolean = false ) = { - if (debug) + if (debug) { println("smt checking !(" + cond + ")") + println("translated as " + formula(PreOp("!", TBool, TBool, cond), expectIds)) + } + solver.push() val res = try { // check that (NOT cond) AND P is unsatisfiable - solver.add(formula(PreOp("!", Type.TBool, Type.TBool, cond), expectIds)) + solver.add(formula(PreOp("!", TBool, TBool, cond), expectIds)) solver.check } catch { @@ -47,7 +50,7 @@ object SMT { "incorrect z3 expression type, probably involving ForAll/Exists" ) case e: Throwable => - // throw error.Z3Error("Z3 failed", cond, given.PStr, e) + // throw error.Z3Error("Z3 failed", cond, e) throw e } finally { solver.pop() @@ -60,6 +63,7 @@ object SMT { println(res) if (res == z3.Status.SATISFIABLE) { val model = solver.getModel + println(s"COND VARS: ${cond}") println( "Model: [" + cond.vars.toList .sortWith((x, y) => x.toString < y.toString) @@ -97,34 +101,33 @@ object SMT { throw error.InvalidProgram("not a bitwise expression", prop, e) } - def getArray(store: Expression): z3.ArrayExpr = store match { - case a: VarAccess => - ctx.mkArrayConst( - a.name.toString, - ctx.getIntSort, - if (a.ident.gamma) ctx.getBoolSort else ctx.getIntSort - ) - case a: VarStore => getArray(a.array) - case _ => throw new Error("Unexpected statement in VarStore") + def handleSelect( + store: Expression, + arr: z3.ArrayExpr, + expectIds: Boolean + ): z3.Expr = store match { + case a: VarAccess => ctx.mkSelect(arr, translate(a.index, expectIds)) + case a: VarStore => handleSelect(a.array, arr, expectIds) + case _ => throw new Error("Unexpected statement in VarStore") } // TODO i think the name should come from the inner load not from the store def handleStore( store: Expression, - arr: z3.ArrayExpr, expectIds: Boolean - ): z3.Expr = store match { - case a: VarAccess => ctx.mkSelect(arr, translate(a.index, expectIds)) + ): z3.ArrayExpr = store match { + case a: VarAccess => + ctx.mkArrayConst( + a.name.toString, + ctx.getIntSort, + if (a.ident.gamma) ctx.getBoolSort else ctx.getIntSort + ) case a: VarStore => - handleStore( - a.array, - ctx.mkStore( - arr, - translate(a.index, expectIds), - // TODO Type? - translate(a.exp, expectIds) - ), - expectIds + ctx.mkStore( + handleStore(a.array, expectIds), + translate(a.index, expectIds), + // TODO Type? + translate(a.exp, expectIds) ) case _ => throw new Error("Unexpected statement in VarStore") } @@ -142,11 +145,11 @@ object SMT { case x: Var => if (expectIds) throw new Error("Program ids should not be resolved") // TODO println(s"$x is of type ${typeOf}") - val sort = if (x.ident.expType == Type.TBool) ctx.getBoolSort else ctx.getIntSort + val sort = if (x.ident.expType == TBool) ctx.getBoolSort else ctx.getIntSort ctx.mkConst(x.toString, sort) case x: Id => if (expectIds) throw new Error("Unresolved id") - val sort = if (x.expType == Type.TBool) ctx.getBoolSort else ctx.getIntSort + val sort = if (x.expType == TBool) ctx.getBoolSort else ctx.getIntSort ctx.mkConst(x.toString, sort) // TODO can these cases be merged together @@ -168,9 +171,12 @@ object SMT { ) case store: VarStore => - handleStore( + handleSelect( store, - getArray(store), + handleStore( + store, + expectIds + ), expectIds ) @@ -186,41 +192,41 @@ object SMT { else throw new Error("ArrayConstDefault is only for gamma values") */ - case BinOp("==", _, Type.TBool, arg1, arg2) => + case BinOp("==", _, TBool, arg1, arg2) => ctx.mkEq(translate(arg1, expectIds), translate(arg2, expectIds)) - case BinOp("!=", _, Type.TBool, arg1, arg2) => + case BinOp("!=", _, TBool, arg1, arg2) => ctx.mkNot( ctx.mkEq(translate(arg1, expectIds), translate(arg2, expectIds)) ) - case PreOp("!", Type.TBool, Type.TBool, arg) => ctx.mkNot(formula(arg, expectIds)) - case BinOp("&&", Type.TBool, Type.TBool, arg1, arg2) => + case PreOp("!", TBool, TBool, arg) => ctx.mkNot(formula(arg, expectIds)) + case BinOp("&&", TBool, TBool, arg1, arg2) => ctx.mkAnd(formula(arg1, expectIds), formula(arg2, expectIds)) - case BinOp("||", Type.TBool, Type.TBool, arg1, arg2) => + case BinOp("||", TBool, TBool, arg1, arg2) => ctx.mkOr(formula(arg1, expectIds), formula(arg2, expectIds)) - case BinOp("=>", Type.TBool, Type.TBool, arg1, arg2) => + case BinOp("=>", TBool, TBool, arg1, arg2) => ctx.mkImplies(formula(arg1, expectIds), formula(arg2, expectIds)) - case PreOp("-", Type.TInt, Type.TInt, arg) => ctx.mkUnaryMinus(arith(arg)) - case BinOp("+", Type.TInt, Type.TInt, arg1, arg2) => + case PreOp("-", TInt, TInt, arg) => ctx.mkUnaryMinus(arith(arg)) + case BinOp("+", TInt, TInt, arg1, arg2) => ctx.mkAdd(arith(arg1, expectIds), arith(arg2, expectIds)) - case BinOp("-", Type.TInt, Type.TInt, arg1, arg2) => + case BinOp("-", TInt, TInt, arg1, arg2) => ctx.mkSub(arith(arg1, expectIds), arith(arg2, expectIds)) - case BinOp("*", Type.TInt, Type.TInt, arg1, arg2) => + case BinOp("*", TInt, TInt, arg1, arg2) => ctx.mkMul(arith(arg1, expectIds), arith(arg2, expectIds)) - case BinOp("/", Type.TInt, Type.TInt, arg1, arg2) => + case BinOp("/", TInt, TInt, arg1, arg2) => ctx.mkDiv(arith(arg1, expectIds), arith(arg2, expectIds)) - case BinOp("%", Type.TInt, Type.TInt, arg1, arg2) => + case BinOp("%", TInt, TInt, arg1, arg2) => ctx.mkMod(arith(arg1, expectIds), arith(arg2, expectIds)) - case BinOp("<=", Type.TInt, Type.TBool, arg1, arg2) => + case BinOp("<=", TInt, TBool, arg1, arg2) => ctx.mkLe(arith(arg1, expectIds), arith(arg2, expectIds)) - case BinOp("<", Type.TInt, Type.TBool, arg1, arg2) => + case BinOp("<", TInt, TBool, arg1, arg2) => ctx.mkLt(arith(arg1, expectIds), arith(arg2, expectIds)) - case BinOp(">=", Type.TInt, Type.TBool, arg1, arg2) => + case BinOp(">=", TInt, TBool, arg1, arg2) => ctx.mkGe(arith(arg1, expectIds), arith(arg2, expectIds)) - case BinOp(">", Type.TInt, Type.TBool, arg1, arg2) => + case BinOp(">", TInt, TBool, arg1, arg2) => ctx.mkGt(arith(arg1, expectIds), arith(arg2, expectIds)) /* diff --git a/wptool/src/wptool/SMT_.scala b/wptool/src/wptool/SMT_.scala index 9939ebc..dcfd968 100644 --- a/wptool/src/wptool/SMT_.scala +++ b/wptool/src/wptool/SMT_.scala @@ -5,8 +5,10 @@ import org.sosy_lab.java_smt.SolverContextFactory._ import org.sosy_lab.java_smt.api.FormulaType import scala.reflect.runtime.universe.{TypeTag, typeOf} import org.sosy_lab.java_smt.api.SolverContext.ProverOptions +import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType object SMT_ { + type array = api.ArrayFormula[api.NumeralFormula.IntegerFormula, _ <: api.Formula] val solver = Solvers.CVC4 val ctx = SolverContextFactory.createSolverContext(solver) val fmgr = ctx.getFormulaManager(); @@ -29,7 +31,7 @@ object SMT_ { val res = try { // check that (NOT cond) AND P is unsatisfiable - prover.addConstraint(translateBool(PreOp("!", Type.TBool, Type.TBool, cond), expectIds)) + prover.addConstraint(translateBool(PreOp("!", TBool, TBool, cond), expectIds)) return prover.isUnsat(); @@ -78,20 +80,9 @@ object SMT_ { } } - def makeSelect( - id: String, - index: Expression, - isBool: Boolean, - expectIds: Boolean - ) = - amgr.select( - makeArray(id, isBool).asInstanceOf[api.ArrayFormula[api.Formula, _ <: api.Formula]], - translateInt(index, expectIds) - ) - def getArray(store: Expression): api.ArrayFormula[api.NumeralFormula.IntegerFormula, _ <: api.Formula] = store match { case a: VarAccess => - if (a.expType == Type.TBool) { + if (a.expType == TBool) { amgr.makeArray[api.NumeralFormula.IntegerFormula, api.BooleanFormula, api.FormulaType[ api.NumeralFormula.IntegerFormula ], api.FormulaType[api.BooleanFormula]]( @@ -112,70 +103,97 @@ object SMT_ { case _ => throw new Error("Unexpected statement in VarStore") } - def handleStore( + def makeSelect( + id: String, + index: Expression, + isBool: Boolean, + expectIds: Boolean + ): api.Formula = { + amgr + .select( + makeArray(id, isBool).asInstanceOf[array], + translateInt(index, expectIds) + ) + } + + def handleSelect( store: Expression, - arr: api.ArrayFormula[api.NumeralFormula.IntegerFormula, _ <: api.Formula], + arr: array, expectIds: Boolean - ): api.Formula = store match { // TODO type - case a: VarAccess => amgr.select(arr, translateInt(a.index, expectIds)) - case a: VarStore => - handleStore( - a.array, + ): api.Formula = store match { + case a: VarAccess => makeSelect(a.ident.toString, a.index, a.expType == TBool, expectIds) + case a: VarStore => handleSelect(a.array, arr, expectIds) + case _ => throw new Error("Unexpected statement in VarStore") + } + + def handleStore( + store: Expression, + expectIds: Boolean, + arrType: Type + ): array = { + store match { + case a: VarAccess => + makeArray(a.ident.toString, a.ident.expType == TBool) + .asInstanceOf[array] + case a: VarStore => + if (a.expType != arrType) throw new Error(s"Actual (${a.expType}) and expect (${arrType}) array type do not match for $a") amgr.store( - arr.asInstanceOf[api.ArrayFormula[api.NumeralFormula.IntegerFormula, api.Formula]], // TODO + handleStore(a.array, expectIds, arrType).asInstanceOf[api.ArrayFormula[api.NumeralFormula.IntegerFormula, api.Formula]], translateInt(a.index, expectIds), - // TODO Type? - // TODO !!!!!!!! - if (a.expType == Type.TInt) translateInt(a.exp, expectIds) else translateBool(a.exp, expectIds) - ), - expectIds - ) - case _ => throw new Error("Unexpected statement in VarStore") + a.expType match { + case TInt => translateInt(a.exp, expectIds) + case TBool => translateBool(a.exp, expectIds) + case _ => throw new Error("Unexpected type") + } + ) + case _ => throw new Error("Unexpected statement in VarStore") + } } def translateBool(prop: Expression, expectIds: Boolean): api.BooleanFormula = prop match { case Const._true => bmgr.makeTrue case Const._false => bmgr.makeFalse - case BinOp("==", Type.TBool, Type.TBool, arg1, arg2) => + case BinOp("==", TBool, TBool, arg1, arg2) => bmgr.equivalence(translateBool(arg1, expectIds), translateBool(arg2, expectIds)) - case BinOp("!=", Type.TBool, Type.TBool, arg1, arg2) => + case BinOp("!=", TBool, TBool, arg1, arg2) => bmgr.not( bmgr.equivalence(translateBool(arg1, expectIds), translateBool(arg2, expectIds)) ) - case PreOp("!", Type.TBool, Type.TBool, arg) => bmgr.not(translateBool(arg, expectIds)) - case BinOp("&&", Type.TBool, Type.TBool, arg1, arg2) => + case PreOp("!", TBool, TBool, arg) => bmgr.not(translateBool(arg, expectIds)) + case BinOp("&&", TBool, TBool, arg1, arg2) => bmgr.and(translateBool(arg1, expectIds), translateBool(arg2, expectIds)) - case BinOp("||", Type.TBool, Type.TBool, arg1, arg2) => + case BinOp("||", TBool, TBool, arg1, arg2) => bmgr.or(translateBool(arg1, expectIds), translateBool(arg2, expectIds)) - case BinOp("=>", Type.TBool, Type.TBool, arg1, arg2) => + case BinOp("=>", TBool, TBool, arg1, arg2) => bmgr.implication(translateBool(arg1, expectIds), translateBool(arg2, expectIds)) - case BinOp("==", Type.TInt, Type.TBool, arg1, arg2) => + case BinOp("==", TInt, TBool, arg1, arg2) => imgr.equal(translateInt(arg1, expectIds), translateInt(arg2, expectIds)) - case BinOp("!=", Type.TInt, Type.TBool, arg1, arg2) => + case BinOp("!=", TInt, TBool, arg1, arg2) => bmgr.not( imgr.equal(translateInt(arg1, expectIds), translateInt(arg2, expectIds)) ) - case BinOp("<=", Type.TInt, Type.TBool, arg1, arg2) => + case BinOp("<=", TInt, TBool, arg1, arg2) => imgr.lessOrEquals(translateInt(arg1, expectIds), translateInt(arg2, expectIds)) - case BinOp("<", Type.TInt, Type.TBool, arg1, arg2) => + case BinOp("<", TInt, TBool, arg1, arg2) => imgr.lessThan(translateInt(arg1, expectIds), translateInt(arg2, expectIds)) - case BinOp(">=", Type.TInt, Type.TBool, arg1, arg2) => + case BinOp(">=", TInt, TBool, arg1, arg2) => imgr.greaterOrEquals(translateInt(arg1, expectIds), translateInt(arg2, expectIds)) - case BinOp(">", Type.TInt, Type.TBool, arg1, arg2) => + case BinOp(">", TInt, TBool, arg1, arg2) => imgr.greaterThan(translateInt(arg1, expectIds), translateInt(arg2, expectIds)) - case v @ Var(Id(_, Type.TBool, _, _, _), _, _) if (!expectIds) => bmgr.makeVariable(v.toString) - case v @ Id(_, Type.TBool, _, _, _) if (expectIds) => bmgr.makeVariable(v.toString) + case v @ Var(Id(_, TBool, _, _, _, _), _, _) if (!expectIds) => bmgr.makeVariable(v.toString) + case v @ Id(_, TBool, _, _, _, _) if (expectIds) => bmgr.makeVariable(v.toString) // TODO refactor to use Type not bool for isBoolean - case x: VarAccess if (!expectIds && x.expType == Type.TBool) => + case x: VarAccess if (!expectIds && x.expType == TBool) => makeSelect(x.name.toString, x.index, true, expectIds).asInstanceOf[api.BooleanFormula] - case x: IdAccess if (expectIds && x.expType == Type.TBool) => + case x: IdAccess if (expectIds && x.expType == TBool) => makeSelect(x.ident.toString, x.index, true, expectIds).asInstanceOf[api.BooleanFormula] - case store: VarStore => handleStore(store, getArray(store), expectIds).asInstanceOf[api.BooleanFormula] + case store: VarStore => + handleSelect(store.array, handleStore(store, expectIds, TBool), expectIds).asInstanceOf[api.BooleanFormula] case _ => throw new Error(s"Unexpected boolean expression $prop") } @@ -184,29 +202,31 @@ object SMT_ { case Lit(n: Int) => imgr.makeNumber(n) case Var(Id.indexId, _, _) => throw new Error("Unsubstituted index") - case BinOp("%", Type.TInt, Type.TInt, arg1, arg2) => + case BinOp("%", TInt, TInt, arg1, arg2) => imgr.modulo(translateInt(arg1, expectIds), translateInt(arg2, expectIds)) - case BinOp("+", Type.TInt, Type.TInt, arg1, arg2) => + case BinOp("+", TInt, TInt, arg1, arg2) => imgr.add(translateInt(arg1, expectIds), translateInt(arg2, expectIds)) - case BinOp("-", Type.TInt, Type.TInt, arg1, arg2) => + case BinOp("-", TInt, TInt, arg1, arg2) => imgr.subtract(translateInt(arg1, expectIds), translateInt(arg2, expectIds)) - case BinOp("*", Type.TInt, Type.TInt, arg1, arg2) => + case BinOp("*", TInt, TInt, arg1, arg2) => imgr.multiply(translateInt(arg1, expectIds), translateInt(arg2, expectIds)) - case BinOp("/", Type.TInt, Type.TInt, arg1, arg2) => + case BinOp("/", TInt, TInt, arg1, arg2) => imgr.divide(translateInt(arg1, expectIds), translateInt(arg2, expectIds)) - case PreOp("-", Type.TInt, Type.TInt, arg) => imgr.negate(translateInt(arg, expectIds)) - case PreOp("+", Type.TInt, Type.TInt, arg) => translateInt(arg, expectIds) + case PreOp("-", TInt, TInt, arg) => imgr.negate(translateInt(arg, expectIds)) + case PreOp("+", TInt, TInt, arg) => translateInt(arg, expectIds) // TODO *+-/ - case v @ Var(Id(_, Type.TInt, _, gamma, _), _, _) if (!expectIds && !gamma) => imgr.makeVariable(v.toString) - case v @ Id(_, Type.TInt, _, gamma, _) if (expectIds && !gamma) => imgr.makeVariable(v.toString) - case x: VarAccess if (!expectIds && x.expType == Type.TInt) => + case v @ Var(Id(_, TInt, _, gamma, _, _), _, _) if (!expectIds && !gamma) => imgr.makeVariable(v.toString) + case v @ Id(_, TInt, _, gamma, _, _) if (expectIds && !gamma) => imgr.makeVariable(v.toString) + // TODO maybe this is the wrong type? + case x: VarAccess if (!expectIds && x.expType == TInt) => makeSelect(x.name.toString, x.index, false, expectIds).asInstanceOf[api.NumeralFormula.IntegerFormula] - case x: IdAccess if (expectIds && x.expType == Type.TInt) => + case x: IdAccess if (expectIds && x.expType == TInt) => makeSelect(x.ident.toString, x.index, false, expectIds).asInstanceOf[api.NumeralFormula.IntegerFormula] - case store: VarStore => handleStore(store, getArray(store), expectIds).asInstanceOf[api.NumeralFormula.IntegerFormula] + case store: VarStore => + handleSelect(store.array, handleStore(store, expectIds, TInt), expectIds).asInstanceOf[api.NumeralFormula.IntegerFormula] /* diff --git a/wptool/src/wptool/Scanner.flex b/wptool/src/wptool/Scanner.flex index 22e9de5..56eabe9 100644 --- a/wptool/src/wptool/Scanner.flex +++ b/wptool/src/wptool/Scanner.flex @@ -63,7 +63,7 @@ WS = {NL} | [ \t\f] "}" { return newToken(Terminals.RBRACE); } //"++" { return newToken(Terminals.INCR); } //"--" { return newToken(Terminals.DECR); } -//"." { return newToken(Terminals.DOT); } +"." { return newToken(Terminals.DOT); } "!" { return newToken(Terminals.BANG); } "=>" { return newToken(Terminals.IMPLIES); } // "~" { return newToken(Terminals.TILDE); } @@ -82,7 +82,7 @@ WS = {NL} | [ \t\f] ">" { return newToken(Terminals.GT); } "==" { return newToken(Terminals.EQ); } "!=" { return newToken(Terminals.NEQ); } -// "&" { return newToken(Terminals.AMP); } +"&" { return newToken(Terminals.AMP); } // "^" { return newToken(Terminals.CARET); } // "|" { return newToken(Terminals.PIPE); } "&&" { return newToken(Terminals.AND); } @@ -95,6 +95,7 @@ WS = {NL} | [ \t\f] ";" { return newToken(Terminals.SEMICOLON);} "CAS" { return newToken(Terminals.CAS); } +"d" { return newToken(Terminals.DECLASSIFY); } //"break" { return newToken(Terminals.BREAK); } //"return" { return newToken(Terminals.RETURN); } @@ -109,6 +110,7 @@ WS = {NL} | [ \t\f] //"fence" { return newToken(Terminals.FENCE); } //"cfence" { return newToken(Terminals.CFENCE); } "_L" { return newToken(Terminals.LPRED); } +"_PT" { return newToken(Terminals.PT); } "_invariant" {return newToken(Terminals.INVARIANT);} "_Gamma" {return newToken(Terminals.GAMMA);} "_Gamma_0" {return newToken(Terminals.GAMMA_0);} @@ -117,7 +119,9 @@ WS = {NL} | [ \t\f] "_Rely" {return newToken(Terminals.RELY);} "_Guar" {return newToken(Terminals.GUAR);} "global array" { return newToken(Terminals.GLOBALARRAY); } -"local array" { return newToken(Terminals.GLOBALARRAY); } +"local array" { return newToken(Terminals.LOCALARRAY); } +"global obj" { return newToken(Terminals.GLOBALOBJ); } +"_Field" { return newToken(Terminals.FIELD); } "TRUE" { return newToken(Terminals.TRUE); } "FALSE" { return newToken(Terminals.FALSE); } diff --git a/wptool/src/wptool/State.scala b/wptool/src/wptool/State.scala index 61024b9..641f688 100644 --- a/wptool/src/wptool/State.scala +++ b/wptool/src/wptool/State.scala @@ -9,10 +9,10 @@ case class State( debug: Boolean, silent: Boolean, simplify: Boolean, - controls: Set[Id], - controlled: Set[Id], - controlledBy: Map[Id, Set[Id]], // TODO check - L: Map[Id, Expression], + controls: Set[Identifier], + controlled: Set[Identifier], + controlledBy: Map[Identifier, Set[Identifier]], // TODO check + L: Map[Identifier, Expression], ids: Set[Id], arrayIds: Set[Id], globals: Set[Id], @@ -21,6 +21,9 @@ case class State( arrRelys: Map[Id, Expression], arrGuars: Map[Id, Expression], indicies: Map[Id, Int], + addrs: Map[Id, Expression], + fieldIndicies: Map[ObjIdAccess, Int], + pointsTo: Map[Id, Set[Id]], error: Boolean = false ) { def incPrimeIndicies = @@ -30,8 +33,7 @@ case class State( .map(x => (x._1, x._2 + 1)) .toMap ) - def incGamma(id: Id) = - this.copy(indicies = indicies + (id -> (indicies.getOrElse(id, -1) + 1))) + def incGamma(id: Id) = this.copy(indicies = indicies + (id -> (indicies.getOrElse(id, throw new Error("index not found")) + 1))) def addQs(Qss: PredInfo*) = this.copy(Qs = Qs ::: Qss.toList) def addQs(Qss: List[PredInfo]) = this.copy(Qs = Qs ::: Qss) } @@ -46,14 +48,24 @@ object State { rely: Option[Rely], guar: Option[Guar] ): State = { - var controls: Set[Id] = Set() - var controlled: Set[Id] = Set() - var controlledBy: Map[Id, Set[Id]] = Map() + var controls: Set[Identifier] = Set() + var controlled: Set[Identifier] = Set() + var controlledBy: Map[Identifier, Set[Identifier]] = Map() - val arrayIds = definitions collect { case a: ArrayDef => - a.toVarDefs.name + val arrayIds = { + definitions collect { case a: ArrayDef => + a.toVarDefs.name + } + } + Id.memId + + val objDefs = { + definitions collect { case a: ObjDef => + a + } } + val objVarDefs = objDefs.map(o => o.toVarDefs) + val arrRelys = definitions .collect { case a: ArrayDef => a.toVarDefs.name -> a.rely.exp @@ -66,15 +78,18 @@ object State { } .toMap[Id, Expression] + // TODO when adding in typing will need to modify code below val variables: Set[VarDef] = definitions map { case a: ArrayDef => a.toVarDefs case v: VarDef => v + case v: ObjDef => v.toVarDefs + case _ => throw new Error("Unexected def: TODO objects") } val ids: Set[Id] = { for (v <- variables) yield v.name } for (v <- variables) { - val controlling: Set[Id] = v.pred.ids + val controlling: Set[Identifier] = v.pred.ids if (controlling.nonEmpty) { controlled += v.name @@ -88,6 +103,12 @@ object State { } } + val pointsTo = variables + .map(v => { + v.name -> (v.pointsTo.toSet + v.name) + }) + .toMap + val controlAndControlled = controls & controlled if (controlAndControlled.nonEmpty) { throw error.InvalidProgram( @@ -97,12 +118,15 @@ object State { } // init L - map variables to their L predicates - val L: Map[Id, Expression] = { - for (v <- variables) yield { + val L: Map[Identifier, Expression] = { + for (v <- (variables)) yield { if (v.access == GlobalVar) v.name -> v.pred else v.name -> Const._false } - }.toMap + }.toMap[Identifier, Expression] ++ objDefs + .map(o => o.fields.map(f => ObjIdAccess(o.name, f.ident) -> f.lpred)) + .flatten + .toMap[Identifier, Expression] val globals = variables.filter(v => v.access == GlobalVar).map(v => v.name) val locals = variables.filter(v => v.access == LocalVar).map(v => v.name) @@ -116,10 +140,17 @@ object State { val _guar = guar.getOrElse(Guar(Const._true)).exp val _rely = rely.getOrElse(Rely(Const._true)).exp - val primeIndicies = - ((ids ++ arrayIds).map(x => x.toPrime -> 0) ++ (ids ++ arrayIds).map(x => - x -> 0 - )).toMap + (Id.indexId -> 0) + (Id.tmpId -> 0) + (Id.tmpId.toPrime -> 0) + // TODO rm ids + val indicies = + ((ids ++ arrayIds).map(x => x.toPrime -> 0) ++ (ids ++ arrayIds).map(x => x -> 0)).toMap + + (Id.indexId -> 0) + (Id.tmpId -> 0) + (Id.tmpId.toPrime -> 0) + (Id.memId -> 0) + (Id.memId.toPrime -> 0) + + // TODO add support for arrays + // TODO tmpId could remain a var as it cant be aliased + val addrs = (ids + Id.tmpId).zipWithIndex.map { case (x, i) => (x -> x.copy(memLoc = true)) }.toMap + + val fieldIndicies = + objDefs.map(o => o.fields.zipWithIndex.map { case (f, i) => ObjIdAccess(o.name, f.ident.toString) -> i }).flatten.toMap // TODO malformed probs insto the best State( @@ -138,7 +169,10 @@ object State { _guar, arrRelys, arrGuars, - primeIndicies + indicies, + addrs, + fieldIndicies, + pointsTo ) } } diff --git a/wptool/src/wptool/Statement.scala b/wptool/src/wptool/Statement.scala index c413ffd..7d6a748 100644 --- a/wptool/src/wptool/Statement.scala +++ b/wptool/src/wptool/Statement.scala @@ -61,9 +61,11 @@ object Block { } -case class Assignment(lhs: Id, expression: Expression, line: (String, Int)) extends Stmt(line) { +case class Assignment(lhs: Expression, expression: Expression, line: (String, Int)) extends Stmt(line) { def this(lhs: String, expression: Expression) = - this(new Id(lhs, Type.TInt, false, false, false), expression, ("", -1)) + this(new Id(lhs, TInt, false, false, false, false), expression, ("", -1)) + def this(lhs: Expression, expression: Expression) = + this(lhs, expression, ("", -1)) override def toString: String = lhs + " = " + expression def incLine = this.copy(line = line.copy(_2 = line._2 + 1)) @@ -76,7 +78,7 @@ object Assignment { case class ArrayAssignment(lhs: IdAccess, expression: Expression, line: (String, Int)) extends Stmt(line) { def this(name: String, index: Expression, expression: Expression) = - this(new IdAccess(new Id(name, Type.TInt, false, false, false), index), expression, ("", -1)) + this(new IdAccess(new Id(name, TInt, false, false, false, false), index), expression, ("", -1)) override def toString: String = lhs.ident + "[" + lhs.index + "]" + " = " + expression @@ -187,7 +189,7 @@ case class Assume(expression: Expression, line: (String, Int)) extends Stmt(line def incLine = this.copy(line = line.copy(_2 = line._2 + 1)) def setLine(line: (String, Int)) = this.copy(line = line) - override def toString = s"assume ${expression.toString})" + override def toString = s"assume ${expression.toString}" } object Assume { @@ -208,6 +210,7 @@ object Assert { case class Havoc(line: (String, Int)) extends Stmt(line) { def incLine = this.copy(line = line.copy(_2 = line._2 + 1)) def setLine(line: (String, Int)) = this.copy(line = line) + override def toString = "Havoc" } object Havoc { diff --git a/wptool/src/wptool/VarDef.scala b/wptool/src/wptool/VarDef.scala index 2f75607..0347456 100644 --- a/wptool/src/wptool/VarDef.scala +++ b/wptool/src/wptool/VarDef.scala @@ -77,9 +77,9 @@ case object Low extends Security { case class GammaMapping(variable: Id, security: Security) extends beaver.Symbol { // TODO hmmmmmm def this(variable: String, index: Int, security: Security) = - this(new Id(variable + "[" + index + "]", Type.TInt, false, false, false), security) + this(new Id(variable + "[" + index + "]", TInt, false, false, false, false), security) def this(variable: String, security: Security) = - this(new Id(variable, Type.TInt, false, false, false), security) + this(new Id(variable, TInt, false, false, false, false), security) def toPair: Seq[(Id, Security)] = this match { case g => @@ -92,11 +92,20 @@ case class Guar(exp: Expression) extends beaver.Symbol sealed trait Definition extends beaver.Symbol -case class VarDef(name: Id, pred: Expression, access: Access) extends Definition { +case class VarDef(name: Id, pred: Expression, pointsTo: List[Id], access: Access) extends Definition { def this(name: String, pred: Expression, access: Access) = - this(new Id(name, Type.TInt, false, false, false), pred, access) + this(new Id(name, TInt, false, false, false, false), pred, List(), access) + def this(name: String, pred: Expression, pointsTo: Array[String], access: Access) = + this(new Id(name, TInt, false, false, false, false), pred, pointsTo.toList.map(v => Id(v, TInt, false, false, false, false)), access) def this(name: String, access: Access) = - this(new Id(name, Type.TInt, false, false, false), Const._true, access) + this(new Id(name, TInt, false, false, false, false), Const._true, List(), access) + def this(name: String, pointsTo: Array[String], access: Access) = + this( + new Id(name, TInt, false, false, false, false), + Const._true, + pointsTo.toList.map(v => Id(v, TInt, false, false, false, false)), + access + ) } case class ArrayDef( @@ -116,7 +125,7 @@ case class ArrayDef( guar: Guar ) = this( - new Id(name, Type.TInt, false, false, false), + new Id(name, TInt, false, false, false, false), size, pred, access, @@ -131,7 +140,7 @@ case class ArrayDef( guar: Guar ) = this( - new Id(name, Type.TInt, false, false, false), + new Id(name, TInt, false, false, false, false), size, Const._true, access, @@ -139,7 +148,7 @@ case class ArrayDef( guar: Guar ) - def toVarDefs: VarDef = VarDef(name, pred, access) + def toVarDefs: VarDef = VarDef(name, pred, List(), access) } object ArrayDef { @@ -148,3 +157,25 @@ object ArrayDef { yield lpred } } + +// TODO L!!! +case class ObjDef( + name: Id, + fields: List[Field], + access: Access +) extends Definition { + def this( + name: String, + fields: Array[Field], + access: Access + ) = + this( + Id(name, TInt, false, false, false, false), + fields.toList, + access + ) + + def toVarDefs: VarDef = VarDef(name, Const._true, List(), access) +} + +case class Field(ident: String, lpred: Expression) extends beaver.Symbol {} diff --git a/wptool/src/wptool/WPTool.scala b/wptool/src/wptool/WPTool.scala index 5e618df..7607a3f 100644 --- a/wptool/src/wptool/WPTool.scala +++ b/wptool/src/wptool/WPTool.scala @@ -105,6 +105,7 @@ object WPTool { // printBlocks(PreProcess.process(statements, state)) if (debug) PreProcess.printGraphvis(PreProcess.process(statements, state)) + if (debug) println(s"Addrs: ${state.addrs}") val _state = Exec.exec(PreProcess.process(statements, state), state) @@ -143,15 +144,18 @@ object WPTool { val gammaSubstr = { for (i <- gammaDom) yield { + // i.toGamma.toVar(_state) -> Left(gamma.getOrElse(i, High).toTruth) + // TODO TO TRUTH + // TODO Low?? i.toGamma.toVar(_state) -> Left(gamma.getOrElse(i, High).toTruth) } - }.toMap.toMap[Var, Left[Expression, Nothing]] ++ Map(Id.tmpId.toGamma.toVar(_state) -> Left(Const._true)) + }.toMap[Expression, Left[Expression, Nothing]] ++ Map(Id.tmpId.toGamma.toVar(_state) -> Left(Const._true)) if (debug) println("Gamma0: " + gammaSubstr) if (debug) println("L: " + _state.L) if (debug) println("Indicies: " + _state.indicies) - checkVcs(_state.Qs, gammaSubstr, debug, simplify) match { + checkVcs(_state.Qs, (gammaSubstr, state), debug, simplify, state) match { case Some(s) => if (!silent) printFalseVcs(s) false diff --git a/wptool/src/wptool/package.scala b/wptool/src/wptool/package.scala index 8cc3368..6b22e1b 100644 --- a/wptool/src/wptool/package.scala +++ b/wptool/src/wptool/package.scala @@ -12,9 +12,7 @@ package object wptool { case class Z3Error(info: Any*) extends Error } - // TODO this doesnt feel like the best way to do this - // Either[substitution, (index, substitution)] - type Subst = Map[Var, Either[Expression, (Expression, Expression)]] + type Subst = (Map[Expression, Either[Expression, (Expression, Expression)]], State) val sub = "₀₁₂₃₄₅₆₇₈₉" implicit class StringOps(self: String) { @@ -71,11 +69,18 @@ package object wptool { def checkVcs( preds: List[PredInfo], debug: Boolean, - simplify: Boolean + simplify: Boolean, + state: State ): Option[List[PredInfo]] = preds.filter(p => { + val disjoint = constructForall((for { + (x, idxX) <- state.ids.zipWithIndex + (y, idxY) <- state.ids.zipWithIndex + if idxX < idxY + } yield BinOp("!=", TInt, TBool, x, y)).toList) + val _p = BinOp("=>", TBool, TBool, disjoint, p.pred) if (debug) println(s"passing ${p.stmt.toStringWLine} ${p.label} along path ${p.path.mkString(", ")} to SMT") - !SMT.prove(p.pred, debug, simplify) + !SMT.prove(_p, debug, simplify) }) match { case List() => None case l => Some(l) @@ -85,16 +90,19 @@ package object wptool { preds: List[PredInfo], gammas: Subst, debug: Boolean, - simplify: Boolean + simplify: Boolean, + state: State ): Option[List[PredInfo]] = checkVcs( preds.map(p => { p.copy(pred = p.pred.subst(gammas)) }), debug, - simplify + simplify, + state ) + /* def checkVcs( preds: List[PredInfo], gammas: Subst, @@ -109,6 +117,7 @@ package object wptool { debug, simplify ) + */ def printFalseVcs(preds: List[PredInfo]) = { println("Failing VCs")