From f32f30c23e5b4d3f0a9f93a33b8a80b00f6743e9 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Thu, 4 Feb 2021 10:55:56 +1000 Subject: [PATCH 01/25] Being adding memory model --- tests/rg/caslev/steal_0 | 66 ---------------------------- tests/rg/caslev/steal_old | 70 ------------------------------ wptool/src/wptool/Exec.scala | 31 ++++++------- wptool/src/wptool/Expression.scala | 12 +++-- wptool/src/wptool/SMT.scala | 11 ++--- wptool/src/wptool/SMT_.scala | 2 +- wptool/src/wptool/State.scala | 18 +++++--- 7 files changed, 33 insertions(+), 177 deletions(-) delete mode 100644 tests/rg/caslev/steal_0 delete mode 100644 tests/rg/caslev/steal_old diff --git a/tests/rg/caslev/steal_0 b/tests/rg/caslev/steal_0 deleted file mode 100644 index 718d343..0000000 --- a/tests/rg/caslev/steal_0 +++ /dev/null @@ -1,66 +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 index: -local var level: -local var task: - -global var ret: -_L: TRUE - -_Gamma_0: z -> LOW, r -> LOW -_Rely: z' >= z -_Guar: z == z' - -h = head; -t = tail; - -if (h < t) { - do - _invariant: Gamma_r && Gamma_h && Gamma_t - { - do - _invariant: Gamma_r && Gamma_h && Gamma_t - { - r = z; - } while (r % 2 == 1) - - index = h % L; - level = levels[index]; - if (level == 1) { - task = tasks[index]; - } 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/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/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 3fdfa7b..637db11 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -45,7 +45,7 @@ object Exec { new PredInfo( stableR(assert.expression, state), assert, - "StableR" + "Assert" ) ) .incPrimeIndicies @@ -85,8 +85,7 @@ object Exec { } else { _state.incPrimeIndicies } - case ass: Assignment => - val assign = ass.asInstanceOf[Assignment] + case assign: Assignment => val globalPred = if (state.globals.contains(assign.lhs)) BinOp.pred( @@ -130,8 +129,7 @@ object Exec { ) .incPrimeIndicies } - case ass: ArrayAssignment => - val assign = ass.asInstanceOf[ArrayAssignment] + case assign: ArrayAssignment => val indexSub = Map(Id.indexId.toVar(state) -> assign.lhs.ident) val globalPred = @@ -209,12 +207,8 @@ 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 = { @@ -228,12 +222,6 @@ object Exec { BinOp.pred("=>", PreOp("!", Type.TBool, Type.TBool, stabRB), eval(exp, state)) ) case Assert(exp, checkStableR, _) => - /* BinOp( - "&&", - eval(exp, state), - Q - ) // Potentially move to exec to evaluate separately - */ Q case havoc: Havoc => Q case ass: Assignment => @@ -242,8 +230,12 @@ object Exec { Q.subst( Map( - (assign.lhs.toGamma.toVar(state) -> Left(rhsGamma)), - (assign.lhs.toVar(state) -> Left(eval(assign.expression, state))) + (assign.lhs.toGamma.toVar(state) -> Left(rhsGamma)), // TODO should gamma be an array (i think so) + // (assign.lhs.toVar(state) -> Left(eval(assign.expression, state))) + (Id.memId.toVar(state) -> Right( + Lit(state.addrs.getOrElse(ass.lhs, throw new Error("Memeory address not found"))), + eval(ass.expression, state) + )) ) ) case ass: ArrayAssignment => @@ -268,7 +260,10 @@ object Exec { } def eval(expr: Expression, state: State): Expression = expr match { - case id: Id => id.toVar(state) + case id: Id => + println(id) + println(state.addrs) + VarAccess(Id.memId.toVar(state), Lit(state.addrs.getOrElse(id, throw new Error("Memeory address not found")))) 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)) diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index 8e17feb..6ed7e60 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -45,8 +45,8 @@ 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 { - /* override def toString: String = - (if (gamma) "Gamma_" else "") + name + (if (prime) "'" else "") + (if (nought) "⁰" else "") */ + override def toString: String = + (if (gamma) "Gamma_" 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() @@ -57,13 +57,10 @@ case class Id(name: String, override val expType: Type.Type, prime: Boolean, gam def toGamma = Id(name, Type.TBool, prime, true, nought) 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 else state.indicies.getOrElse( - this.copy(gamma = false, expType = Type.TInt), + this.copy(gamma = false, expType = Type.TInt), // TODO change Type.TInt throw new Error(s"Index not found for gamma var $this with type $expType") ) } @@ -76,6 +73,7 @@ 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 memId = Id("mem", Type.TInt, false, false, false) } case class Var(ident: Id, index: Int, tmp: Boolean = false) extends Variable { @@ -183,7 +181,7 @@ case class PostOp(op: String, override val expType: Type.Type, argType: Type.Typ } case class BinOp(op: String, override val expType: Type.Type, argType: Type.Type, arg1: Expression, arg2: Expression) extends Expression { - // override def toString: String = "(" + arg1 + " " + op + " " + arg2 + ")" + 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 diff --git a/wptool/src/wptool/SMT.scala b/wptool/src/wptool/SMT.scala index 81ac9e5..fe8375f 100644 --- a/wptool/src/wptool/SMT.scala +++ b/wptool/src/wptool/SMT.scala @@ -5,7 +5,7 @@ import com.microsoft.z3.BoolExpr import com.microsoft.z3.enumerations.Z3_decl_kind import scala.reflect.runtime.universe.{TypeTag, typeOf} -object SMT_ { +object SMT { val intSize = 32 // size of bitvectors used val cfg = new java.util.HashMap[String, String]() val ctx = new z3.Context(cfg) @@ -21,19 +21,15 @@ object SMT_ { def prove( cond: Expression, - given: List[Expression], debug: Boolean, simplify: Boolean, expectIds: Boolean = false ) = { if (debug) - println("smt checking !(" + cond + ") given " + given.PStr) + println("smt checking !(" + cond + ")") solver.push() val res = try { - for (p <- given) { - solver.add(formula(p, expectIds)) - } // check that (NOT cond) AND P is unsatisfiable solver.add(formula(PreOp("!", Type.TBool, Type.TBool, cond), expectIds)) @@ -48,11 +44,10 @@ object SMT_ { throw error.Z3Error( "Z3 failed", cond, - given.PStr, "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() diff --git a/wptool/src/wptool/SMT_.scala b/wptool/src/wptool/SMT_.scala index 08ac9b3..9939ebc 100644 --- a/wptool/src/wptool/SMT_.scala +++ b/wptool/src/wptool/SMT_.scala @@ -6,7 +6,7 @@ import org.sosy_lab.java_smt.api.FormulaType import scala.reflect.runtime.universe.{TypeTag, typeOf} import org.sosy_lab.java_smt.api.SolverContext.ProverOptions -object SMT { +object SMT_ { val solver = Solvers.CVC4 val ctx = SolverContextFactory.createSolverContext(solver) val fmgr = ctx.getFormulaManager(); diff --git a/wptool/src/wptool/State.scala b/wptool/src/wptool/State.scala index 61024b9..6fa303f 100644 --- a/wptool/src/wptool/State.scala +++ b/wptool/src/wptool/State.scala @@ -21,6 +21,7 @@ case class State( arrRelys: Map[Id, Expression], arrGuars: Map[Id, Expression], indicies: Map[Id, Int], + addrs: Map[Id, Int], error: Boolean = false ) { def incPrimeIndicies = @@ -30,8 +31,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) } @@ -116,10 +116,13 @@ 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 + val addrs = ids.zipWithIndex.map { case (x, i) => Map((x -> i), (x.toPrime -> (i + ids.size))) }.flatten.toMap // TODO malformed probs insto the best State( @@ -138,7 +141,8 @@ object State { _guar, arrRelys, arrGuars, - primeIndicies + indicies, + addrs ) } } From ddf24434ad18c0acce41ea7e22c2fcbccfcb3acb Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Thu, 4 Feb 2021 13:56:33 +1000 Subject: [PATCH 02/25] Pointers WIP --- wptool/src/wptool/Exec.scala | 127 +++++++++++++++++------------ wptool/src/wptool/Expression.scala | 5 ++ wptool/src/wptool/State.scala | 3 +- 3 files changed, 82 insertions(+), 53 deletions(-) diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 637db11..45722d6 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -53,7 +53,7 @@ object Exec { _state .addQs( new PredInfo( - eval(assert.expression, state), + eval(assert.expression, state, true), assert, "Assert" ) @@ -101,8 +101,8 @@ object Exec { .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(assign.lhs.toVar(state) -> Left(assign.expression))), state, true), // TODO + BinOp.pred("||", eval(contr.toGamma, state, true), getL(contr, state)) ) }) .toList @@ -149,11 +149,12 @@ object Exec { "=>", eval( getL(contr, state).subst(Map(assign.lhs.ident.toVar(state) -> Right((assign.lhs.index, assign.expression)))), - state + state, + true ), // TODO BinOp.pred( "||", - eval(contr.toGamma, state), + eval(contr.toGamma, state, true), getL(contr, state).subst(Map(Id.indexId.toVar(state) -> Left(assign.lhs.index))) ) // TODO check subst is correct ) @@ -213,13 +214,13 @@ object Exec { 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("!", Type.TBool, Type.TBool, stabRB), eval(exp, state, true)) ) case Assert(exp, checkStableR, _) => Q @@ -232,10 +233,13 @@ object Exec { Map( (assign.lhs.toGamma.toVar(state) -> Left(rhsGamma)), // TODO should gamma be an array (i think so) // (assign.lhs.toVar(state) -> Left(eval(assign.expression, state))) - (Id.memId.toVar(state) -> Right( - Lit(state.addrs.getOrElse(ass.lhs, throw new Error("Memeory address not found"))), - eval(ass.expression, state) - )) + ((if (ass.lhs.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state)) + -> Right( + ( + Id.getAddr(ass.lhs, state), + eval(ass.expression, state, true) + ) + )) ) ) case ass: ArrayAssignment => @@ -245,11 +249,11 @@ object Exec { Q.subst( Map( (assign.lhs.ident.toGamma.toVar(state) -> Right( - (eval(assign.lhs.index, state), rhsGamma) + (eval(assign.lhs.index, state, true), rhsGamma) )), (assign.lhs.ident.toVar(state) -> Right( - eval(assign.lhs.index, state), - eval(assign.expression, state) + eval(assign.lhs.index, state, true), + eval(assign.expression, state, true) )) ) ) @@ -259,28 +263,36 @@ object Exec { } } - def eval(expr: Expression, state: State): Expression = expr match { + def eval(expr: Expression, state: State, memAccess: Boolean): Expression = expr match { case id: Id => - println(id) - println(state.addrs) - VarAccess(Id.memId.toVar(state), Lit(state.addrs.getOrElse(id, throw new Error("Memeory address not found")))) - case id: IdAccess => id.toVar(state).copy(index = eval(id.index, state)) + if (id == Id.indexId) id.toVar(state) + else if (memAccess && !id.gamma) + VarAccess(if (id.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state), Id.getAddr(id, state)) + else id.toVar(state) + case v: Var => + if (v.ident == Id.indexId) v + else if (memAccess && !v.ident.gamma) + VarAccess(if (v.ident.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state), Id.getAddr(v.ident, state)) + else if (memAccess && !v.ident.gamma) + VarAccess(if (v.ident.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state), Id.getAddr(v.ident, state)) + else v + case id: IdAccess => id.toVar(state).copy(index = eval(id.index, state, memAccess)) 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)) + 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 s: VarStore => s.copy( - array = eval(s.array, state), - index = eval(s.index, state), - exp = eval(s.exp, state) + 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)) + case a: VarAccess => a.copy(index = eval(a.index, state, memAccess)) case forall: ForAll => forall.copy( - bound = forall.bound.map(b => eval(b, state)), - body = eval(forall.body, state) + bound = forall.bound.map(b => eval(b, state, memAccess)), + body = eval(forall.body, state, memAccess) ) - case _: Lit | _: Const | _: Var => expr + case _: Lit | _: Const => expr case expr => println(s"Unhandled expression(eval): [${expr.getClass()}] $expr") expr @@ -290,7 +302,7 @@ object Exec { def getBaseArrays(vars: Set[VarAccess]): Set[VarAccess] = vars.map(v => v.getBase.resetIndex) def getRely(exp: Expression, state: State) = { - val evalExp = eval(exp, state) + val evalExp = eval(exp, state, false) eval( BinOp.pred( @@ -342,16 +354,17 @@ object Exec { 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)))) ) }) .toList ), - eval(state.rely, state) + eval(state.rely, state, false) ), - state + state, + false ) } @@ -360,20 +373,21 @@ object Exec { else eval( state.L.getOrElse(id, throw new Error("L not defined for " + id)), - state + state, + false ) } def getL(id: IdAccess, state: State): Expression = getL(id.ident, state) - .subst(Map(Id.indexId.toVar(state) -> Left(eval(id.index, state)))) + .subst(Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, false)))) def getL(v: VarAccess, state: State): Expression = getL(v.ident, state) - .subst(Map(Id.indexId.toVar(state) -> Left(eval(v.index, state)))) + .subst(Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, false)))) def primed(p: Expression, state: State) = - eval(p, state).subst( + eval(p, state, false).subst( (state.ids ++ state.arrayIds) .map(id => id.toVar(state) -> Left(id.toPrime.toVar(state))) .toMap @@ -383,11 +397,12 @@ object Exec { 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,7 +416,8 @@ object Exec { ), primed(p, state) ), - state + state, + true ) def rImplies(p: Expression, index: Expression, state: State) = @@ -411,15 +427,19 @@ object Exec { getRely(p, state).subst(Map(Id.indexId.toVar(state) -> Left(index))), 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 guar = eval(state.guar, state, true) + val subst = Map( + (Id.memId.toVar(state) -> Left(Id.memId.toVar(state).toNought)), + (Id.memId.toPrime.toVar(state) -> Left(Id.memId.toVar(state))) + ) val gPrime = guar.subst(subst) - val _subst = vars.map(v => v.toNought.asInstanceOf[Var] -> Left(v)).toMap + // val _subst = vars.map(v => v.toNought.asInstanceOf[Var] -> Left(v)).toMap + val _subst = Map(Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) wp(gPrime, a, state).subst(_subst) } @@ -429,9 +449,10 @@ 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, + 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 @@ -441,22 +462,24 @@ object Exec { } def computeGamma(exp: Expression, state: State): Expression = { - val expEval = eval(exp, state) + val expEval = eval(exp, state, false) constructForall( expEval.vars .map(v => eval( BinOp.pred("||", v.toGamma(state), getL(v.ident, state)), - 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))) + val subst = Map[Var, Left[Expression, Nothing]](Id.indexId.toVar(state) -> Left(eval(a.index, state, false))) eval( BinOp.pred("||", a.toGamma(state), getL(a.ident, state)).subst(subst), - state + state, + true ) // Default to high }) .toList diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index 6ed7e60..b6fd921 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -74,6 +74,11 @@ object Id { val tmpId = Id("tmp", Type.TInt, false, false, false) val indexId = Id("_i", Type.TInt, false, false, false) val memId = Id("mem", Type.TInt, false, false, false) + + def getAddr(id: Id, state: State): Lit = { + if (id.prime) Lit(state.addrs.getOrElse(id.copy(prime = false), throw new Error("Couldn't resolve memeory address"))) + else Lit(state.addrs.getOrElse(id, throw new Error("Couldn't resolve memeory address"))) + } } case class Var(ident: Id, index: Int, tmp: Boolean = false) extends Variable { diff --git a/wptool/src/wptool/State.scala b/wptool/src/wptool/State.scala index 6fa303f..de26fc9 100644 --- a/wptool/src/wptool/State.scala +++ b/wptool/src/wptool/State.scala @@ -122,7 +122,8 @@ object State { (Id.indexId -> 0) + (Id.tmpId -> 0) + (Id.tmpId.toPrime -> 0) + (Id.memId -> 0) + (Id.memId.toPrime -> 0) // TODO add support for arrays - val addrs = ids.zipWithIndex.map { case (x, i) => Map((x -> i), (x.toPrime -> (i + ids.size))) }.flatten.toMap + // TODO tmpId could remain a var as it cant be aliased + val addrs = (ids + Id.tmpId).zipWithIndex.map { case (x, i) => (x -> i) }.toMap // TODO malformed probs insto the best State( From 5d10ff369fbdbf44c8bb43319fa2bbad64074918 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Thu, 4 Feb 2021 15:08:32 +1000 Subject: [PATCH 03/25] Pointers WIP --- tests/rg/seqlock/read | 4 +- wptool/src/wptool/Exec.scala | 92 +++++++++++++++++------------- wptool/src/wptool/Expression.scala | 3 +- 3 files changed, 54 insertions(+), 45 deletions(-) diff --git a/tests/rg/seqlock/read b/tests/rg/seqlock/read index f07dfd5..4661f37 100644 --- a/tests/rg/seqlock/read +++ b/tests/rg/seqlock/read @@ -17,8 +17,8 @@ _Rely: z' >= z _Guar: (z' == z) do -// _invariant: Gamma_r1 -_invariant: Gamma_r1 && ((z == r1) => Gamma_r2) +_invariant: Gamma_r1 +// _invariant: Gamma_r1 && ((z == r1) => Gamma_r2) { do _invariant: Gamma_r1 diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 45722d6..aa6b0fd 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -231,8 +231,12 @@ object Exec { Q.subst( Map( - (assign.lhs.toGamma.toVar(state) -> Left(rhsGamma)), // TODO should gamma be an array (i think so) - // (assign.lhs.toVar(state) -> Left(eval(assign.expression, state))) + (Id.memId.toVar(state) -> Right( + ( + Id.getAddr(assign.lhs, state), + rhsGamma + ) + )), ((if (ass.lhs.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state)) -> Right( ( @@ -263,40 +267,44 @@ object Exec { } } - def eval(expr: Expression, state: State, memAccess: Boolean): Expression = expr match { - case id: Id => - if (id == Id.indexId) id.toVar(state) - else if (memAccess && !id.gamma) - VarAccess(if (id.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state), Id.getAddr(id, state)) - else id.toVar(state) - case v: Var => - if (v.ident == Id.indexId) v - else if (memAccess && !v.ident.gamma) - VarAccess(if (v.ident.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state), Id.getAddr(v.ident, state)) - else if (memAccess && !v.ident.gamma) - VarAccess(if (v.ident.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state), Id.getAddr(v.ident, state)) - else v - case id: IdAccess => id.toVar(state).copy(index = eval(id.index, state, memAccess)) - 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 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 => 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 == Id.indexId) id.toVar(state) + else if (memAccess && !id.gamma) + VarAccess(if (id.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state), Id.getAddr(id, state)) + else if (memAccess && id.gamma) + VarAccess(if (id.prime) Id.memId.toPrime.toGamma.toVar(state) else Id.memId.toGamma.toVar(state), Id.getAddr(id, state)) + else + id.toVar(state) + case v: Var => + if (v.ident == Id.indexId) v + else if (memAccess && !v.ident.gamma) + VarAccess(if (v.ident.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state), Id.getAddr(v.ident, state)) + else if (memAccess && v.ident.gamma) + VarAccess(if (v.ident.prime) Id.memId.toPrime.toGamma.toVar(state) else Id.memId.toGamma.toVar(state), Id.getAddr(v.ident, state)) + else v + case id: IdAccess => id.toVar(state).copy(index = eval(id.index, state, memAccess)) + 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 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 => expr + case expr => + println(s"Unhandled expression(eval): [${expr.getClass()}] $expr") + expr + } 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) @@ -304,7 +312,7 @@ object Exec { def getRely(exp: Expression, state: State) = { val evalExp = eval(exp, state, false) - eval( + val p = eval( BinOp.pred( "&&", constructForall( @@ -364,8 +372,9 @@ object Exec { eval(state.rely, state, false) ), state, - false + true ) + p } def getL(id: Id, state: State): Expression = { @@ -374,17 +383,17 @@ object Exec { eval( state.L.getOrElse(id, throw new Error("L not defined for " + id)), state, - false + true ) } def getL(id: IdAccess, state: State): Expression = getL(id.ident, state) - .subst(Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, false)))) + .subst(Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true)))) def getL(v: VarAccess, state: State): Expression = getL(v.ident, state) - .subst(Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, false)))) + .subst(Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, true)))) def primed(p: Expression, state: State) = eval(p, state, false).subst( @@ -468,6 +477,7 @@ object Exec { .map(v => eval( BinOp.pred("||", v.toGamma(state), getL(v.ident, state)), + // BinOp.pred("||", VarAccess(Id.memId.toGamma.toVar(state), Id.getAddr(v.ident, state)), getL(v.ident, state)), state, true ) // Default to high diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index b6fd921..2d099c2 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -76,8 +76,7 @@ object Id { val memId = Id("mem", Type.TInt, false, false, false) def getAddr(id: Id, state: State): Lit = { - if (id.prime) Lit(state.addrs.getOrElse(id.copy(prime = false), throw new Error("Couldn't resolve memeory address"))) - else Lit(state.addrs.getOrElse(id, throw new Error("Couldn't resolve memeory address"))) + Lit(state.addrs.getOrElse(id.getBase, throw new Error("Couldn't resolve memeory address"))) } } From a3d1b69d466ecb9a775d622095139e33dca03701 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Fri, 5 Feb 2021 09:20:08 +1000 Subject: [PATCH 04/25] Pointers WIP --- wptool/src/wptool/Exec.scala | 2 ++ wptool/src/wptool/WPTool.scala | 7 +++++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index aa6b0fd..8352d7c 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -76,6 +76,8 @@ object Exec { if (RG) { val gamma = computeGamma(guard.test, state) val stabR = stableR(gamma, state) + + println(s"$guard - $gamma") _state .addQs( new PredInfo(gamma, guard, "Gamma"), diff --git a/wptool/src/wptool/WPTool.scala b/wptool/src/wptool/WPTool.scala index 5e618df..c9ea748 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)) + println(state.addrs) val _state = Exec.exec(PreProcess.process(statements, state), state) @@ -143,9 +144,11 @@ object WPTool { val gammaSubstr = { for (i <- gammaDom) yield { - i.toGamma.toVar(_state) -> Left(gamma.getOrElse(i, High).toTruth) + // i.toGamma.toVar(_state) -> Left(gamma.getOrElse(i, High).toTruth) + // TODO TO TRUTH + Id.memId.toGamma.toVar(state) -> Right(Id.getAddr(i, state), gamma.getOrElse(i, High).toTruth) } - }.toMap.toMap[Var, Left[Expression, Nothing]] ++ Map(Id.tmpId.toGamma.toVar(_state) -> Left(Const._true)) + }.toMap ++ Map(Id.tmpId.toGamma.toVar(_state) -> Left(Const._true)) if (debug) println("Gamma0: " + gammaSubstr) if (debug) println("L: " + _state.L) From d80c5303c91fac5c0403fea7984b2255724d9b0d Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Fri, 5 Feb 2021 12:25:36 +1000 Subject: [PATCH 05/25] Fixed(?) guar for vars --- tests/rg/caslev/steal_ | 64 +++++++++++++++++++++++++++++++++ working-tests/array0 | 11 ++++++ wptool/lib/beaver.jar | Bin 0 -> 15118 bytes wptool/src/wptool/Exec.scala | 26 +++++++++----- wptool/src/wptool/WPTool.scala | 6 ++-- 5 files changed, 96 insertions(+), 11 deletions(-) create mode 100644 tests/rg/caslev/steal_ create mode 100644 working-tests/array0 create mode 100644 wptool/lib/beaver.jar diff --git a/tests/rg/caslev/steal_ b/tests/rg/caslev/steal_ new file mode 100644 index 0000000..95a6a01 --- /dev/null +++ b/tests/rg/caslev/steal_ @@ -0,0 +1,64 @@ +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: + +global var ret: +_L: TRUE + +_Gamma_0: z -> LOW, r -> LOW +_Rely: z' >= z +_Guar: z == z' + +h = head; +t = tail; + +if (h < t) { + do + _invariant: Gamma_r && Gamma_h && Gamma_t + { + do + _invariant: Gamma_r && Gamma_h && Gamma_t + { + 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/working-tests/array0 b/working-tests/array0 new file mode 100644 index 0000000..0ade55a --- /dev/null +++ b/working-tests/array0 @@ -0,0 +1,11 @@ +global array a[2]: +_L: FALSE +_Rely: TRUE +_Guar: TRUE + +_Rely: TRUE +_Guar: TRUE + +a[0] = 1; +a[0] = 2; +assert a[0] == 2; diff --git a/wptool/lib/beaver.jar b/wptool/lib/beaver.jar new file mode 100644 index 0000000000000000000000000000000000000000..677606233014d886643ef8ce0c41fc0d9541005c GIT binary patch literal 15118 zcmb7r19WCd*KRttZQFLowr$%^x?|h6Z9C~$9ot67>`rdx@A;-@dcJ?%d(T?+p0n0l z_0+Ci=WNv8TTT)P7!u%*3n4U)|9>9-{DFACOA9OU(}>H6(8>MT4IBXez1t;u->}j9 z-=6Oc`S0DN`DMgKgcX%&rA2O}$H$~3X=rC)Bxxuo$EWHQ=;xTW_8q7tCWomdX#~K* z_6k%IP^o%|-C8rk6_6wq6rD0DE0M9G5aXE?P`r@F6mH)CkzjI^=-CP7lZN*Rt5TI< z9kz4i@pl7~)S=a(1^5qD0RKbPJ0X8vVDC=`#`-SC4!@Bu$QH{T4-5dX{=R6;zje}g za5Q!x7IrbVadM&*n`CkN)c}i}xzf5aNTVEmr6Cvp zLxqAF+cq<`73=W@X-^5$341>3$BWL(g)4=j&?qz=kL{0pnY)fI&Eii-c0jG{hdkfh zr#v?fn@y(GTGqKM!d8o3qS_2^uj+UB zUxBB)8pp@=hr-*8z9vD7jU6;$Z^WvQ28_U81kt1PHH2ZHsDoH9LXX*1Q<+75~h)R^97h|5wdj-DQL*kCzevum!Q^y^0{DXY;&nyu6Y@YtM05wV|* z?FHzdxEN?Ol;QmUbjU^ExU}UFcjlwtPF?OStd|}knPAW8vm&2ecnr{kl&sh z%ErsfSzm6@^6np-9K||j4R4J*-ZyiWwCsx$Xr8J)3L{}1CHxk)ua3b)6joTKrZTO_ zj6GBXnZ;%;A49b+TG&o4RgbI7de@N=3ZdR}8&=7cmsP0zs4QGp7?z2K6tuT=0mRu| zrg}%NGayNMkne`~fb0Yc$RaDPFbF2^6%t5(VJNR5S?3NvC`etlwS#>vPi@E_7_t)^ zL7_(iDacx`rbHhzSBIO0pT96&?k?9rzMwbSAeYb;i=%B(*?4PWFw$dGjKr3 zCh=IATgC3o9n5^y@2qGyjBpdtrYMJPcLKd|put+rW}z`qXK$IKE;v29gIZJzWr{m~ zy0CsLa}YJ24lCL@&4l~heP_4Max8gVV#XtFQIoCRAbH_OGo1qbMS&f5XAi%umzk>z zNLh392sX|tEN8ic*1Cx@WxY`c;NC$6fz*&&jeUL1UTWou$zVH>3nKPvF6HIuPC9gz zQe9-^kK$gWP8@d7=_yayS0(c6%X*$(dB4uSF6T#A^6qJ~KJg~&tQ%q-6RbO+oNZ>$ zEY1uV)VH1^(tD)tJc1U!z2l7hH6*K4Pxt!-Lxh?VMEE}4XQUWc(g4!31 zfaNTK5H6Q1){A1(&+S=)*va$}3>p*>Zu56fD8TdLR8a)7bM*P&Ip1JT)~?6Q-hgJb z8)udg*hNn#Cp!tbPGf6nbsZlzr;Wx-J)~S==zz19WRDULj-U5pF+DI1sulCRU~yVL z>u436sj5GdXbl?s_*dcg%g$4aLVa)9ixrB!W@Ephu-Ss>=7a&)bOzT9U^?Mv|MUp& z0S7G*22TpUO-isv7{F}2Sv1EL5JM0kE|5YPU@qVm4SxWxp9Oz$4n$!82>%QV-3Lgp zMiw9}phg$~7H}B@??gC^AdrRNcTOZg4&R4KkP@JG4z%63Ey(Vn2ak*7Ck+lu&=Md= z5I{*#fz$^|V1?Kx8gR)#;3Y6+8gR)$;8hD35bg~A5e)tS7PGIGr>c&Q;*e_eDa|2E zZW49hOORtzVbV3><_DAU)cjc1t~CCb&5kwxjrM^BzDRlY&?kWF=#z@I?N9%acR!^t zdq$Q$)dv88vG<1ZOO){&I+@$r5HtRiV%l=jlKp(}-swf+(uyzJY`6G3xylV+Ernyk z;K6k$JKgN#ZJbG@_2QAgt9l@EKLUN1-`VT;S6@n9X1m!KKYN%uM6+P;?-I5d8mJ28 z0o_#yVr(@ifeCU1^~R(D7FJVM`2gL76eJ)G zggfLHQ*{c_g=*n+PR0lsJ%n^pFhF=0>dfr+C^@C0s)H<*p$~#@UX>+QqDVuMY1SGc z+}DE*YKdAniq_1CRjlsB^=aGEMo=^pwRF69`Z;(D5Yt=Kg}H4Y*BClXWY3&wPL{W4 z<-wOL46fMRKl#mEgD`+Pzsfiv9S2Cga+}h95}|s9dcdKkjq^xR>4jUvpHvv zot}4~=rTXpb4EpbAK@vtd2-+@&@ipJ);}z-Px-ifdwKZysY?L;#ZGmQiycc4O+?uz zLy;k5%5Zq6ZZL>f~3o#om3z4dLhp`HL&mw|gR$tFq zd5}d*)lRTiS|I%NIO`ZuVDUPjMm3#CE-6QerhV(p;%YQ$_0#7X8dc^y_t_DxX`Dr; zAn@Ane&>nOQ;g^?eRVXpDKTQ!eK1l8ghY*T6cp5}*ww1xMNFk=RA=IQ7C}0xUvVUT zz$QZy5^hx*b!Ix#1gGnotT~BL)|~^bA5K}G7h}gMImviIKm<;WtQQ(?vJ6j@`zEEw zpVK#BVWb=j&QU55q3{)sf`)Kq@ufQt(aHuj0?PxaT^_#63ix^4XX#J6t4z3{tnK&+ z<#rTf)o1XM)H$g&_3AC&b`m{j*r;s)imn{2_pKP^*(|5&)5a?4802+jgSd_>tiv}d zEPo)aV807Ho{eUq_AC-v+DTaVvs^dLNUNU5>Bnvq+F1bI{o#7+uHA2gJzIm+&g?~< z6qN@kCMLJqCHC=T+Qr7 zh=EfBoE5}*0HJN0ibFu_#E7!qm6=Mu!C(xyZmXO!ebHa3LCRH2%hGI{{?IYT zhWe;$6HhrkXDHQ{7rkshYJm#n)5jv+S)%SO57GzhSsYPadJD%6(qko?dOg8qwwAg& zwv%U-M_sN@yP9knMXTV5Fz-)TsUsGceKWy_1>q2R^ z&kRjHJT2;r1U@RwQsvxkF$#QojQ#Ne(FxIWX<;BJ4355sta(6HUyN}Yw+l7@%ySf@ z&wmO5Lz0f5A%Gl@=6f~va(e*H6atpaYuJL51IP)JmN+Y4Wj6t)y40)R?6J|&6=Xwx z?8FRC?4g-u)OsyKxlk4XqK;P(`A3ycdncNobi9$(wQTjV&!w)Q37NytYt@`^J;{Ta zBlYp5x6ri*>_-h#Xt%MozreHsW>)p(S+>Y7Ud2E@203w)0?C%_N!q8Z@&pSmMMH;o zVX@hNuB10m>*4p>8+&4gm#7fL=4aoD4zWwvyct@Bhm*~D?2{2||CFm8r5btP)cK5) zdCc-+Y?XQkPDh06_80<&IS4d&e{8I>w*W=VYO+L8PXMLOJQk_iVvn_}WSMp>#MhXL zzX{UogUqgjxw6j`o}~N5!5|QvKSJw;*9TZ zM@7fB0}sexSVdmW^H}Dv`lVKqv!mrtb!;aQDa-+N`l({F#ETHm5W zJi~V0@_-(LWec>$dS&+Udwtm?(j~=q537Wa-wd3!5?>|qnPd`sk`8<?ar*$nclbqaaj}!Xn zcs!@hdE%sJDOxAJfkR77IIuF!XR+PT_}GTmJbJXA#xk%m7sM2?G%a+Mm`%q#l5Lua zL2}fRFck>LU7%moZ!n0irAY|4sX*sY9S9@lcGM`q&7PYP&*K@pZS|V4)XJ3>L#Mzf+7)UPyVkRJTX+qBI zKKn7FS^GkI#h=`+L;TQ7tf=ZEsbZV##>=vk5g44;o&wq81I-1j`&P(HTd7F2%y3MH zckS8X@Rhm$%ndi!Q5!e3wMW^lC~NjAzo(x4m0c6YIX(HT9pP|y9DPDs=f)<)o$p5| z>X%7`4-qW)3K5vo^6_ z)WqgfN=Nxu^y{?+gKS|dg88Hb83kjkY@oc$8%5iECM87glOZV{ zrLviTQ)wgfu2w?fUj909q5*}p7mXCf#A~vnnA!MPD$VN+yZ}1|Drr30=*CwqW7$eN zzi<{jp1!SY1A&M3%ixvg{UKcJS9GorvSdb&aghqHh>e*mrlZhQpzOsO6|l3_Ue5a0 z(LezC^_|>6mK@O51j}qj{Jl@7qB8@K&^*fa}CHdnAp9J=FrGc|Lu6onS zjOEN9&pvMfVT#!3tGI9;627?9~YdnBvSmFk&{raiXB=;y5I;9YN0iSocM z9s?TAruScCM6U&gEU<6)m<-)$kI~B+0uP zXy1+1&g0e-JhMb}2IfuPr=$PPahKp}>7ZA3@ZJXx_sdkk>^49YUh+DT!I}J%=Xm50 zk6T}G=@QW^T+3Af904~;E*`RM@WAj?;6npFr|}{QY@2X_=xbJNw=Vc@4ZX+yw~*;9 z6pd^zT<6_n8}8z*$bmG?T@lh$g=tGf2&P7Sn}S&r4gICCJy0fukpiiF_1?ys2`QtL zGwl`%izXw35nv>yFDos>QB~TOnARp`4ymycLx`s;YPZXffg(x;r;#OQb3>TON&zUd z7(_&24QbujsYXzvE^ex&}3Rk3#)h0>uU8TkD0GT>QYE?j2Ib- zrTY+NmFgxl@7zs@Soo*bT}v`ljkk0_!<3PnDkphEd5X!VxnU#(YDts#-r3o?a}Z$E z_Q?+-T6bvLur`QHJju5!%TSb;ruxJ+k?tG(U@VoyPYQ7WHfM@s$iqTKrx9UJS{`2( zPr*8U!TOT^Bg958__#>TP{isGBPxUgtQnE2TGAx0scD`M5h+-WRfzsV$#Shh;i%Cy z^b2vbQ5l7Hc9gX~jjL9ZK_k7fNPI;Hd7_n0ip0q6_%Phgs>1j-hhZqFBNEm`N~y_M zIVl$`yuhPmSL$=5$}*|f#Epp!SVzQeYT!k154tL{L#ni#U{PLv+dSNo6I7d zIy!^Ky}Xp$C;C;LKxEw^g#jn(9(Nn=>fOc1$f!WIf?cr3+$hok_J}ukPI({xA&H9Z z&oW}6b~*{&nH&4|fNH{kJG&x!QW_c~hfwwVh@+dHE z+pnUcT(7`zPD#)r)rxm{LLZ{pb@ipPp81Fim&NLE6uu7AD8!jFN`6g8!Z1_}P4vY1 zw(B2Xu_r4@AUyG%Smhc;}Owkd-!MH>gNw7@wIXSh_AMsd7P$L-KWcwe+&f;_A zFPq2Hre?b(S#7g~f{Q;Xngqfy5sk^<>c??VSnbW!S>NYJ*H@4-X4+z!rX$!k#`u6o zV9|O=F7Xd!W$`WJQ(Rc{wxSHsx5q8FJ{(SUf*2cMGYv7mOPhJyC?L=dRvr4ty|I#-(;mj|3r$yURA&lovMj_yI}(C#Q_2yxsH z@`s`<+amz6#8IiL54h|xBdLmg{qpIwvUb#OF_HnoLdlWZnk5W;j#!PA2-dla6!DI= z!+xmc{kHS8GqMMoKf;XpH7V8v7n=+Eo>#=GF@^gcCaHDbL~<=8taYYx4TdHo23r(4 zRbFpG?Vdtk&@$ZoI&ixgeJoAEYs9FqG4wkC7uIK}eBetrHi?=jRq3rs4UFQ7#M%)J z3`w`UD;tU={%wKRuxrbBw@mmGU&usPUxEEhyW5!s9PMcVB9!jlwk_@f!hrqnA2DV4 zcmSl&eN}lvKCgsdS>O?(PB8|ew1C&RAYvv*9KIPGg!bR4>lS=Jn?^YaY^PP)0Fs64 z0CVK^BFx1##gm1uJDpm-+eMtKomW-?1TTNurr@QWcn-Pom)~s^^ID?y*e<6!>8-&% zk`!Q)xn%WI1aMC2yfbLvG;oJre&&c4R*$Z0kC>Ihj)zLl&vFJ6<#+I1k|&RM&!EC4 z|Mul_Fjq##nk?fx76a8IjV?=Y+tl}S<)8o$nWLY8_Bs8ZTTe+@Dj z4z&)fF@eE`MzH)8-ldewWevUx7&s7?RW0#_wGe*RM=$4B1|If1GcXYbF7%5pOL8f@ zSc@N2hpxuBqN>LWjcH`|1-aphJw6!DhimO6%a!STVZMW;oVP4dsW!~=0D_uNFOj!3 zZ1n(>KG7bS_cT-dwrg=mP^F5e-~NowHAmJW>K(*$;&`U2nN&S`<8>jv965MywxuMAh!-@%Z0-lt8i!r;^^*XSS(=vH0>op}l*^;aLULaw5tvWx z%}jV+8!ob|eGy5p_f+2y1|&yYO0smPQ}`z@I8veK`ie?ybl=e;7XUg^a)X1bg*2yo9Y(xDp!5m4Brn3mPm1o%du;G``5=PLOKXS!)A93{c zpJ_}|{3pT#gL*|d{g^WhDSDVGg-{{~tgba{6P8}apa2b{# zn`#<{g9V)(E?COXI@n+C`zCIfYd?zax2_>qj{AdQMk|^DevyM9{VJ3&TflE0;D`cE zG@`7$P&J528Mmm&8dco_X5^(&xQr3^ML9!zFWc!(i>hJ=G}I!)?c0|<3z`xX6jYtT z7-hM&s2%)Iheahwg2B0?pBHhypdx9{U)V(&#E&zWT( zDb7zY$@81+kxC2H;DowUibS5Mg>^5&ak_}96k|HLvhEe1x{Q+RkzN_)0+V>ku~wp0W`xhqIXLB@PQv#>^$W?b4{^@&Pqn zejl3so9azLJkVtCh+es(hn)O5B$)PkNy2e;MlYY;3T?!}{%wta=5PhL=K%r1^1&3i z8H)17XGP8W{86OKr2!^90qq`~%Zk!#&<<8}l}%nyq>S_*kZz_R+@2hFRiA@TZ*Zyr zamT!duDl(V%5uuNHA$AmtN|zAf^WX73Lzw^8p_sAbjLlBC|p8bCA=7?1G<>m#T0oX<(EY^uYL=hOt3`D>QVX`0`qnEbVy&){! zgGH(h`Sh64=E9?422)EM)F!8~B^I+L6SFox?Gn6lNU`CAD0x)=T*M-IsA~xbo;)O; zB4)NcsIDSaS8n7Z+ZbLx%_zSrMW#;ypi^X;z+x%AwX*5VodxWA4sDLL1;=`U%8ZLM z$9i6#Q+e2|by@0#oNCSYM5pAoB$u-EV;yI#_2P>>Z40!8Zz!8@s&JsvKbniEf= zgDcL^ZQ=p9kICMx?mWSZggS>e>P6Qcv>k6C|1`iKj+6}v-~FHR_x48!_RnDFpZ@+& z3tU-FTDI@~>>nynqVl?QXJ!B>MGp>_MJI%m_}#HxYj(~HH(qQA+?u*J+UdpHie{Wt z5io+gaoOldWozI3n5|20_*pSJcXwxaur?gYcV(TkXi*D;W-Gd($SGx*I$tWsBfnwP z7G$*ZRjLOgO%$;tSYo!{0YRQKQNB-#in&(Ggi)DwGe+jM!cBxILad4$hP1Y!zj|4I zmNPpI&0xr+x*Mf~hA`f4ebpwR^~iyjVT`%R(|G7Pog>+?HI7&73%IR7fic~WjCx~>>l-Scz3@z* z2rBx-zI!&_d6?yS!O`v6wXu%Z@oSZ|H}(7%!oM?3=IT)6AuP;HaykZDSJ zUn8DV-VO@w-L21}U9PFl#Ikp0(u`Qn5hwm-N1>f>*&Gz4Z;;%>Dm+*leK`UlSwwaf zMJ@iLVNp7#Vrs?&j3AzU6og_=I`A(07XQXNh;1;qLS2qolDlcTm*0+@U1W!}mK zPQE=6kzpTCbgD*O>z>|nPO8Kib7e(mFay1!N8G&yrzHkCo@<0WX=p?g(7=$`5+k?` zD7e{mgHxJ*BL@XvYT6{Ods{<{By=9~s&&NI3Qu1BflT^Jok?%+b0lYYzj*6jPrmdR^uiZGi_t3MVlb&v2i+Xgo7xr4K7wwsn+qOi}|l{1p=t zcm+_dHF?OtQvH8=3@>gT*`LGzu*zUsZ&`8N`QGZ(55+^pNl_8kl*P^2u{pZ2BwXrh$SBMEpaQ@>#X zvo8{npbdC-S}W!L1Dwgyd_YSxs=!jz5uF=sf`A;RYiU#y50n(+K; z?SxUMk6TRAKbE_XAP2c_Pv0X zfteS2$QgMt^O{tao;2Z)<8mrp)i%c*eM{#H-CR>VDPU<(VlYBG0W9ae^K>}VqwGC!yI9=eNK6$A0xXiWqUv$Vv`S*XIR z<|5gZl(!OLJ8Qc;tMc0yG#pWPbSjmO_cTW=*i;NO3Trg_slc??q_1$-9ky!lkZteI zg5`bW^p8`2^fW~{s!ZoUhW2YeDXz_9!Q@cq1ess02uK`eND$Qxz*K2*Uf2)}OG){( zio)Kmwsl4V2xZ}?sHRTc_%&8zMq5tsL!}y@CSi=KBe0J#V3;eUF){_0UnK2kxvPP9ftSdO@@41EQ`vqt*{^qnr(uqYqB8zd<%{Kd^^1yPe>y1$OV+bcA~f z0X&33uF*{Pd+z|Q(P3W3w4lQwT?yuaL?d1i<-r6CN60Fr8XL;h;vUi;HX*#+13C-( zdgSnVSM&V*NgO7 zNv@7IAAMxEO-^lWsx3URPf%G7HZE%r8P@cMo+%USmO@O;brh9n^kuQBvx$o6M@x+$ z{}HT7cA$GBg=%pkus}#ZiODf4`fM+0I@ucJpve zA0_Qlz6qv!K&hnnJfg@7!>1`OI{x|+mf_1xXFrk_RmSQ%SA&SaY1TksY}u=d?H)Vf zHRg#{*8pL9`4@zQjNt?EW<;gbCrh?5D!PpvL=x;`v)IY1HPkBSZ((=J8s7G0KS2>Htue+<e>Qks=p6@1+3QpD%Q)Rm8>xo>`WiMoV+2Q$8# zc5lt!xqn14+SZ(Rj09bRB@Jp?v3(kVejRAKHvJA|3+3A#0{=SNbj?;98+jlhYWvyr zWO<-zB&U9Be+c3-6h=l7DFl4p9QxYvjx=a_rvv(>dRfiL-5FslQU=I9*w?jjIEL)z z_(^eecwkt?BDvOzsxdr@u!n&`y|fZfG;~42pr1XhkxJ~0D=JK)@|;}7PRgv;=NkPx zI@NU^0uWjs7cHHX7oq0+#l(aFK{mO}7627$Ze^PQj~OS8RH*RqnYVQ|-Bb?sKU z$8A;IIc=Pk_Lz4PZ_Jn>Z{l0xdp)XoNRzp9I-|Iq!Xf$iXg=1>I$008-(|M9mI zZbf%%16!+~_I0F^rsJ##GOwkiLq!<7xHu*kL;$MQkk(p~CILZUOTpb1F+Hq#syWu4 z8hc(COjHI1)0z(e_suvL-8i#gG2C|mALQHB{Ky&{nEtVgtobL}Lo?US&bMzggU7@_ z%)SC-$}0Hz#Pox3XeIPlgzD4sCnGY`nYA=1w6->Mbg6Y|Jehmvc4(jwkNUwTXiQjd z+B{n}E!yu08Qqc5X_xBs2hV}=KSzxtGAp!Nep?crvSAIQYHXhj`bb57u+R&kgA-t_ zE4OBDFtk$l=1|q#q`hg)a>bxaJH@9))p(*Op}ba9zqVY)ajx8cz~E}xf4^|nL}l1m z>Mn+4WYy3yiK>POGgN(zONnxG6z7mExFQ^^tD2jL9<+?FA{RCM*D;mlL#Tg+!A`A`-c;!&x27n{i zEEHf*!S6odPx;4#N1Vj0i+PeS4E;uEf7yr z5E9-K3xLfF{=qyeWe5V{6k;Cd#18zayhp@@{chX-Bj;uyE3(Gtn-GEO5=@0aHeyJm zc4Vp$?XYfGa}hc28RH05{PxeN32i45GmEz{i-|i)5TqZ=hHVMRHY9xr{k#x%r|{oE z_KZohVf9{y_a$C)(Z{eA8F2>U$ksIl^&OHM`sQel@j#f&0OdiBCE>M#wjh13oW0t6 z`vO0cBg+K$ne#$2=#2Ekn?k7@Z&P#~#l7VRHr$KDmCLn3z*&+XsnWlKZfKruOZ6ao z3+(6gv4d1gFo#-+a zQ?Tw3;OtP~(;r*Ov0L>S&KJKW&*kNQ^M?fm0JwP%V&VPrpZ`qnQnIx)wo!C)FxI#J z`Kbr0NID`bBfnmZ8+n*~O*QHxiuo*rXw2vy`zQntLBK!+Ap{Bt%yMkRDc)Z|CiM{T z8Isorq|H7UGF(nr041r;p6Ezm{c)uPYD@vGO8GWpH8X3HZ&c~7^I>hsb@Cz8(e_}n zQ!^Vs#H9mA5J*N?K03L@UA>oTE!v)GGV;rWP(+%zO&#Pdc#%QL0P`vn0{U9^!2vWI zhm8plJ<;$GeQ-S_q`X>W8 zXRv5v(526O0Zq}yU-P}4@FyGz(j@WN8Cd7yIfh;2_-aX6X6K*)S^SaOSgX-EnI^|= zuG!=>(&8+OI|gs+k)E(CDMVcKrN&IwXBup7%=E2Ps4{Zn?<4eCz9E`INA8<)TGdAaSIX;*85$v?5gM z)tt)&u><>#=07pDrPe~Vu~Ov}VN|jet0&2X!<2WjzT7hkOEw1=jLA790EKXRpdT=A zV=lbLp-44FFn%hxb(!Rq9e^(HP8pjKA8W}OyJI#MWt&3f*f2`XfW~dwTOvy>b~ck) z6rU5S+wUq2tDq%lf0gY4b5kmg@H39Ce2h$c_M<_854od}I&o~`Cn@^;gna85l$t0c zQoxa(o!nQj46BxKV&`Kqy2BU}=cA4$HeFN#Mk=R^s#@PHVq}o&RZCy`fR)iL5iB-j zZmpv@6R3}ZbEH%YBu@FNY^BtIU-)&qlhv$Z* zv8A-im%cErRBPsnFBGF#FYP%y9K2fE8echDI~FSQ(7=?i`#*;Lso2}l>ek#@Vti2WvocYn1OgH3H+IE$Q19r$>{E&<53Ve};x5a#*7dA6v%zV_^b{U%}X4lb?O z!cjM^OMpQ3vu3=ds=ydHZqY-HZ&nF9t07d=SIc{N^$%7=?K7q~UFT-kXC`%cSIf~~ zMNx=`l!)t!Phz~&SDVMWlE%U(&-aFq>@nrDO1&d0>{kZi4wB}iLzGSt0ZW@mfE7oF zz-e*`QPcz;+Xg%`Rw7Gs?!ASsK5To5-7D`nz{n0a0_<*ypT+q!4IcsS9b%lhbQX>r zXoo8G8xJV3xli*feG~Y2E--|V=3583ot*D=A{gpP?o_FrP@f=-+L#F#t}QYzTEeYfz9BSk z?N=d|Nqjal{fJ0diD4c<_qC-1oY&uvYv7F*<@iv^PWQ2H{=&E%$NMOG*&P=sicuHMMjcL#vXqkzOk5mducWXI#Welz7;JAiGUD?b%v6d_?v^7csi&x!t?07$jaNz- z-MS&0)yNaJMsNI_ug8kcft&DeC3&fWw>V#F#%!0QwRv7X4b8iD&Lx+p4^Y=uCQ5u4 z?s_GqdCOfq&zh3$OzuPzX94>`n_G{$;(Y|8s-6ynxcXF{Z0d`Q#67u@NYbUlwS=od zQP3o1KIpsJV^@gZPJtZ)Nlq9MAU92FaDE90Dvdz!?z^qqE|1 zG%_g{#!fsTnG=+M9SeKeEyreUcu}t^+6$aqYi}O|>Wj5B*A_9M`uangQ68Q@QT-+vM15$-TESm&xnDhC{J3|I-q$}j;FIDpI zq8Ye%Rq|KSjP-l{iOpYUjQ{TZNAk~aoo$SrXdO*xe=A-2_fWF`+t8l~G!9OG%?}R1 z9T>;|-INdXkFuSu_eT5w4q|6(P3vZDRZl@aIwc`ZTf3_uS2HppD?S17XLS$L4AV4I z&5S6*E?_C87`4O%kR^b_*YImeC~n2GYX!;Mu-V%p=gB(3` zGhV&0RW8>OSUl&XD4nW2)Im6QO%lpjb`Q;JJX zO3?yL_#ASCnrQdoo%9cY$Uy&lmDM}_?-xA4IsYH`zut&n!~T2K)gPVzxC(s#@izRe z2J08Xf3J}GIsT7{JKrDwdg=Z{?ayg{ubBEd=#Oc4{x;~}^;5ql|L^4rzi=u+{+j%s z#S6bf{GOBl3j*rB;Ojs1|JMxt-=TibU;PC|3H=w;-?LeN2lzeV@)tlG%wGWiOZw&S zSiffk{=zbT7byQ+*KhfOzeD|=7xxRQ4E`^uKe_y8mfY_Uzvp)Sf}lYB3*zsYUcUqU z9-I0FQ1&kJ{#?#KB2~X5{2qz + 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 (memAccess && !id.gamma) - VarAccess(if (id.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state), Id.getAddr(id, state)) + VarAccess(mem, Id.getAddr(id, state)) else if (memAccess && id.gamma) - VarAccess(if (id.prime) Id.memId.toPrime.toGamma.toVar(state) else Id.memId.toGamma.toVar(state), Id.getAddr(id, state)) + VarAccess(mem.toGamma(state), Id.getAddr(id, state)) else id.toVar(state) case v: Var => + 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(if (v.ident.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state), Id.getAddr(v.ident, state)) + VarAccess(mem, Id.getAddr(v.ident, state)) else if (memAccess && v.ident.gamma) - VarAccess(if (v.ident.prime) Id.memId.toPrime.toGamma.toVar(state) else Id.memId.toGamma.toVar(state), Id.getAddr(v.ident, state)) + VarAccess(mem.toGamma(state), Id.getAddr(v.ident, state)) else v case id: IdAccess => id.toVar(state).copy(index = eval(id.index, state, memAccess)) case BinOp(op, t1, t2, arg1, arg2) => @@ -443,15 +448,20 @@ object Exec { ) def guar(a: Assignment, state: State) = { - val guar = eval(state.guar, state, true) + val guar = eval(state.guar, state, false) + 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 subst = Map( (Id.memId.toVar(state) -> Left(Id.memId.toVar(state).toNought)), (Id.memId.toPrime.toVar(state) -> Left(Id.memId.toVar(state))) ) + */ val gPrime = guar.subst(subst) - // val _subst = vars.map(v => v.toNought.asInstanceOf[Var] -> Left(v)).toMap val _subst = Map(Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) - wp(gPrime, a, state).subst(_subst) + // val _subst = vars.map(v => v.toNought -> Left(v)).toMap + // val _subst = Map(Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) + wp(eval(gPrime, state, true), a, state).subst(_subst) } def guar(a: ArrayAssignment, state: State) = { diff --git a/wptool/src/wptool/WPTool.scala b/wptool/src/wptool/WPTool.scala index c9ea748..7491d84 100644 --- a/wptool/src/wptool/WPTool.scala +++ b/wptool/src/wptool/WPTool.scala @@ -105,7 +105,6 @@ object WPTool { // printBlocks(PreProcess.process(statements, state)) if (debug) PreProcess.printGraphvis(PreProcess.process(statements, state)) - println(state.addrs) val _state = Exec.exec(PreProcess.process(statements, state), state) @@ -146,11 +145,12 @@ object WPTool { for (i <- gammaDom) yield { // i.toGamma.toVar(_state) -> Left(gamma.getOrElse(i, High).toTruth) // TODO TO TRUTH - Id.memId.toGamma.toVar(state) -> Right(Id.getAddr(i, state), gamma.getOrElse(i, High).toTruth) + // TODO Low?? + Id.memId.toGamma.toVar(state) -> Right(Id.getAddr(i, state), gamma.getOrElse(i, Low).toTruth) } }.toMap ++ Map(Id.tmpId.toGamma.toVar(_state) -> Left(Const._true)) - if (debug) println("Gamma0: " + gammaSubstr) + // if (debug) println("Gamma0: " + gammaSubstr) if (debug) println("L: " + _state.L) if (debug) println("Indicies: " + _state.indicies) From a7154f66954cd47ad697c814ce65d483b36990fc Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Mon, 8 Feb 2021 11:21:11 +1000 Subject: [PATCH 06/25] Fix substitute for vars in memory --- wptool/src/wptool/Exec.scala | 80 +++++++++++++++--------------- wptool/src/wptool/Expression.scala | 40 ++++++++++++--- wptool/src/wptool/SMT.scala | 2 +- wptool/src/wptool/SMT_.scala | 2 +- wptool/src/wptool/State.scala | 8 +-- wptool/src/wptool/WPTool.scala | 7 +-- wptool/src/wptool/package.scala | 2 +- 7 files changed, 83 insertions(+), 58 deletions(-) diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 53b0449..90d6c38 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -102,7 +102,7 @@ object Exec { .map(contr => { BinOp.pred( "=>", - eval(getL(contr, state).subst(Map(assign.lhs.toVar(state) -> Left(assign.expression))), state, true), // TODO + eval(getL(contr, state).subst((Map(assign.lhs.toVar(state) -> Left(assign.expression)), state)), state, true), // TODO BinOp.pred("||", eval(contr.toGamma, state, true), getL(contr, state)) ) }) @@ -149,14 +149,14 @@ object Exec { BinOp.pred( "=>", eval( - getL(contr, state).subst(Map(assign.lhs.ident.toVar(state) -> Right((assign.lhs.index, assign.expression)))), + getL(contr, state).subst((Map(assign.lhs.ident.toVar(state) -> Right((assign.lhs.index, assign.expression))), state)), state, true ), // TODO BinOp.pred( "||", eval(contr.toGamma, state, true), - getL(contr, state).subst(Map(Id.indexId.toVar(state) -> Left(assign.lhs.index))) + getL(contr, state).subst((Map(Id.indexId.toVar(state) -> Left(assign.lhs.index)), state)) ) // TODO check subst is correct ) }) @@ -226,25 +226,16 @@ object Exec { case Assert(exp, checkStableR, _) => Q case havoc: Havoc => Q - case ass: Assignment => - val assign = ass.asInstanceOf[Assignment] + case assign: Assignment => val rhsGamma = computeGamma(assign.expression, state) Q.subst( - Map( - (Id.memId.toVar(state) -> Right( - ( - Id.getAddr(assign.lhs, state), - rhsGamma - ) - )), - ((if (ass.lhs.prime) Id.memId.toPrime.toVar(state) else Id.memId.toVar(state)) - -> Right( - ( - Id.getAddr(ass.lhs, state), - eval(ass.expression, state, true) - ) - )) + ( + Map( + (assign.lhs.toGamma.toVar(state) -> Left(rhsGamma)), + (assign.lhs.toVar(state) -> Left(eval(assign.expression, state, false))) + ), + state ) ) case ass: ArrayAssignment => @@ -252,14 +243,17 @@ object Exec { val rhsGamma = computeGamma(assign.expression, state) 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) - )) + ( + 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 ) ) case stmt => @@ -370,7 +364,7 @@ object Exec { "&&", pred, eval(state.arrRelys.getOrElse(v.ident, Const._true), state, false) - .subst(Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, false)))) + .subst((Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, false))), state)) ) }) @@ -396,17 +390,20 @@ object Exec { def getL(id: IdAccess, state: State): Expression = getL(id.ident, state) - .subst(Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true)))) + .subst((Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true))), state)) def getL(v: VarAccess, state: State): Expression = getL(v.ident, state) - .subst(Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, true)))) + .subst((Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, true))), state)) def primed(p: Expression, state: State) = eval(p, state, false).subst( - (state.ids ++ state.arrayIds) - .map(id => id.toVar(state) -> Left(id.toPrime.toVar(state))) - .toMap + ( + (state.ids ++ state.arrayIds) + .map(id => id.toVar(state) -> Left(id.toPrime.toVar(state))) + .toMap, + state + ) ) // TODO take havoc statements into account @@ -427,7 +424,7 @@ 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) @@ -440,7 +437,7 @@ object Exec { 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, @@ -457,11 +454,11 @@ object Exec { (Id.memId.toPrime.toVar(state) -> Left(Id.memId.toVar(state))) ) */ - val gPrime = guar.subst(subst) + val gPrime = guar.subst((subst, state)) val _subst = Map(Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) // val _subst = vars.map(v => v.toNought -> Left(v)).toMap // val _subst = Map(Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) - wp(eval(gPrime, state, true), a, state).subst(_subst) + wp(eval(gPrime, state, true), a, state).subst((_subst, state)) } def guar(a: ArrayAssignment, state: State) = { @@ -470,16 +467,17 @@ object Exec { BinOp.pred( "&&", state.guar, - eval(state.arrGuars.getOrElse(a.lhs.ident, Const._true), state, true).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, 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 gPrime = guar.subst((subst, state)) val _subst = vars.map(v => v.toNought.asInstanceOf[Var] -> Left(v)).toMap - wp(gPrime, a, state).subst(_subst) + wp(gPrime, a, state).subst((_subst, state)) } def computeGamma(exp: Expression, state: State): Expression = { @@ -499,7 +497,7 @@ object Exec { .map(a => { val subst = Map[Var, Left[Expression, Nothing]](Id.indexId.toVar(state) -> Left(eval(a.index, state, false))) eval( - BinOp.pred("||", a.toGamma(state), getL(a.ident, state)).subst(subst), + BinOp.pred("||", a.toGamma(state), getL(a.ident, state)).subst((subst, state)), state, true ) // Default to high diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index 2d099c2..062314f 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -86,7 +86,7 @@ case class Var(ident: Id, index: Int, tmp: Boolean = false) extends Variable { 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") @@ -130,13 +130,37 @@ case class VarAccess(name: Var, index: Expression) extends Variable { 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 + 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 { + + su._1 + .filter { + case (v, 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 + case (v, Right(_)) => false + } + .foldLeft(updatedArr: Expression) { + case (p, (v, Left(e))) => { + val i = su._2.addrs.get(v.ident.getBase).get + this.index match { + case Lit(n) if (i != n) => + p + case _ => + val memId = v.ident.copy(name = Id.memId.name) + VarStore(p, Lit(su._2.addrs.get(v.ident.getBase).get), e) + } + } + } } } diff --git a/wptool/src/wptool/SMT.scala b/wptool/src/wptool/SMT.scala index fe8375f..5b970d0 100644 --- a/wptool/src/wptool/SMT.scala +++ b/wptool/src/wptool/SMT.scala @@ -5,7 +5,7 @@ import com.microsoft.z3.BoolExpr import com.microsoft.z3.enumerations.Z3_decl_kind import scala.reflect.runtime.universe.{TypeTag, typeOf} -object SMT { +object SMT_ { val intSize = 32 // size of bitvectors used val cfg = new java.util.HashMap[String, String]() val ctx = new z3.Context(cfg) diff --git a/wptool/src/wptool/SMT_.scala b/wptool/src/wptool/SMT_.scala index 9939ebc..08ac9b3 100644 --- a/wptool/src/wptool/SMT_.scala +++ b/wptool/src/wptool/SMT_.scala @@ -6,7 +6,7 @@ import org.sosy_lab.java_smt.api.FormulaType import scala.reflect.runtime.universe.{TypeTag, typeOf} import org.sosy_lab.java_smt.api.SolverContext.ProverOptions -object SMT_ { +object SMT { val solver = Solvers.CVC4 val ctx = SolverContextFactory.createSolverContext(solver) val fmgr = ctx.getFormulaManager(); diff --git a/wptool/src/wptool/State.scala b/wptool/src/wptool/State.scala index de26fc9..ab3152d 100644 --- a/wptool/src/wptool/State.scala +++ b/wptool/src/wptool/State.scala @@ -50,9 +50,11 @@ object State { var controlled: Set[Id] = Set() var controlledBy: Map[Id, Set[Id]] = Map() - val arrayIds = definitions collect { case a: ArrayDef => - a.toVarDefs.name - } + val arrayIds = { + definitions collect { case a: ArrayDef => + a.toVarDefs.name + } + } + Id.memId val arrRelys = definitions .collect { case a: ArrayDef => diff --git a/wptool/src/wptool/WPTool.scala b/wptool/src/wptool/WPTool.scala index 7491d84..32c6404 100644 --- a/wptool/src/wptool/WPTool.scala +++ b/wptool/src/wptool/WPTool.scala @@ -146,15 +146,16 @@ object WPTool { // i.toGamma.toVar(_state) -> Left(gamma.getOrElse(i, High).toTruth) // TODO TO TRUTH // TODO Low?? - Id.memId.toGamma.toVar(state) -> Right(Id.getAddr(i, state), gamma.getOrElse(i, Low).toTruth) + i.toGamma.toVar(_state) -> Left(gamma.getOrElse(i, High).toTruth) } }.toMap ++ Map(Id.tmpId.toGamma.toVar(_state) -> Left(Const._true)) - // if (debug) println("Gamma0: " + gammaSubstr) + println("Gamma0: " + gammaSubstr) + 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) 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..91adfbe 100644 --- a/wptool/src/wptool/package.scala +++ b/wptool/src/wptool/package.scala @@ -14,7 +14,7 @@ package object wptool { // 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[Var, Either[Expression, (Expression, Expression)]], State) val sub = "₀₁₂₃₄₅₆₇₈₉" implicit class StringOps(self: String) { From 6a37cfb718c99902fd5e4196d3a84b075ff501ca Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Tue, 9 Feb 2021 09:53:46 +1000 Subject: [PATCH 07/25] More bug squashing - Fixed issue with priming vars --- README.md | 4 ++++ wptool/src/wptool/Exec.scala | 6 +++--- wptool/src/wptool/Expression.scala | 25 ++++++++++++++++++------- wptool/src/wptool/Parser.grammar | 2 ++ wptool/src/wptool/SMT.scala | 7 +++++-- wptool/src/wptool/SMT_.scala | 3 ++- wptool/src/wptool/Scanner.flex | 2 +- wptool/src/wptool/WPTool.scala | 1 - 8 files changed, 35 insertions(+), 15 deletions(-) diff --git a/README.md b/README.md index 49f606b..a7344f5 100644 --- a/README.md +++ b/README.md @@ -127,3 +127,7 @@ Below is an inconclusive list of unsupported language features. ### Weak memory model The logic for the weak memory model is currently not implemented +## Optimisations +### Passification + + diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 90d6c38..14345b3 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -238,8 +238,7 @@ object Exec { state ) ) - case ass: ArrayAssignment => - val assign = ass.asInstanceOf[ArrayAssignment] + case assign: ArrayAssignment => val rhsGamma = computeGamma(assign.expression, state) Q.subst( @@ -397,9 +396,10 @@ object Exec { .subst((Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, true))), state)) def primed(p: Expression, state: State) = + // TODO handle memId eval(p, state, false).subst( ( - (state.ids ++ state.arrayIds) + (state.arrayIds + Id.memId) .map(id => id.toVar(state) -> Left(id.toPrime.toVar(state))) .toMap, state diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index 062314f..42b0a35 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -2,6 +2,12 @@ package wptool import scala.reflect.runtime.universe.{TypeTag, typeOf} +sealed abstract class Type +sealed abstract class TPointer(pointerType: Type) extends Type +case object TBool extends Type +case object TInt extends Type +case object TPointerInt extends TPointer(TInt) + object Type extends Enumeration { type Type = Value val TBool, TInt = Value @@ -130,7 +136,7 @@ case class VarAccess(name: Var, index: Expression) extends Variable { def subst(su: Subst) = { val updatedArr = this.copy(index = index.subst(su)) - if (name.ident.getBase != Id.memId) { + val s = if (name.ident.getBase != Id.memId) { su._1.get(name) match { case Some(Right((i: Expression, e: Expression))) => VarStore(updatedArr, i, e) @@ -140,7 +146,6 @@ case class VarAccess(name: Var, index: Expression) extends Variable { case None => updatedArr } } else { - su._1 .filter { case (v, Left(_)) => @@ -153,15 +158,18 @@ case class VarAccess(name: Var, index: Expression) extends Variable { case (p, (v, Left(e))) => { val i = su._2.addrs.get(v.ident.getBase).get this.index match { - case Lit(n) if (i != n) => - p - case _ => - val memId = v.ident.copy(name = Id.memId.name) + case Lit(n) if (i != n) => p + case _ if (name.index != v.index) => p + case _ => + // val memId = v.ident.copy(name = Id.memId.name) + // VarStore(p, Lit(su._2.addrs.get(v.ident.getBase).get), e) VarStore(p, Lit(su._2.addrs.get(v.ident.getBase).get), e) } } } } + // println(this, s) + s } override def toString = name + "[" + index + "]" @@ -178,7 +186,10 @@ case class VarStore(array: Expression, index: Expression, exp: Expression) exten 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)) + def subst(su: Subst) = { + // println(this, VarStore(array.subst(su), index.subst(su), exp.subst(su))) + VarStore(array.subst(su), index.subst(su), exp.subst(su)) + } override def expType = array.expType } diff --git a/wptool/src/wptool/Parser.grammar b/wptool/src/wptool/Parser.grammar index 9ad2307..64a775a 100644 --- a/wptool/src/wptool/Parser.grammar +++ b/wptool/src/wptool/Parser.grammar @@ -156,6 +156,8 @@ 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); :} + // TODO | ID.n AMP {: return new Id(n, TPointer.TPointerInt(), false, false, false); :} + | ID.n AMP {: return new Id(n, Type.TInt(), false, false, false); :} | 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 diff --git a/wptool/src/wptool/SMT.scala b/wptool/src/wptool/SMT.scala index 5b970d0..5eff96d 100644 --- a/wptool/src/wptool/SMT.scala +++ b/wptool/src/wptool/SMT.scala @@ -5,7 +5,7 @@ import com.microsoft.z3.BoolExpr import com.microsoft.z3.enumerations.Z3_decl_kind import scala.reflect.runtime.universe.{TypeTag, typeOf} -object SMT_ { +object SMT { val intSize = 32 // size of bitvectors used val cfg = new java.util.HashMap[String, String]() val ctx = new z3.Context(cfg) @@ -25,8 +25,11 @@ object SMT_ { simplify: Boolean, expectIds: Boolean = false ) = { - if (debug) + if (debug) { println("smt checking !(" + cond + ")") + println("translated as " + formula(PreOp("!", Type.TBool, Type.TBool, cond), expectIds)) + } + solver.push() val res = try { diff --git a/wptool/src/wptool/SMT_.scala b/wptool/src/wptool/SMT_.scala index 08ac9b3..fca1a12 100644 --- a/wptool/src/wptool/SMT_.scala +++ b/wptool/src/wptool/SMT_.scala @@ -6,7 +6,7 @@ import org.sosy_lab.java_smt.api.FormulaType import scala.reflect.runtime.universe.{TypeTag, typeOf} import org.sosy_lab.java_smt.api.SolverContext.ProverOptions -object SMT { +object SMT_ { val solver = Solvers.CVC4 val ctx = SolverContextFactory.createSolverContext(solver) val fmgr = ctx.getFormulaManager(); @@ -112,6 +112,7 @@ object SMT { case _ => throw new Error("Unexpected statement in VarStore") } + // TODO is this necessary (i.e. do we ever actually get nested stores) def handleStore( store: Expression, arr: api.ArrayFormula[api.NumeralFormula.IntegerFormula, _ <: api.Formula], diff --git a/wptool/src/wptool/Scanner.flex b/wptool/src/wptool/Scanner.flex index 22e9de5..debb4b7 100644 --- a/wptool/src/wptool/Scanner.flex +++ b/wptool/src/wptool/Scanner.flex @@ -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); } diff --git a/wptool/src/wptool/WPTool.scala b/wptool/src/wptool/WPTool.scala index 32c6404..51c5aeb 100644 --- a/wptool/src/wptool/WPTool.scala +++ b/wptool/src/wptool/WPTool.scala @@ -150,7 +150,6 @@ object WPTool { } }.toMap ++ Map(Id.tmpId.toGamma.toVar(_state) -> Left(Const._true)) - println("Gamma0: " + gammaSubstr) if (debug) println("Gamma0: " + gammaSubstr) if (debug) println("L: " + _state.L) if (debug) println("Indicies: " + _state.indicies) From d923a28a518feabb68e09cf3334c46ac2ac24a81 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Tue, 9 Feb 2021 10:44:06 +1000 Subject: [PATCH 08/25] Fix subst over _i --- wptool/src/wptool/Expression.scala | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index 42b0a35..bf6babb 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -136,7 +136,7 @@ case class VarAccess(name: Var, index: Expression) extends Variable { def subst(su: Subst) = { val updatedArr = this.copy(index = index.subst(su)) - val s = if (name.ident.getBase != Id.memId) { + if (name.ident.getBase != Id.memId) { su._1.get(name) match { case Some(Right((i: Expression, e: Expression))) => VarStore(updatedArr, i, e) @@ -146,6 +146,12 @@ case class VarAccess(name: Var, index: Expression) extends Variable { 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, Left(_)) => @@ -154,22 +160,22 @@ case class VarAccess(name: Var, index: Expression) extends Variable { ) && this.ident.gamma == v.ident.gamma && this.ident.prime == v.ident.prime && this.ident.nought == v.ident.nought case (v, Right(_)) => false } - .foldLeft(updatedArr: Expression) { + .foldLeft(memId: Expression) { case (p, (v, Left(e))) => { - val i = su._2.addrs.get(v.ident.getBase).get + // TODO handle _i this.index match { - case Lit(n) if (i != n) => p - case _ if (name.index != v.index) => p - case _ => + case _ if v == Id.indexId.toVar(su._2) => p + case Lit(n) if (su._2.addrs.get(v.ident.getBase).get != n) => p + case _ if (name.index != v.index) => p + case _ => // val memId = v.ident.copy(name = Id.memId.name) // VarStore(p, Lit(su._2.addrs.get(v.ident.getBase).get), e) VarStore(p, Lit(su._2.addrs.get(v.ident.getBase).get), e) } } } + } - // println(this, s) - s } override def toString = name + "[" + index + "]" @@ -186,10 +192,7 @@ case class VarStore(array: Expression, index: Expression, exp: Expression) exten 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) = { - // println(this, VarStore(array.subst(su), index.subst(su), exp.subst(su))) - VarStore(array.subst(su), index.subst(su), exp.subst(su)) - } + def subst(su: Subst) = VarStore(array.subst(su), index.subst(su), exp.subst(su)) override def expType = array.expType } From dda888152b013fcae509190cb6b19893c400f2b2 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Tue, 9 Feb 2021 11:01:49 +1000 Subject: [PATCH 09/25] Update SMT array handling --- wptool/src/wptool/SMT.scala | 48 +++++++++++++++++++------------------ 1 file changed, 25 insertions(+), 23 deletions(-) diff --git a/wptool/src/wptool/SMT.scala b/wptool/src/wptool/SMT.scala index 5eff96d..4889b89 100644 --- a/wptool/src/wptool/SMT.scala +++ b/wptool/src/wptool/SMT.scala @@ -100,34 +100,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") } @@ -171,9 +170,12 @@ object SMT { ) case store: VarStore => - handleStore( + handleSelect( store, - getArray(store), + handleStore( + store, + expectIds + ), expectIds ) From 525b1bfe159bb0a4f2a047c7b9df786c50b66772 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Tue, 9 Feb 2021 14:09:49 +1000 Subject: [PATCH 10/25] Leave local vars unresolved and update rely for globals --- wptool/src/wptool/Exec.scala | 36 ++++++++++++++++++++++++++---- wptool/src/wptool/Expression.scala | 3 ++- 2 files changed, 34 insertions(+), 5 deletions(-) diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 14345b3..cc6d781 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -263,7 +263,7 @@ object Exec { def eval(expr: Expression, state: State, memAccess: Boolean): Expression = expr match { - case id: Id => + 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) @@ -273,7 +273,8 @@ object Exec { VarAccess(mem.toGamma(state), Id.getAddr(id, state)) else id.toVar(state) - case v: Var => + 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 @@ -300,18 +301,23 @@ object Exec { bound = forall.bound.map(b => eval(b, state, memAccess)), body = eval(forall.body, state, memAccess) ) - case _: Lit | _: Const => expr + case _: Lit | _: Const | _: Var => expr case expr => println(s"Unhandled expression(eval): [${expr.getClass()}] $expr") expr } 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 getBaseArrays(vars: Set[VarAccess]): Set[VarAccess] = vars.filter(v => v.name.ident != Id.memId).map(v => v.getBase.resetIndex) + def getBaseMems(vars: Set[VarAccess]): Set[VarAccess] = vars.filter(v => v.name.ident == Id.memId).map(v => v.getBase.resetIndex) def getRely(exp: Expression, state: State) = { val evalExp = eval(exp, state, false) + // TODO !!!! + // rely incorrect as using mem for rely not var itself + // TODO should local vars not be loaded into memeory (????) + // related: how will the rely work for pointers ?!?? val p = eval( BinOp.pred( "&&", @@ -366,6 +372,28 @@ object Exec { .subst((Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, false))), state)) ) + }) + .toList + ++ getBaseMems(evalExp.arrays) + .map(v => { + val pred = + // 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)) + // ) + + BinOp.pred( + "&&", + pred, + eval(state.arrRelys.getOrElse(v.ident, Const._true), state, false) + .subst((Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, false))), state)) + ) + }) .toList ), diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index bf6babb..668906f 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -157,7 +157,8 @@ case class VarAccess(name: Var, index: Expression) extends Variable { case (v, 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 + ) && 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 } .foldLeft(memId: Expression) { From 2448bf13cd22efe73897b2298e0b3f893d716c94 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Tue, 9 Feb 2021 14:59:20 +1000 Subject: [PATCH 11/25] Passing all tests - Fixed small issue with generating rely --- wptool/src/wptool/Exec.scala | 5 +++-- wptool/src/wptool/WPTool.scala | 1 + 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index cc6d781..4a2e7d5 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -308,8 +308,9 @@ object Exec { } def getBaseVars(vars: Set[Var]): Set[Var] = vars.map(v => v.getBase.resetIndex) - def getBaseArrays(vars: Set[VarAccess]): Set[VarAccess] = vars.filter(v => v.name.ident != Id.memId).map(v => v.getBase.resetIndex) - def getBaseMems(vars: Set[VarAccess]): Set[VarAccess] = vars.filter(v => v.name.ident == Id.memId).map(v => v.getBase.resetIndex) + def getBaseArrays(vars: Set[VarAccess]): Set[VarAccess] = + vars.filter(v => v.name.ident.getBase != Id.memId).map(v => v.getBase.resetIndex) + def getBaseMems(vars: Set[VarAccess]): Set[VarAccess] = vars.filter(v => v.name.ident.getBase == Id.memId).map(v => v.getBase.resetIndex) def getRely(exp: Expression, state: State) = { val evalExp = eval(exp, state, false) diff --git a/wptool/src/wptool/WPTool.scala b/wptool/src/wptool/WPTool.scala index 51c5aeb..08a2c36 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) From 1f925c0a4a1d1585471e34dec233d655419f9715 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Wed, 10 Feb 2021 09:58:17 +1000 Subject: [PATCH 12/25] Update type structure and grammar --- README.md | 10 ++++ wptool/src/wptool/Exec.scala | 12 ++--- wptool/src/wptool/Expression.scala | 74 +++++++++++++++++----------- wptool/src/wptool/Parser.grammar | 78 ++++++++++++++++++------------ wptool/src/wptool/Preprocess.scala | 12 ++--- wptool/src/wptool/SMT.scala | 40 +++++++-------- wptool/src/wptool/SMT_.scala | 60 +++++++++++------------ wptool/src/wptool/Statement.scala | 4 +- wptool/src/wptool/VarDef.scala | 12 ++--- 9 files changed, 174 insertions(+), 128 deletions(-) diff --git a/README.md b/README.md index a7344f5..d4b9b4f 100644 --- a/README.md +++ b/README.md @@ -123,6 +123,16 @@ _invariant: TRUE ### Unsupported language features Below is an inconclusive list of unsupported language features. * Pointers + * Dynamic allocation + + + * 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 diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 4a2e7d5..450f18e 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -221,7 +221,7 @@ object Exec { BinOp.pred( "&&", BinOp.pred("=>", BinOp.pred("&&", eval(exp, state, true), stabRB), Q), - BinOp.pred("=>", PreOp("!", Type.TBool, Type.TBool, stabRB), eval(exp, state, true)) + BinOp.pred("=>", PreOp("!", TBool, TBool, stabRB), eval(exp, state, true)) ) case Assert(exp, checkStableR, _) => Q @@ -330,7 +330,7 @@ object Exec { // "&&", 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)) @@ -338,7 +338,7 @@ 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)) ) @@ -353,7 +353,7 @@ object Exec { // "&&", 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, state), state), v.toPrime(state).toGamma(state)) @@ -361,7 +361,7 @@ 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)) ) } @@ -382,7 +382,7 @@ object Exec { // "&&", 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, state), state), v.toPrime(state).toGamma(state)) diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index 668906f..e0bba1b 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -3,15 +3,9 @@ package wptool import scala.reflect.runtime.universe.{TypeTag, typeOf} sealed abstract class Type -sealed abstract class TPointer(pointerType: Type) extends Type -case object TBool extends Type -case object TInt extends Type -case object TPointerInt extends TPointer(TInt) - -object Type extends Enumeration { - type Type = Value - val TBool, TInt = Value -} +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 @@ -21,7 +15,7 @@ trait Expression extends beaver.Symbol { def subst(su: Subst): Expression def arrays: Set[VarAccess] - def expType: Type.Type + def expType: Type } case class Lit(arg: Int) extends Expression { @@ -30,7 +24,7 @@ case class Lit(arg: Int) extends Expression { override def ids = Set() override def arrays = Set() override def subst(su: Subst): Lit = this - override def expType = Type.TInt + override def expType = TInt } trait Identifier extends Expression { @@ -50,7 +44,7 @@ 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) extends Identifier { override def toString: String = (if (gamma) "Gamma_" else "") + name + (if (prime) "'" else "") + (if (nought) "⁰" else "") override def vars = throw new Error("Tried to get var from id") @@ -60,26 +54,26 @@ case class Id(name: String, override val expType: Type.Type, prime: Boolean, gam 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) def getIndex(state: State) = { if (!gamma) state.indicies.getOrElse(this, throw new Error(s"Index not found for var $this with type $expType")) else state.indicies.getOrElse( - this.copy(gamma = false, expType = Type.TInt), // TODO change 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") ) } // TODO use actual type - override def getBase = Id(name, Type.TInt, false, false, false) + override def getBase = Id(name, TInt, 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 memId = Id("mem", Type.TInt, false, false, false) + val tmpId = Id("tmp", TInt, false, false, false) + val indexId = Id("_i", TInt, false, false, false) + val memId = Id("mem", TInt, false, false, false) def getAddr(id: Id, state: State): Lit = { Lit(state.addrs.getOrElse(id.getBase, throw new Error("Couldn't resolve memeory address"))) @@ -113,8 +107,8 @@ 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 this(name: String, index: Expression) = this(Id(name, TInt, false, false, false), index) + def this(name: String, prime: Boolean, gamma: Boolean, index: Expression) = this(Id(name, TInt, prime, gamma, false), index) def vars = index.vars def ids = index.ids def arrays = throw new Error("tried to get array from IdAccess") @@ -134,6 +128,7 @@ case class VarAccess(name: Var, index: Expression) extends Variable { def ids = index.ids def arrays = Set(this) + // TODO document/comment def subst(su: Subst) = { val updatedArr = this.copy(index = index.subst(su)) if (name.ident.getBase != Id.memId) { @@ -207,7 +202,7 @@ case class ArrayConstDefault(name: Var, const: Expression) extends Expression { } */ -case class PreOp(op: String, override val expType: Type.Type, argType: Type.Type, arg: Expression) extends Expression { +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 @@ -215,7 +210,7 @@ case class PreOp(op: String, override val expType: Type.Type, argType: Type.Type 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 @@ -223,7 +218,7 @@ case class PostOp(op: String, override val expType: Type.Type, argType: Type.Typ 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 @@ -232,7 +227,7 @@ case class BinOp(op: String, override val expType: Type.Type, argType: Type.Type } 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 { @@ -246,18 +241,18 @@ case class Const(name: String) extends Expression { 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), 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 ForAll(bound: Set[_ <: Expression], body: Expression) extends Expression { @@ -267,5 +262,28 @@ case class ForAll(bound: Set[_ <: Expression], body: Expression) extends Express 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: Id) extends Expression { + def this(x: String) = this(Id(x, TInt, false, false, false)) + override def vars = ident.vars + override def ids = ident.ids + override def arrays = ident.arrays + override def subst(su: Subst) = Dereference(ident.subst(su)) + + override def expType = ident.expType match { + case TPointer(t) => t + case _ => throw new Error("Invalid pointer type") + } +} + +case class Reference(ident: Id) extends Expression { + def this(x: String) = this(Id(x, TInt, false, false, false)) + override def vars = ident.vars + override def ids = ident.ids + override def arrays = ident.arrays + 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 64a775a..40eb274 100644 --- a/wptool/src/wptool/Parser.grammar +++ b/wptool/src/wptool/Parser.grammar @@ -65,8 +65,11 @@ %typeof NUM = "Integer"; +%typeof ptrdef = "VarDef"; + %typeof boolexpr = "Expression"; %typeof intexpr = "Expression"; +%typeof ptrexpr = "Expression"; %typeof local = "Stmt"; @@ -90,12 +93,22 @@ 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()); :} + ; +vardef + = 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()); :} + | ptrdef.n COLON {: return new VarDef(n.name().name(), GlobalVar.instance()); :} // TODO + | ptrdef.n COLON lpred.l {: return new VarDef(n.name().name(), l, 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); :} @@ -111,6 +124,7 @@ 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); :} | 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); :} @@ -125,27 +139,27 @@ 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); :} + | GAMMAID.n {: return new Id(n, TBool.instance(), false, true, false); :} + // | PRIMEID.n {: return new Id(n, TBool.instance(), true, 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); :} + | 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); :} | LPAREN boolexpr.e RPAREN {: return (Symbol) e; :} | TRUE {: return new Const("True"); :} @@ -154,25 +168,29 @@ boolexpr 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); :} - // TODO | ID.n AMP {: return new Id(n, TPointer.TPointerInt(), false, false, false); :} - | ID.n AMP {: return new Id(n, Type.TInt(), false, false, false); :} + | PRIMEID.n {: return new Id(n, TInt.instance(), true, false, false); :} + | ID.n {: return new Id(n, TInt.instance(), false, false, false); :} | 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); :} | 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; :} ; +ptrexpr + // TODO = ID.n {: return new Id(n, new TPointer(TInt.instance()), false, false, false) :} + = AMP ID.n {: return new Reference(n); :} + | STAR ID.n {: return new Dereference(n); :} + ; + // for _L(x): pred construction to set predicate for variable security level lpred = LPRED COLON boolexpr.a {: return (Symbol) a; :}; diff --git a/wptool/src/wptool/Preprocess.scala b/wptool/src/wptool/Preprocess.scala index cfed0bd..1f0a915 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,7 +85,7 @@ object PreProcess { // Assert(branchGamma) head case doWhile: DoWhile => - val after = currBlock.prepend(Assume(PreOp("!", Type.TBool, Type.TBool, evalExp(doWhile.test)))) + val after = currBlock.prepend(Assume(PreOp("!", TBool, TBool, evalExp(doWhile.test)))) val repeat = Block( "do-while repeat", List(Guard(doWhile.test), Assert(doWhile.invariant, true)), @@ -106,7 +106,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 +116,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 4889b89..4f15bf0 100644 --- a/wptool/src/wptool/SMT.scala +++ b/wptool/src/wptool/SMT.scala @@ -27,14 +27,14 @@ object SMT { ) = { if (debug) { println("smt checking !(" + cond + ")") - println("translated as " + formula(PreOp("!", Type.TBool, Type.TBool, cond), expectIds)) + 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 { @@ -144,11 +144,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 @@ -191,41 +191,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 fca1a12..b214bdc 100644 --- a/wptool/src/wptool/SMT_.scala +++ b/wptool/src/wptool/SMT_.scala @@ -29,7 +29,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(); @@ -91,7 +91,7 @@ object SMT_ { 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]]( @@ -127,7 +127,7 @@ object SMT_ { translateInt(a.index, expectIds), // TODO Type? // TODO !!!!!!!! - if (a.expType == Type.TInt) translateInt(a.exp, expectIds) else translateBool(a.exp, expectIds) + if (a.expType == TInt) translateInt(a.exp, expectIds) else translateBool(a.exp, expectIds) ), expectIds ) @@ -138,43 +138,43 @@ object SMT_ { 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] @@ -185,26 +185,26 @@ 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) + 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] diff --git a/wptool/src/wptool/Statement.scala b/wptool/src/wptool/Statement.scala index c413ffd..5daec4a 100644 --- a/wptool/src/wptool/Statement.scala +++ b/wptool/src/wptool/Statement.scala @@ -63,7 +63,7 @@ object Block { case class Assignment(lhs: Id, 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), expression, ("", -1)) override def toString: String = lhs + " = " + expression def incLine = this.copy(line = line.copy(_2 = line._2 + 1)) @@ -76,7 +76,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), index), expression, ("", -1)) override def toString: String = lhs.ident + "[" + lhs.index + "]" + " = " + expression diff --git a/wptool/src/wptool/VarDef.scala b/wptool/src/wptool/VarDef.scala index 2f75607..98d27d7 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), 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), security) def toPair: Seq[(Id, Security)] = this match { case g => @@ -94,9 +94,9 @@ sealed trait Definition extends beaver.Symbol case class VarDef(name: Id, pred: Expression, 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), pred, 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), Const._true, access) } case class ArrayDef( @@ -116,7 +116,7 @@ case class ArrayDef( guar: Guar ) = this( - new Id(name, Type.TInt, false, false, false), + new Id(name, TInt, false, false, false), size, pred, access, @@ -131,7 +131,7 @@ case class ArrayDef( guar: Guar ) = this( - new Id(name, Type.TInt, false, false, false), + new Id(name, TInt, false, false, false), size, Const._true, access, From c0d29e1871fa386ebe751965354c54e616fbab04 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Fri, 12 Feb 2021 09:47:14 +1000 Subject: [PATCH 13/25] Fix subst for pointer aliasing --- tests/rg/pointers1 | 13 ++++ wptool/src/wptool/Exec.scala | 111 +++++++++++++++++++++++++---- wptool/src/wptool/Expression.scala | 25 +++++-- wptool/src/wptool/Parser.grammar | 1 + wptool/src/wptool/Statement.scala | 4 +- wptool/src/wptool/WPTool.scala | 2 +- wptool/src/wptool/package.scala | 4 +- 7 files changed, 135 insertions(+), 25 deletions(-) create mode 100644 tests/rg/pointers1 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/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 450f18e..5f838fb 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -86,23 +86,23 @@ object Exec { } else { _state.incPrimeIndicies } - case assign: Assignment => + case assign @ Assignment(lhs: Id, _, _) => val globalPred = - if (state.globals.contains(assign.lhs)) + if (state.globals.contains(lhs)) 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)), state, true), // TODO + eval(getL(contr, state).subst((Map(lhs.toVar(state) -> Left(assign.expression)), state)), state, true), // TODO BinOp.pred("||", eval(contr.toGamma, state, true), getL(contr, state)) ) }) @@ -130,6 +130,56 @@ object Exec { ) .incPrimeIndicies } + case assign @ Assignment(Dereference(id), _, _) => + // TODO preds + /* + val globalPred = + if (state.globals.contains(id)) + BinOp.pred( + "=>", + getL(id, state), + computeGamma(assign.expression, state) + ) + else Const._true + */ + /* + val controlPred = if (state.controls.contains(id)) { + constructForall( + state.controlledBy + .getOrElse(id, Set()) + .map(contr => { + BinOp.pred( + "=>", + eval(getL(contr, state).subst((Map(id.toVar(state) -> Left(assign.expression)), state)), state, true), // TODO + BinOp.pred("||", eval(contr.toGamma, state, true), getL(contr, state)) + ) + }) + .toList + ) + } else Const._true + */ + + 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, "Global"), + // new PredInfo(rImplies(controlPred, state), assign, "Control") + ) + .incPrimeIndicies + } else { + _state + .addQs( + // new PredInfo(globalPred, assign, "Global"), + // new PredInfo(controlPred, assign, "Control") + ) + .incPrimeIndicies + } + case assign: ArrayAssignment => val indexSub = Map(Id.indexId.toVar(state) -> assign.lhs.ident) @@ -226,14 +276,35 @@ object Exec { case Assert(exp, checkStableR, _) => Q case havoc: Havoc => Q - case assign: 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, false))) + (lhs.toGamma.toVar(state) -> Left(rhsGamma)), + (lhs.toVar(state) -> Left(eval(assign.expression, state, false))) + ), + state + ) + ) + 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") + } + + // TODO this is broken + // could make subst exp -> Either + // and then pass in Deref(id) and handle in subst + // this may be better as it is more general + // current approach doesnt work for multiple ***id + Q.subst( + ( + Map( + (Dereference(lhs) -> Left(eval(assign.expression, state, true))), + (Dereference(lhs.toGamma(state)) -> Left(rhsGamma)) ), state ) @@ -286,6 +357,18 @@ object Exec { VarAccess(mem.toGamma(state), Id.getAddr(v.ident, state)) else v case id: IdAccess => id.toVar(state).copy(index = eval(id.index, state, memAccess)) + 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, VarAccess(memId, Lit(state.addrs.get(v.ident).get))) + case d @ _ => d + } + case r @ Reference(id) => + r.copy(ident = eval(r.ident, state, false)) match { + case Reference(v: Var) => Lit(state.addrs.get(v.ident).get) + 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)) @@ -476,7 +559,7 @@ object Exec { def guar(a: Assignment, state: State) = { val guar = eval(state.guar, state, false) 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 subst = vars.map(v => List(v -> Left(v.toNought), v.toPrime(state) -> Left(v))).flatten.toMap[Expression, Left[Expression, Nothing]] /* val subst = Map( (Id.memId.toVar(state) -> Left(Id.memId.toVar(state).toNought)), @@ -484,7 +567,7 @@ object Exec { ) */ val gPrime = guar.subst((subst, state)) - val _subst = Map(Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) + val _subst = Map[Expression, Left[Expression, Nothing]](Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) // val _subst = vars.map(v => v.toNought -> Left(v)).toMap // val _subst = Map(Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) wp(eval(gPrime, state, true), a, state).subst((_subst, state)) @@ -503,9 +586,9 @@ object Exec { 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 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 = vars.map(v => v.toNought.asInstanceOf[Var] -> Left(v)).toMap + val _subst = vars.map(v => v.toNought.asInstanceOf[Var] -> Left(v)).toMap[Expression, Left[Expression, Nothing]] wp(gPrime, a, state).subst((_subst, state)) } @@ -524,7 +607,7 @@ object Exec { .toList ++ expEval.arrays .map(a => { - val subst = Map[Var, Left[Expression, Nothing]](Id.indexId.toVar(state) -> Left(eval(a.index, state, false))) + val subst = Map[Expression, Left[Expression, Nothing]](Id.indexId.toVar(state) -> Left(eval(a.index, state, false))) eval( BinOp.pred("||", a.toGamma(state), getL(a.ident, state)).subst((subst, state)), state, diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index e0bba1b..f65ba33 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -23,7 +23,7 @@ case class Lit(arg: Int) extends Expression { override def vars = Set() override def ids = Set() override def arrays = Set() - override def subst(su: Subst): Lit = this + override def subst(su: Subst) = this override def expType = TInt } @@ -149,18 +149,24 @@ case class VarAccess(name: Var, index: Expression) extends Variable { su._1 .filter { - case (v, Left(_)) => + 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 _ => throw new Error("Unexpected subst") } .foldLeft(memId: Expression) { - case (p, (v, Left(e))) => { + case (p, (v: Var, Left(e))) => { // TODO handle _i this.index match { - case _ if v == Id.indexId.toVar(su._2) => p + case _ if v.ident == Id.indexId => p case Lit(n) if (su._2.addrs.get(v.ident.getBase).get != n) => p case _ if (name.index != v.index) => p case _ => @@ -169,6 +175,13 @@ case class VarAccess(name: Var, index: Expression) extends Variable { VarStore(p, Lit(su._2.addrs.get(v.ident.getBase).get), 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 _ => + VarStore(p, VarAccess(Id.memId.toVar(su._2), Lit(su._2.addrs.get(v.ident).get)), e) + } } } @@ -265,7 +278,7 @@ case class ForAll(bound: Set[_ <: Expression], body: Expression) extends Express override def expType = TBool } -case class Dereference(ident: Id) extends Expression { +case class Dereference(ident: Expression) extends Expression { def this(x: String) = this(Id(x, TInt, false, false, false)) override def vars = ident.vars override def ids = ident.ids @@ -278,7 +291,7 @@ case class Dereference(ident: Id) extends Expression { } } -case class Reference(ident: Id) extends Expression { +case class Reference(ident: Expression) extends Expression { def this(x: String) = this(Id(x, TInt, false, false, false)) override def vars = ident.vars override def ids = ident.ids diff --git a/wptool/src/wptool/Parser.grammar b/wptool/src/wptool/Parser.grammar index 40eb274..a3007f2 100644 --- a/wptool/src/wptool/Parser.grammar +++ b/wptool/src/wptool/Parser.grammar @@ -126,6 +126,7 @@ 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); :} + | 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); :} diff --git a/wptool/src/wptool/Statement.scala b/wptool/src/wptool/Statement.scala index 5daec4a..e30d5a7 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, TInt, 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)) diff --git a/wptool/src/wptool/WPTool.scala b/wptool/src/wptool/WPTool.scala index 08a2c36..c7aac7d 100644 --- a/wptool/src/wptool/WPTool.scala +++ b/wptool/src/wptool/WPTool.scala @@ -149,7 +149,7 @@ object WPTool { // TODO Low?? i.toGamma.toVar(_state) -> Left(gamma.getOrElse(i, High).toTruth) } - }.toMap ++ 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) diff --git a/wptool/src/wptool/package.scala b/wptool/src/wptool/package.scala index 91adfbe..3c89ff1 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)]], State) + type Subst = (Map[Expression, Either[Expression, (Expression, Expression)]], State) val sub = "₀₁₂₃₄₅₆₇₈₉" implicit class StringOps(self: String) { From acc779dfa612ff7a3936326cd053b5d21d071192 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Mon, 15 Feb 2021 14:33:32 +1000 Subject: [PATCH 14/25] Fix typing errors --- wptool/src/wptool/Expression.scala | 24 ++++----- wptool/src/wptool/SMT.scala | 2 +- wptool/src/wptool/SMT_.scala | 79 ++++++++++++++++++------------ 3 files changed, 60 insertions(+), 45 deletions(-) diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index f65ba33..2363548 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -130,7 +130,9 @@ case class VarAccess(name: Var, index: Expression) extends Variable { // TODO document/comment def subst(su: Subst) = { - val updatedArr = this.copy(index = index.subst(su)) + // TODO not happy with filter + // println(s"$index -> ${index.subst((su._1.filter { case (v, _) => v.expType == TInt }, su._2))}") + 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))) => @@ -172,6 +174,7 @@ case class VarAccess(name: Var, index: Expression) extends Variable { case _ => // val memId = v.ident.copy(name = Id.memId.name) // VarStore(p, Lit(su._2.addrs.get(v.ident.getBase).get), e) + // VarStore(p, Lit(su._2.addrs.get(v.ident.getBase).get), e) } } @@ -180,7 +183,8 @@ case class VarAccess(name: Var, index: Expression) extends Variable { case _ if v.ident == Id.indexId => p case _ if (name.index != v.index) => p case _ => - VarStore(p, VarAccess(Id.memId.toVar(su._2), Lit(su._2.addrs.get(v.ident).get)), e) + val memId = v.ident.copy(name = Id.memId.name).toVar(su._2) + VarStore(p, VarAccess(memId.copy(ident = memId.ident.copy(gamma = false)), Lit(su._2.addrs.get(v.ident.getBase).get)), e) } } @@ -205,16 +209,6 @@ case class VarStore(array: Expression, index: Expression, exp: Expression) exten 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 PreOp(op: String, override val expType: Type, argType: Type, arg: Expression) extends Expression { override def toString: String = "(" + op + " " + arg + ")" override def vars = arg.vars @@ -285,9 +279,11 @@ case class Dereference(ident: Expression) extends Expression { override def arrays = ident.arrays override def subst(su: Subst) = Dereference(ident.subst(su)) + // TODO override def expType = ident.expType match { - case TPointer(t) => t - case _ => throw new Error("Invalid pointer type") + case TPointer(t) => t + case TInt | TBool => ident.expType + case _ => throw new Error("Invalid pointer type") } } diff --git a/wptool/src/wptool/SMT.scala b/wptool/src/wptool/SMT.scala index 4f15bf0..57b6bd6 100644 --- a/wptool/src/wptool/SMT.scala +++ b/wptool/src/wptool/SMT.scala @@ -5,7 +5,7 @@ import com.microsoft.z3.BoolExpr import com.microsoft.z3.enumerations.Z3_decl_kind import scala.reflect.runtime.universe.{TypeTag, typeOf} -object SMT { +object SMT_ { val intSize = 32 // size of bitvectors used val cfg = new java.util.HashMap[String, String]() val ctx = new z3.Context(cfg) diff --git a/wptool/src/wptool/SMT_.scala b/wptool/src/wptool/SMT_.scala index b214bdc..0595a4c 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_ { +object SMT { + type array = api.ArrayFormula[api.NumeralFormula.IntegerFormula, _ <: api.Formula] val solver = Solvers.CVC4 val ctx = SolverContextFactory.createSolverContext(solver) val fmgr = ctx.getFormulaManager(); @@ -78,17 +80,6 @@ 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 == TBool) { @@ -112,26 +103,51 @@ object SMT_ { case _ => throw new Error("Unexpected statement in VarStore") } - // TODO is this necessary (i.e. do we ever actually get nested stores) - 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 == 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 { @@ -176,7 +192,8 @@ object SMT_ { makeSelect(x.name.toString, x.index, true, expectIds).asInstanceOf[api.BooleanFormula] 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") } @@ -202,12 +219,14 @@ object SMT_ { 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 == 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] /* From bd8afeca4487a72f9e3eaba76d8e4f94404cf1f3 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Tue, 16 Feb 2021 14:18:16 +1000 Subject: [PATCH 15/25] More pointers - Implement pointers - Fix smt stuff - Being adding objects --- tests/rg/{TODO => _TODO} | 0 tests/rg/neg/pointers1 | 13 ++++ tests/rg/neg/pointers2 | 19 ++++++ tests/rg/neg/pointers3 | 22 ++++++ tests/rg/neg/pointers4 | 21 ++++++ tests/rg/neg/pointers5 | 21 ++++++ tests/rg/neg/pointers6 | 15 +++++ tests/rg/pointers2 | 21 ++++++ tests/rg/pointers3 | 21 ++++++ tests/rg/pointers4 | 21 ++++++ tests/rg/treiber/put | 18 +++++ wptool/src/wptool/Exec.scala | 105 +++++++---------------------- wptool/src/wptool/Expression.scala | 55 +++++++++------ wptool/src/wptool/Parser.grammar | 15 ++++- wptool/src/wptool/SMT.scala | 2 +- wptool/src/wptool/SMT_.scala | 2 +- wptool/src/wptool/Scanner.flex | 5 +- wptool/src/wptool/State.scala | 26 ++++--- wptool/src/wptool/VarDef.scala | 29 ++++++-- 19 files changed, 311 insertions(+), 120 deletions(-) rename tests/rg/{TODO => _TODO} (100%) create mode 100644 tests/rg/neg/pointers1 create mode 100644 tests/rg/neg/pointers2 create mode 100644 tests/rg/neg/pointers3 create mode 100644 tests/rg/neg/pointers4 create mode 100644 tests/rg/neg/pointers5 create mode 100644 tests/rg/neg/pointers6 create mode 100644 tests/rg/pointers2 create mode 100644 tests/rg/pointers3 create mode 100644 tests/rg/pointers4 create mode 100644 tests/rg/treiber/put 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/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..f9aa576 --- /dev/null +++ b/tests/rg/neg/pointers3 @@ -0,0 +1,22 @@ +global var a: +_L: FALSE +_PT: b + +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 +*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/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/treiber/put b/tests/rg/treiber/put new file mode 100644 index 0000000..0499210 --- /dev/null +++ b/tests/rg/treiber/put @@ -0,0 +1,18 @@ +global object n: +_Fields: val, level, next + +global object head: +_Fields: val, level + +_Rely: TRUE +_Guar: (n.level == 0) => (n'.level == 0) + +n.level = 1; +n.val = v; + +do { + ss := &val; + n.next = ss; +} +while(!CAS(head, ss, n)) + diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 5f838fb..a53230a 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -118,15 +118,15 @@ 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 } @@ -390,7 +390,7 @@ object Exec { expr } - def getBaseVars(vars: Set[Var]): Set[Var] = vars.map(v => v.getBase.resetIndex) + def getBaseVars(vars: Set[Variable]): Set[Variable] = vars.map(v => v.getBase.resetIndex) def getBaseArrays(vars: Set[VarAccess]): Set[VarAccess] = vars.filter(v => v.name.ident.getBase != Id.memId).map(v => v.getBase.resetIndex) def getBaseMems(vars: Set[VarAccess]): Set[VarAccess] = vars.filter(v => v.name.ident.getBase == Id.memId).map(v => v.getBase.resetIndex) @@ -408,7 +408,7 @@ object Exec { constructForall( getBaseVars(evalExp.vars - Id.indexId.toVar(state)) .map(v => { - if (state.globals.contains(v.ident)) { + if (state.globals.contains(v.ident) || v.ident.getBase == Id.memId) { // BinOp( // "&&", BinOp.pred( @@ -428,58 +428,6 @@ object Exec { } }) .toList - ++ - getBaseArrays(evalExp.arrays) - .map(v => { - val pred = if (state.globals.contains(v.ident)) { - // BinOp( - // "&&", - BinOp.pred( - "=>", - BinOp("==", TInt, 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("==", TInt, TBool, v, v.toPrime(state)), - BinOp.pred("==", v.toGamma(state), v.toPrime(state).toGamma(state)) - ) - } - - BinOp.pred( - "&&", - pred, - eval(state.arrRelys.getOrElse(v.ident, Const._true), state, false) - .subst((Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, false))), state)) - ) - - }) - .toList - ++ getBaseMems(evalExp.arrays) - .map(v => { - val pred = - // BinOp( - // "&&", - BinOp.pred( - "=>", - BinOp("==", TInt, 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)) - // ) - - BinOp.pred( - "&&", - pred, - eval(state.arrRelys.getOrElse(v.ident, Const._true), state, false) - .subst((Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, false))), state)) - ) - - }) - .toList ), eval(state.rely, state, false) ), @@ -489,9 +437,20 @@ object Exec { p } - 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 _: IdAccess | _: VarAccess => + id match { + case id: IdAccess => + getL(id.ident, state).subst( + (Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true))), state) + ) + case id: VarAccess => + getL(id.ident, state).subst( + (Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true))), state) + ) + } + case id: Id => eval( state.L.getOrElse(id, throw new Error("L not defined for " + id)), state, @@ -499,14 +458,6 @@ object Exec { ) } - def getL(id: IdAccess, state: State): Expression = - getL(id.ident, state) - .subst((Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true))), state)) - - def getL(v: VarAccess, state: State): Expression = - getL(v.ident, state) - .subst((Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, true))), state)) - def primed(p: Expression, state: State) = // TODO handle memId eval(p, state, false).subst( @@ -558,7 +509,7 @@ object Exec { def guar(a: Assignment, state: State) = { val guar = eval(state.guar, state, false) - val vars = getBaseVars(guar.vars ++ guar.arrays.map(a => a.name)) + 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 subst = Map( @@ -585,7 +536,7 @@ object Exec { state, true ) - val vars = getBaseVars(guar.vars ++ guar.arrays.map(a => a.name)) + 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 = vars.map(v => v.toNought.asInstanceOf[Var] -> Left(v)).toMap[Expression, Left[Expression, Nothing]] @@ -604,17 +555,7 @@ object Exec { true ) // Default to high ) - .toList ++ - expEval.arrays - .map(a => { - val subst = Map[Expression, Left[Expression, Nothing]](Id.indexId.toVar(state) -> Left(eval(a.index, state, false))) - eval( - BinOp.pred("||", a.toGamma(state), getL(a.ident, state)).subst((subst, state)), - state, - true - ) // Default to high - }) - .toList + .toList ) } diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index 2363548..5d3a3ed 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -9,12 +9,10 @@ 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 } @@ -22,7 +20,6 @@ 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) = this override def expType = TInt } @@ -49,7 +46,6 @@ case class Id(name: String, override val expType: Type, prime: Boolean, gamma: B (if (gamma) "Gamma_" 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) @@ -85,7 +81,6 @@ 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._1.get(this) match { case Some(Left(e: Expression)) => e case Some(Right(_)) => @@ -111,7 +106,6 @@ case class IdAccess(ident: Id, index: Expression) extends Expression with Identi def this(name: String, prime: Boolean, gamma: Boolean, index: Expression) = this(Id(name, 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 subst(su: Subst) = throw new Error("tried to subst var id") override def toString = ident + "[" + index + "]" def toGamma = this.copy(ident = ident.toGamma) @@ -124,9 +118,8 @@ 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 + name + def ids = index.ids + name.ident // TODO document/comment def subst(su: Subst) = { @@ -195,7 +188,7 @@ case class VarAccess(name: Var, index: Expression) extends Variable { 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) @@ -204,16 +197,43 @@ 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 ObjIdAccess(ident: Id, field: String) extends Expression with Identifier { + 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 toVar(state: State) = ObjVarAccess(ident.toVar(state), field) + def getBase = this.copy(ident = ident.getBase) +} + +case class ObjVarAccess(name: Var, field: String) extends Expression with Variable { + def vars = Set(this) + def ids = Set(this.ident) + def subst(su: Subst) = throw new Error("tried to subst var id") + 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 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)) } @@ -221,7 +241,6 @@ case class PostOp(op: String, override val expType: Type, argType: Type, arg: Ex 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)) } @@ -229,7 +248,6 @@ case class BinOp(op: String, override val expType: Type, argType: Type, arg1: Ex 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)) } @@ -246,7 +264,6 @@ 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 = TBool } @@ -257,7 +274,6 @@ case class CompareAndSwap(x: Id, e1: Expression, e2: Expression) extends Express 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 = TInt // TODO } @@ -266,7 +282,6 @@ case class ForAll(bound: Set[_ <: Expression], body: Expression) extends Express 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 = TBool @@ -276,7 +291,6 @@ case class Dereference(ident: Expression) extends Expression { def this(x: String) = this(Id(x, TInt, false, false, false)) override def vars = ident.vars override def ids = ident.ids - override def arrays = ident.arrays override def subst(su: Subst) = Dereference(ident.subst(su)) // TODO @@ -291,7 +305,6 @@ case class Reference(ident: Expression) extends Expression { def this(x: String) = this(Id(x, TInt, false, false, false)) override def vars = ident.vars override def ids = ident.ids - override def arrays = ident.arrays 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 a3007f2..875564b 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 FIELDS; //%terminals RETURN, BREAK, CONTINUE; %terminals IF, ELSE, WHILE, DO; @@ -34,6 +36,7 @@ %terminals CAS; %terminals INVARIANT, GAMMA, GAMMA_0, RELY, GUAR; %terminals LPRED; +%terminals PT; %terminals MAPSTO; %terminals PRIMEGAMMAID; %terminals PRIMEID; @@ -100,7 +103,8 @@ ptrdef ; vardef - = 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 lpred.l {: return new VarDef(n, l, GlobalVar.instance()); :} + | GLOBALVAR ID.n COLON lpred.l PT COLON id_list.p {: return new VarDef(n, l, p, GlobalVar.instance()); :} | GLOBALVAR ID.n COLON {: return new VarDef(n, GlobalVar.instance()); :} | LOCALVAR ID.n COLON {: return new VarDef(n, LocalVar.instance()); :} | ptrdef.n COLON {: return new VarDef(n.name().name(), GlobalVar.instance()); :} // TODO @@ -113,6 +117,7 @@ definition | 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 FIELDS COLON id_list.i {: return new ObjDef(n, i, GlobalVar.instance()); :} ; arrrely = RELY COLON boolexpr.a {: return new Rely(a); :}; @@ -162,6 +167,8 @@ boolexpr | 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"); :} @@ -184,12 +191,12 @@ intexpr | 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); :} ; ptrexpr // TODO = ID.n {: return new Id(n, new TPointer(TInt.instance()), false, false, false) :} = AMP ID.n {: return new Reference(n); :} - | STAR ID.n {: return new Dereference(n); :} ; // for _L(x): pred construction to set predicate for variable security level @@ -213,3 +220,7 @@ security = LOW {: return Low.instance(); :} | HIGH {: return High.instance(); :} ; + +id_list + = ID + | id_list COMMA ID; diff --git a/wptool/src/wptool/SMT.scala b/wptool/src/wptool/SMT.scala index 57b6bd6..4f15bf0 100644 --- a/wptool/src/wptool/SMT.scala +++ b/wptool/src/wptool/SMT.scala @@ -5,7 +5,7 @@ import com.microsoft.z3.BoolExpr import com.microsoft.z3.enumerations.Z3_decl_kind import scala.reflect.runtime.universe.{TypeTag, typeOf} -object SMT_ { +object SMT { val intSize = 32 // size of bitvectors used val cfg = new java.util.HashMap[String, String]() val ctx = new z3.Context(cfg) diff --git a/wptool/src/wptool/SMT_.scala b/wptool/src/wptool/SMT_.scala index 0595a4c..494f5cf 100644 --- a/wptool/src/wptool/SMT_.scala +++ b/wptool/src/wptool/SMT_.scala @@ -7,7 +7,7 @@ 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 { +object SMT_ { type array = api.ArrayFormula[api.NumeralFormula.IntegerFormula, _ <: api.Formula] val solver = Solvers.CVC4 val ctx = SolverContextFactory.createSolverContext(solver) diff --git a/wptool/src/wptool/Scanner.flex b/wptool/src/wptool/Scanner.flex index debb4b7..6232290 100644 --- a/wptool/src/wptool/Scanner.flex +++ b/wptool/src/wptool/Scanner.flex @@ -109,6 +109,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 +118,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); } +"_Fields" { return newToken(Terminals.FIELDS); } "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 ab3152d..e9ea6a2 100644 --- a/wptool/src/wptool/State.scala +++ b/wptool/src/wptool/State.scala @@ -9,9 +9,9 @@ case class State( debug: Boolean, silent: Boolean, simplify: Boolean, - controls: Set[Id], - controlled: Set[Id], - controlledBy: Map[Id, Set[Id]], // TODO check + controls: Set[Identifier], + controlled: Set[Identifier], + controlledBy: Map[Identifier, Set[Identifier]], // TODO check L: Map[Id, Expression], ids: Set[Id], arrayIds: Set[Id], @@ -22,6 +22,7 @@ case class State( arrGuars: Map[Id, Expression], indicies: Map[Id, Int], addrs: Map[Id, Int], + pointsTo: Map[Id, Set[Id]], error: Boolean = false ) { def incPrimeIndicies = @@ -46,9 +47,9 @@ 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 => @@ -68,15 +69,17 @@ 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 _ => 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 @@ -90,6 +93,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( @@ -145,7 +154,8 @@ object State { arrRelys, arrGuars, indicies, - addrs + addrs, + pointsTo ) } } diff --git a/wptool/src/wptool/VarDef.scala b/wptool/src/wptool/VarDef.scala index 98d27d7..685e899 100644 --- a/wptool/src/wptool/VarDef.scala +++ b/wptool/src/wptool/VarDef.scala @@ -92,11 +92,15 @@ 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, TInt, false, false, false), pred, access) + this(new Id(name, TInt, 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), pred, pointsTo.toList.map(v => Id(v, TInt, false, false, false)), access) def this(name: String, access: Access) = - this(new Id(name, TInt, false, false, false), Const._true, access) + this(new Id(name, TInt, false, false, false), Const._true, List(), access) + def this(name: String, pointsTo: Array[String], access: Access) = + this(new Id(name, TInt, false, false, false), Const._true, pointsTo.toList.map(v => Id(v, TInt, false, false, false)), access) } case class ArrayDef( @@ -139,7 +143,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 +152,20 @@ object ArrayDef { yield lpred } } + +case class ObjDef( + name: Id, + fields: List[Id], + access: Access +) extends Definition { + def this( + name: String, + fields: Array[String], + access: Access + ) = + this( + new Id(name, TInt, false, false, false), + fields.map(i => new Id(i, TInt, false, false, false)).toList, + access + ) +} From 6fff56f12e2fee9a0dd6e9967feb3cd995879ee5 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Tue, 16 Feb 2021 14:55:58 +1000 Subject: [PATCH 16/25] Fix handling of array relys --- wptool/src/wptool/Exec.scala | 32 ++++++++++++++++++++++++------ wptool/src/wptool/Expression.scala | 10 +++++----- 2 files changed, 31 insertions(+), 11 deletions(-) diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index a53230a..1541dba 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -390,10 +390,16 @@ object Exec { expr } - def getBaseVars(vars: Set[Variable]): Set[Variable] = vars.map(v => v.getBase.resetIndex) - def getBaseArrays(vars: Set[VarAccess]): Set[VarAccess] = - vars.filter(v => v.name.ident.getBase != Id.memId).map(v => v.getBase.resetIndex) - def getBaseMems(vars: Set[VarAccess]): Set[VarAccess] = vars.filter(v => v.name.ident.getBase == Id.memId).map(v => v.getBase.resetIndex) + def getBaseVars(vars: Set[Variable]): Set[Variable] = vars.map(v => + v.getBase.resetIndex match { + case v: VarAccess => v.name + case v @ _ => v + } + ) + def getBaseVariables(vars: Set[Variable]): Set[Variable] = vars.map(v => v.getBase.resetIndex) + // def getBaseArrays(vars: Set[VarAccess]): Set[VarAccess] = + // vars.filter(v => v.name.ident.getBase != Id.memId).map(v => v.getBase.resetIndex) + // def getBaseMems(vars: Set[VarAccess]): Set[VarAccess] = vars.filter(v => v.name.ident.getBase == Id.memId).map(v => v.getBase.resetIndex) def getRely(exp: Expression, state: State) = { val evalExp = eval(exp, state, false) @@ -402,13 +408,14 @@ object Exec { // rely incorrect as using mem for rely not var itself // TODO should local vars not be loaded into memeory (????) // related: how will the rely work for pointers ?!?? + val p = 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) || v.ident.getBase == Id.memId) { + val pred = if (state.globals.contains(v.ident) || v.ident.getBase == Id.memId) { // BinOp( // "&&", BinOp.pred( @@ -426,6 +433,19 @@ object Exec { ) } + + 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, false) + .subst((Map(Id.indexId.toVar(state) -> Left(eval(v.index, state, false))), state)) + ) + + case _ => pred + } }) .toList ), diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index 5d3a3ed..3f331c5 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -104,8 +104,8 @@ 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, TInt, false, false, false), index) def this(name: String, prime: Boolean, gamma: Boolean, index: Expression) = this(Id(name, TInt, prime, gamma, false), index) - def vars = index.vars - def ids = index.ids + 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) @@ -118,8 +118,8 @@ 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 + name - def ids = index.ids + name.ident + def vars = index.vars + this + def ids = index.ids + this.ident // TODO document/comment def subst(su: Subst) = { @@ -155,7 +155,7 @@ case class VarAccess(name: Var, index: Expression) extends Variable { 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 _ => throw new Error("Unexpected subst") + case s @ _ => throw new Error(s"Unexpected subst ($s)") } .foldLeft(memId: Expression) { case (p, (v: Var, Left(e))) => { From 359b27ab7055779cbded7def0d2e835fe529a83d Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Wed, 17 Feb 2021 08:58:29 +1000 Subject: [PATCH 17/25] More pointers/objects --- tests/rg/treiber/put | 12 +++++++----- wptool/src/wptool/Exec.scala | 4 +++- wptool/src/wptool/Expression.scala | 1 + wptool/src/wptool/Parser.grammar | 13 +++++++++++-- wptool/src/wptool/Scanner.flex | 2 +- wptool/src/wptool/State.scala | 1 + wptool/src/wptool/VarDef.scala | 3 +++ 7 files changed, 27 insertions(+), 9 deletions(-) diff --git a/tests/rg/treiber/put b/tests/rg/treiber/put index 0499210..914767b 100644 --- a/tests/rg/treiber/put +++ b/tests/rg/treiber/put @@ -1,7 +1,7 @@ -global object n: +global obj n: _Fields: val, level, next -global object head: +global obj head: _Fields: val, level _Rely: TRUE @@ -10,9 +10,11 @@ _Guar: (n.level == 0) => (n'.level == 0) n.level = 1; n.val = v; -do { - ss := &val; +do +_invariant: TRUE +{ + ss = &val; n.next = ss; } -while(!CAS(head, ss, n)) +while(CAS(head, ss, n) == 0) diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 1541dba..9eae761 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -356,7 +356,9 @@ object Exec { else if (memAccess && v.ident.gamma) VarAccess(mem.toGamma(state), Id.getAddr(v.ident, state)) else v - case id: IdAccess => id.toVar(state).copy(index = eval(id.index, state, memAccess)) + case id: IdAccess => id.toVar(state).copy(index = eval(id.index, state, memAccess)) + case idObj: ObjIdAccess => idObj // TODO + case varObj: ObjVarAccess => varObj case deref @ Dereference(id) => deref.copy(ident = eval(deref.ident, state, false)) match { case Dereference(v: Var) if (memAccess) => diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index 3f331c5..3d4d009 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -202,6 +202,7 @@ case class VarStore(array: Expression, index: Expression, exp: Expression) exten } case class ObjIdAccess(ident: Id, field: String) extends Expression with Identifier { + def this(name: String, field: String) = this(Id(name, TInt, 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") diff --git a/wptool/src/wptool/Parser.grammar b/wptool/src/wptool/Parser.grammar index 875564b..62aadf9 100644 --- a/wptool/src/wptool/Parser.grammar +++ b/wptool/src/wptool/Parser.grammar @@ -28,6 +28,7 @@ %terminals AND; %terminals OR; %terminals COLON; +%terminals DOT; %terminals ASG; %terminals COMMA, SEMICOLON; %terminals FORALL; @@ -73,6 +74,7 @@ %typeof boolexpr = "Expression"; %typeof intexpr = "Expression"; %typeof ptrexpr = "Expression"; +%typeof intid = "Id"; %typeof local = "Stmt"; @@ -131,6 +133,8 @@ 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); :} @@ -174,10 +178,14 @@ boolexpr | FALSE {: return new Const("False"); :} ; +intid + = PRIMEID.n {: return new Id(n, TInt.instance(), true, false, false); :} + | ID.n {: return new Id(n, TInt.instance(), false, false, false); :} + ; + intexpr = PREFIX | POSTFIX /* unused */ - | PRIMEID.n {: return new Id(n, TInt.instance(), true, false, false); :} - | ID.n {: return new Id(n, TInt.instance(), 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 @@ -192,6 +200,7 @@ intexpr | 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 diff --git a/wptool/src/wptool/Scanner.flex b/wptool/src/wptool/Scanner.flex index 6232290..57bb81d 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); } diff --git a/wptool/src/wptool/State.scala b/wptool/src/wptool/State.scala index e9ea6a2..7678d93 100644 --- a/wptool/src/wptool/State.scala +++ b/wptool/src/wptool/State.scala @@ -73,6 +73,7 @@ object State { 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") } diff --git a/wptool/src/wptool/VarDef.scala b/wptool/src/wptool/VarDef.scala index 685e899..2245850 100644 --- a/wptool/src/wptool/VarDef.scala +++ b/wptool/src/wptool/VarDef.scala @@ -153,6 +153,7 @@ object ArrayDef { } } +// TODO L!!! case class ObjDef( name: Id, fields: List[Id], @@ -168,4 +169,6 @@ case class ObjDef( fields.map(i => new Id(i, TInt, false, false, false)).toList, access ) + + def toVarDefs: VarDef = VarDef(name, Const._true, List(), access) } From 4085b909d12fb124bc94de1f530407c5c0a32e9c Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Wed, 17 Feb 2021 13:31:58 +1000 Subject: [PATCH 18/25] Fixed vc for pointers --- tests/rg/neg/pointers3 | 4 +- wptool/src/wptool/Exec.scala | 63 +++++++++++++++++------------- wptool/src/wptool/Expression.scala | 3 +- wptool/src/wptool/Parser.grammar | 11 +++--- 4 files changed, 45 insertions(+), 36 deletions(-) diff --git a/tests/rg/neg/pointers3 b/tests/rg/neg/pointers3 index f9aa576..652feb8 100644 --- a/tests/rg/neg/pointers3 +++ b/tests/rg/neg/pointers3 @@ -1,9 +1,9 @@ global var a: _L: FALSE -_PT: b -global var b: +global var *b: _L: FALSE +_PT: a global var out: _L: a == 2 diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 9eae761..04fac77 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -132,32 +132,41 @@ object Exec { } case assign @ Assignment(Dereference(id), _, _) => // TODO preds - /* - val globalPred = - if (state.globals.contains(id)) - BinOp.pred( + 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) ) - else Const._true - */ - /* - val controlPred = if (state.controls.contains(id)) { - constructForall( - state.controlledBy - .getOrElse(id, Set()) - .map(contr => { - BinOp.pred( - "=>", - eval(getL(contr, state).subst((Map(id.toVar(state) -> Left(assign.expression)), state)), state, true), // TODO - BinOp.pred("||", eval(contr.toGamma, state, true), getL(contr, state)) - ) - }) - .toList - ) - } else Const._true - */ + + // Check if anything that b points to is a control variable + // TODO move check to inside map (i.e. only check secUpd if necessary + 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), // TODO + BinOp.pred("||", eval(contr.toGamma, state, true), getL(contr, state)) + ) + ) + }) + .flatten + .toList + ) + case _ => throw new Error("Expected id") + + } val _state = evalWp(assign, state, RG) @@ -166,16 +175,16 @@ 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(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, "Global"), - // new PredInfo(controlPred, assign, "Control") + new PredInfo(globalPred, assign, "L => G"), + new PredInfo(controlPred, assign, "secUpd") ) .incPrimeIndicies } diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index 3d4d009..c227660 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -290,6 +290,7 @@ case class ForAll(bound: Set[_ <: Expression], body: Expression) extends Express case class Dereference(ident: Expression) extends Expression { def this(x: String) = this(Id(x, TInt, 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)) @@ -304,9 +305,9 @@ case class Dereference(ident: Expression) extends Expression { case class Reference(ident: Expression) extends Expression { def this(x: String) = this(Id(x, TInt, 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 62aadf9..79cc058 100644 --- a/wptool/src/wptool/Parser.grammar +++ b/wptool/src/wptool/Parser.grammar @@ -105,12 +105,11 @@ ptrdef ; vardef - = GLOBALVAR ID.n COLON lpred.l {: return new VarDef(n, l, GlobalVar.instance()); :} - | GLOBALVAR ID.n COLON lpred.l PT COLON id_list.p {: return new VarDef(n, l, p, GlobalVar.instance()); :} - | GLOBALVAR ID.n COLON {: return new VarDef(n, GlobalVar.instance()); :} - | LOCALVAR ID.n COLON {: return new VarDef(n, LocalVar.instance()); :} - | ptrdef.n COLON {: return new VarDef(n.name().name(), GlobalVar.instance()); :} // TODO - | ptrdef.n COLON lpred.l {: return new VarDef(n.name().name(), l, GlobalVar.instance()); :} // TODO + = 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 From 66ffc154be59d6ebcb06ddcf8f52788182aede5a Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Wed, 17 Feb 2021 13:41:49 +1000 Subject: [PATCH 19/25] Remove fixed/unnecessary TODOs --- wptool/src/wptool/Exec.scala | 23 ++++------------------- wptool/src/wptool/Expression.scala | 1 - 2 files changed, 4 insertions(+), 20 deletions(-) diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 04fac77..9bb389b 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -23,7 +23,6 @@ object Exec { block.children.map(c => { val res = exec(c, state) if (c.atomic) - // TODO change this to R implies res.copy(Qs = res.Qs.map(q => q.copy(pred = rImplies(q.pred, state)))) else res }), @@ -102,7 +101,7 @@ object Exec { .map(contr => { BinOp.pred( "=>", - eval(getL(contr, state).subst((Map(lhs.toVar(state) -> Left(assign.expression)), state)), state, true), // TODO + 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)) ) }) @@ -131,7 +130,6 @@ object Exec { .incPrimeIndicies } case assign @ Assignment(Dereference(id), _, _) => - // TODO preds var globalPred: Expression = null var controlPred: Expression = null id match { @@ -144,7 +142,6 @@ object Exec { ) // Check if anything that b points to is a control variable - // TODO move check to inside map (i.e. only check secUpd if necessary controlPred = constructForall( state.pointsTo .get(id) @@ -156,7 +153,7 @@ object Exec { .map(contr => BinOp.pred( "=>", - eval(getL(contr, state).subst((Map(i.toVar(state) -> Left(assign.expression)), state)), state, true), // TODO + 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)) ) ) @@ -211,12 +208,12 @@ object Exec { getL(contr, state).subst((Map(assign.lhs.ident.toVar(state) -> Right((assign.lhs.index, assign.expression))), state)), state, true - ), // TODO + ), BinOp.pred( "||", eval(contr.toGamma, state, true), getL(contr, state).subst((Map(Id.indexId.toVar(state) -> Left(assign.lhs.index)), state)) - ) // TODO check subst is correct + ) ) }) .toList @@ -304,11 +301,6 @@ object Exec { case _ => throw new Error("Unexpected dereference") } - // TODO this is broken - // could make subst exp -> Either - // and then pass in Deref(id) and handle in subst - // this may be better as it is more general - // current approach doesnt work for multiple ***id Q.subst( ( Map( @@ -415,11 +407,6 @@ object Exec { def getRely(exp: Expression, state: State) = { val evalExp = eval(exp, state, false) - // TODO !!!! - // rely incorrect as using mem for rely not var itself - // TODO should local vars not be loaded into memeory (????) - // related: how will the rely work for pointers ?!?? - val p = eval( BinOp.pred( "&&", @@ -490,7 +477,6 @@ object Exec { } def primed(p: Expression, state: State) = - // TODO handle memId eval(p, state, false).subst( ( (state.arrayIds + Id.memId) @@ -500,7 +486,6 @@ object Exec { ) ) - // TODO take havoc statements into account def stableR(p: Expression, state: State) = eval( BinOp.pred("=>", BinOp.pred("&&", getRely(p, state), p), primed(p, state)), diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index c227660..83e4633 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -66,7 +66,6 @@ case class Id(name: String, override val expType: Type, prime: Boolean, gamma: B } object Id { - // TODO change to bool val tmpId = Id("tmp", TInt, false, false, false) val indexId = Id("_i", TInt, false, false, false) val memId = Id("mem", TInt, false, false, false) From 762d91347598cfdf384291f73969de6ba9460135 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Thu, 18 Feb 2021 16:09:27 +1000 Subject: [PATCH 20/25] Work on processing treiber stack THIS IS BROKEN --- README.md | 3 ++ tests/rg/treiber/put | 20 ++++++--- wptool/src/wptool/Exec.scala | 72 ++++++++++++++++++++++-------- wptool/src/wptool/Expression.scala | 67 ++++++++++++++++----------- wptool/src/wptool/Parser.grammar | 27 ++++++++--- wptool/src/wptool/Preprocess.scala | 11 +++-- wptool/src/wptool/SMT_.scala | 8 ++-- wptool/src/wptool/Scanner.flex | 2 +- wptool/src/wptool/State.scala | 28 +++++++++--- wptool/src/wptool/Statement.scala | 4 +- wptool/src/wptool/VarDef.scala | 31 ++++++++----- 11 files changed, 186 insertions(+), 87 deletions(-) diff --git a/README.md b/README.md index d4b9b4f..85f88b9 100644 --- a/README.md +++ b/README.md @@ -140,4 +140,7 @@ 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 + diff --git a/tests/rg/treiber/put b/tests/rg/treiber/put index 914767b..4fe2725 100644 --- a/tests/rg/treiber/put +++ b/tests/rg/treiber/put @@ -1,8 +1,18 @@ global obj n: -_Fields: val, level, next +_Field: val + _L: n.level == 1 +_Field: level + _L: TRUE +_Field: next + _L: TRUE -global obj head: -_Fields: val, level +global var *head: +_L: TRUE +_PT: n + +global var *ss: +_L: TRUE +_PT: head, n _Rely: TRUE _Guar: (n.level == 0) => (n'.level == 0) @@ -13,8 +23,8 @@ n.val = v; do _invariant: TRUE { - ss = &val; + ss = head; n.next = ss; } -while(CAS(head, ss, n) == 0) +while(CAS(head, ss, &n) == 0) diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 9bb389b..61670af 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -85,9 +85,9 @@ object Exec { } else { _state.incPrimeIndicies } - case assign @ Assignment(lhs: Id, _, _) => + case assign @ Assignment(lhs: Identifier, _, _) => val globalPred = - if (state.globals.contains(lhs)) + if (state.globals.contains(lhs.ident)) BinOp.pred( "=>", getL(lhs, state), @@ -310,6 +310,20 @@ object Exec { state ) ) + 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})") + } + + Q.subst( + Map( + (o.toVar(state) -> Left(eval(assign.expression, state, true))), + (o.toGamma.toVar(state) -> Left(rhsGamma)) + ), + state + ) case assign: ArrayAssignment => val rhsGamma = computeGamma(assign.expression, state) @@ -328,7 +342,7 @@ object Exec { ) ) case stmt => - println("Unhandled statement(wp exec): " + stmt) + println(s"Unhandled statement(wp exec): $stmt (${stmt.getClass})") Q } } @@ -339,10 +353,11 @@ object Exec { 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, Id.getAddr(id, state)) + VarAccess(mem, eval(Id.getAddr(id, state), state, true)) else if (memAccess && id.gamma) - VarAccess(mem.toGamma(state), Id.getAddr(id, state)) + VarAccess(mem.toGamma(state), eval(Id.getAddr(id, state), state, true)) else id.toVar(state) case id: Id => id.toVar(state) @@ -353,23 +368,35 @@ object Exec { else Id.memId.toVar(state)) if (v.ident == Id.indexId) v else if (memAccess && !v.ident.gamma) - VarAccess(mem, Id.getAddr(v.ident, state)) + VarAccess(mem, eval(Id.getAddr(v.ident, state), state, true)) else if (memAccess && v.ident.gamma) - VarAccess(mem.toGamma(state), Id.getAddr(v.ident, state)) + 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 => idObj // TODO - case varObj: ObjVarAccess => varObj + 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, VarAccess(memId, Lit(state.addrs.get(v.ident).get))) + 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) => Lit(state.addrs.get(v.ident).get) + case Reference(v: Var) => eval(state.addrs.get(v.ident).get, state, true) case r @ _ => r } case BinOp(op, t1, t2, arg1, arg2) => @@ -393,12 +420,17 @@ object Exec { expr } - def getBaseVars(vars: Set[Variable]): Set[Variable] = vars.map(v => - v.getBase.resetIndex match { - case v: VarAccess => v.name - case v @ _ => v + def getBaseVars(vars: Set[Variable]): Set[Variable] = vars + .filter { + case v: Var if (v.ident.memLoc) => false + case _ => true } - ) + .map(v => + v.getBase.resetIndex match { + case v: VarAccess => v.name + case v @ _ => v + } + ) def getBaseVariables(vars: Set[Variable]): Set[Variable] = vars.map(v => v.getBase.resetIndex) // def getBaseArrays(vars: Set[VarAccess]): Set[VarAccess] = // vars.filter(v => v.name.ident.getBase != Id.memId).map(v => v.getBase.resetIndex) @@ -456,7 +488,8 @@ object Exec { } def getL(id: Identifier, state: State): Expression = id match { - case Id.tmpId => Const._true + case Id.tmpId => Const._true + case id: Id if (id.memLoc) => Const._true case _: IdAccess | _: VarAccess => id match { case id: IdAccess => @@ -468,7 +501,7 @@ object Exec { (Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true))), state) ) } - case id: Id => + case id: Identifier => eval( state.L.getOrElse(id, throw new Error("L not defined for " + id)), state, @@ -537,6 +570,7 @@ object Exec { val _subst = Map[Expression, Left[Expression, Nothing]](Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) // val _subst = vars.map(v => v.toNought -> Left(v)).toMap // val _subst = Map(Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) + println(wp(eval(gPrime, state, true), a, state)) wp(eval(gPrime, state, true), a, state).subst((_subst, state)) } diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index 83e4633..d8e79b9 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -1,7 +1,5 @@ package wptool -import scala.reflect.runtime.universe.{TypeTag, typeOf} - sealed abstract class Type case class TPointer(pointerType: Type) extends Type case object TBool extends Type { def instance = this } @@ -29,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 { @@ -41,19 +40,20 @@ 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, 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 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, TBool, prime, true, nought) + def toGamma = Id(name, TBool, prime, true, nought, false) def getIndex(state: State) = { - if (!gamma) state.indicies.getOrElse(this, throw new Error(s"Index not found for var $this with type $expType")) + 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 = TInt), // TODO change TInt @@ -61,17 +61,19 @@ case class Id(name: String, override val expType: Type, prime: Boolean, gamma: B ) } + override def ident = this + // TODO use actual type - override def getBase = Id(name, TInt, false, false, false) + override def getBase = Id(name, TInt, false, false, false, false) } object Id { - val tmpId = Id("tmp", TInt, false, false, false) - val indexId = Id("_i", TInt, false, false, false) - val memId = Id("mem", 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): Lit = { - Lit(state.addrs.getOrElse(id.getBase, throw new Error("Couldn't resolve memeory address"))) + def getAddr(id: Id, state: State): Expression = { + state.addrs.getOrElse(id.getBase, throw new Error("Couldn't resolve memeory address")) } } @@ -101,8 +103,8 @@ 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, TInt, false, false, false), index) - def this(name: String, prime: Boolean, gamma: Boolean, index: Expression) = this(Id(name, TInt, prime, gamma, false), index) + 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") @@ -154,20 +156,21 @@ case class VarAccess(name: Var, index: Expression) extends Variable { 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)") + 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 Lit(n) if (su._2.addrs.get(v.ident.getBase).get != n) => p + case v: Var if (su._2.addrs.get(v.ident.getBase).get != v) => p case _ if (name.index != v.index) => p - case _ => - // val memId = v.ident.copy(name = Id.memId.name) - // VarStore(p, Lit(su._2.addrs.get(v.ident.getBase).get), e) - // - VarStore(p, Lit(su._2.addrs.get(v.ident.getBase).get), e) + case _ => VarStore(p, su._2.addrs.get(v.ident.getBase).get, e) } } case (p, (Dereference(v: Var), Left(e))) => @@ -176,7 +179,12 @@ case class VarAccess(name: Var, index: Expression) extends Variable { 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)), Lit(su._2.addrs.get(v.ident.getBase).get)), e) + VarStore(p, VarAccess(memId.copy(ident = memId.ident.copy(gamma = false)), su._2.addrs.get(v.ident.getBase).get), 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) } } @@ -201,7 +209,7 @@ case class VarStore(array: Expression, index: Expression, exp: Expression) exten } case class ObjIdAccess(ident: Id, field: String) extends Expression with Identifier { - def this(name: String, field: String) = this(Id(name, TInt, false, false, false), field) + 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") @@ -209,6 +217,7 @@ case class ObjIdAccess(ident: Id, field: String) extends Expression with Identif 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) @@ -217,7 +226,9 @@ case class ObjIdAccess(ident: Id, field: String) extends Expression with Identif case class ObjVarAccess(name: Var, field: String) extends Expression with Variable { def vars = Set(this) def ids = Set(this.ident) - def subst(su: Subst) = throw new Error("tried to subst var id") + 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)) @@ -225,6 +236,8 @@ case class ObjVarAccess(name: Var, field: String) extends Expression with Variab 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) @@ -270,7 +283,7 @@ case class Const(name: String) extends Expression { // 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, 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 @@ -288,7 +301,7 @@ case class ForAll(bound: Set[_ <: Expression], body: Expression) extends Express } case class Dereference(ident: Expression) extends Expression { - def this(x: String) = this(Id(x, TInt, false, false, false)) + 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 @@ -303,7 +316,7 @@ case class Dereference(ident: Expression) extends Expression { } case class Reference(ident: Expression) extends Expression { - def this(x: String) = this(Id(x, TInt, false, false, false)) + 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 diff --git a/wptool/src/wptool/Parser.grammar b/wptool/src/wptool/Parser.grammar index 79cc058..a029ed9 100644 --- a/wptool/src/wptool/Parser.grammar +++ b/wptool/src/wptool/Parser.grammar @@ -4,7 +4,7 @@ %terminals GLOBALVAR, LOCALVAR; %terminals GLOBALARRAY, LOCALARRAY; %terminals GLOBALOBJ; -%terminals FIELDS; +%terminals FIELD; //%terminals RETURN, BREAK, CONTINUE; %terminals IF, ELSE, WHILE, DO; @@ -89,6 +89,7 @@ %typeof arrrely = "Rely"; %typeof arrguar = "Guar"; %typeof security = "Security"; +%typeof fielddef = "Field"; %goal unit; @@ -104,6 +105,17 @@ ptrdef | 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()); :} @@ -118,7 +130,7 @@ definition | 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 FIELDS COLON id_list.i {: return new ObjDef(n, i, GlobalVar.instance()); :} + | GLOBALOBJ ID.n COLON fielddefs.f {: return new ObjDef(n, f, GlobalVar.instance()); :} ; arrrely = RELY COLON boolexpr.a {: return new Rely(a); :}; @@ -148,9 +160,9 @@ local locals = local *; boolexpr - = PRIMEGAMMAID.n {: return new Id(n, TBool.instance(), true, true, false); :} - | GAMMAID.n {: return new Id(n, TBool.instance(), false, true, false); :} - // | PRIMEID.n {: return new Id(n, TBool.instance(), true, 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); :} @@ -178,8 +190,8 @@ boolexpr ; intid - = PRIMEID.n {: return new Id(n, TInt.instance(), true, false, false); :} - | ID.n {: return new Id(n, TInt.instance(), false, false, false); :} + = 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 @@ -189,6 +201,7 @@ intexpr | 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); :} | NUM.n {: return new Lit(n); :} | PLUS intexpr.a @ PREFIX {: return new PreOp("+", TInt.instance(), TInt.instance(), a); :} | MINUS intexpr.a @ PREFIX {: return new PreOp("-", TInt.instance(), TInt.instance(), a); :} diff --git a/wptool/src/wptool/Preprocess.scala b/wptool/src/wptool/Preprocess.scala index 1f0a915..a999683 100644 --- a/wptool/src/wptool/Preprocess.scala +++ b/wptool/src/wptool/Preprocess.scala @@ -86,10 +86,13 @@ object PreProcess { head case doWhile: DoWhile => val after = currBlock.prepend(Assume(PreOp("!", TBool, TBool, evalExp(doWhile.test)))) - val repeat = Block( - "do-while repeat", - List(Guard(doWhile.test), Assert(doWhile.invariant, true)), - List() + 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) diff --git a/wptool/src/wptool/SMT_.scala b/wptool/src/wptool/SMT_.scala index 494f5cf..dcfd968 100644 --- a/wptool/src/wptool/SMT_.scala +++ b/wptool/src/wptool/SMT_.scala @@ -185,8 +185,8 @@ object SMT_ { case BinOp(">", TInt, TBool, arg1, arg2) => imgr.greaterThan(translateInt(arg1, expectIds), translateInt(arg2, expectIds)) - case v @ Var(Id(_, TBool, _, _, _), _, _) if (!expectIds) => bmgr.makeVariable(v.toString) - case v @ Id(_, 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 == TBool) => makeSelect(x.name.toString, x.index, true, expectIds).asInstanceOf[api.BooleanFormula] @@ -217,8 +217,8 @@ object SMT_ { // TODO *+-/ - 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) + 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] diff --git a/wptool/src/wptool/Scanner.flex b/wptool/src/wptool/Scanner.flex index 57bb81d..b8962f6 100644 --- a/wptool/src/wptool/Scanner.flex +++ b/wptool/src/wptool/Scanner.flex @@ -120,7 +120,7 @@ WS = {NL} | [ \t\f] "global array" { return newToken(Terminals.GLOBALARRAY); } "local array" { return newToken(Terminals.LOCALARRAY); } "global obj" { return newToken(Terminals.GLOBALOBJ); } -"_Fields" { return newToken(Terminals.FIELDS); } +"_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 7678d93..641f688 100644 --- a/wptool/src/wptool/State.scala +++ b/wptool/src/wptool/State.scala @@ -12,7 +12,7 @@ case class State( controls: Set[Identifier], controlled: Set[Identifier], controlledBy: Map[Identifier, Set[Identifier]], // TODO check - L: Map[Id, Expression], + L: Map[Identifier, Expression], ids: Set[Id], arrayIds: Set[Id], globals: Set[Id], @@ -21,7 +21,8 @@ case class State( arrRelys: Map[Id, Expression], arrGuars: Map[Id, Expression], indicies: Map[Id, Int], - addrs: Map[Id, Int], + addrs: Map[Id, Expression], + fieldIndicies: Map[ObjIdAccess, Int], pointsTo: Map[Id, Set[Id]], error: Boolean = false ) { @@ -57,6 +58,14 @@ object State { } } + 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 @@ -109,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) @@ -135,7 +147,10 @@ object State { // 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 -> i) }.toMap + 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( @@ -156,6 +171,7 @@ object State { arrGuars, indicies, addrs, + fieldIndicies, pointsTo ) } diff --git a/wptool/src/wptool/Statement.scala b/wptool/src/wptool/Statement.scala index e30d5a7..6c1ee52 100644 --- a/wptool/src/wptool/Statement.scala +++ b/wptool/src/wptool/Statement.scala @@ -63,7 +63,7 @@ object Block { case class Assignment(lhs: Expression, expression: Expression, line: (String, Int)) extends Stmt(line) { def this(lhs: String, expression: Expression) = - this(new Id(lhs, 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 @@ -78,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, 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 diff --git a/wptool/src/wptool/VarDef.scala b/wptool/src/wptool/VarDef.scala index 2245850..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 + "]", 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, TInt, false, false, false), security) + this(new Id(variable, TInt, false, false, false, false), security) def toPair: Seq[(Id, Security)] = this match { case g => @@ -94,13 +94,18 @@ sealed trait Definition extends beaver.Symbol 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, TInt, false, false, false), pred, List(), 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), pred, pointsTo.toList.map(v => Id(v, TInt, false, false, false)), 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, TInt, false, false, false), Const._true, List(), 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), Const._true, pointsTo.toList.map(v => Id(v, TInt, false, false, false)), 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( @@ -120,7 +125,7 @@ case class ArrayDef( guar: Guar ) = this( - new Id(name, TInt, false, false, false), + new Id(name, TInt, false, false, false, false), size, pred, access, @@ -135,7 +140,7 @@ case class ArrayDef( guar: Guar ) = this( - new Id(name, TInt, false, false, false), + new Id(name, TInt, false, false, false, false), size, Const._true, access, @@ -156,19 +161,21 @@ object ArrayDef { // TODO L!!! case class ObjDef( name: Id, - fields: List[Id], + fields: List[Field], access: Access ) extends Definition { def this( name: String, - fields: Array[String], + fields: Array[Field], access: Access ) = this( - new Id(name, TInt, false, false, false), - fields.map(i => new Id(i, TInt, false, false, false)).toList, + 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 {} From 9875630155eaa339b815c0a965782b9ab3dc20cf Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Fri, 19 Feb 2021 09:44:11 +1000 Subject: [PATCH 21/25] Fixed subst/eval --- tests/rg/treiber/put | 10 +- wptool/src/wptool/Exec.scala | 188 ++++++++++++++++++++--------- wptool/src/wptool/Expression.scala | 10 +- 3 files changed, 140 insertions(+), 68 deletions(-) diff --git a/tests/rg/treiber/put b/tests/rg/treiber/put index 4fe2725..508ceb5 100644 --- a/tests/rg/treiber/put +++ b/tests/rg/treiber/put @@ -14,10 +14,16 @@ global var *ss: _L: TRUE _PT: head, n +global var v: +_L: l == 1 + +global var l: +_L: TRUE + _Rely: TRUE -_Guar: (n.level == 0) => (n'.level == 0) +_Guar: TRUE // (n.level == 0) => (n'.level == 0) -n.level = 1; +n.level = l; n.val = v; do diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index 61670af..ceb711f 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -205,14 +205,18 @@ object Exec { BinOp.pred( "=>", eval( - getL(contr, state).subst((Map(assign.lhs.ident.toVar(state) -> Right((assign.lhs.index, assign.expression))), state)), + 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, true), - getL(contr, state).subst((Map(Id.indexId.toVar(state) -> Left(assign.lhs.index)), state)) + eval(getL(contr, state).subst((Map(Id.indexId.toVar(state) -> Left(assign.lhs.index)), state)), state, true) ) ) }) @@ -285,14 +289,18 @@ object Exec { case assign @ Assignment(lhs: Id, _, _) => val rhsGamma = computeGamma(assign.expression, state) - Q.subst( - ( - Map( - (lhs.toGamma.toVar(state) -> Left(rhsGamma)), - (lhs.toVar(state) -> Left(eval(assign.expression, state, false))) - ), - state - ) + eval( + Q.subst( + ( + Map( + (lhs.toGamma.toVar(state) -> Left(rhsGamma)), + (lhs.toVar(state) -> Left(eval(assign.expression, state, false))) + ), + state + ) + ), + state, + false ) case assign @ Assignment(Dereference(id), _, _) => val rhsGamma = computeGamma(assign.expression, state) @@ -301,14 +309,18 @@ object Exec { case _ => throw new Error("Unexpected dereference") } - Q.subst( - ( - Map( - (Dereference(lhs) -> Left(eval(assign.expression, state, true))), - (Dereference(lhs.toGamma(state)) -> Left(rhsGamma)) - ), - 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) @@ -317,29 +329,37 @@ object Exec { case lhs => throw new Error(s"Unexpected object $lhs (${lhs.getClass})") } - Q.subst( - Map( - (o.toVar(state) -> Left(eval(assign.expression, state, true))), - (o.toGamma.toVar(state) -> Left(rhsGamma)) + eval( + Q.subst( + Map( + (o.toVar(state) -> Left(eval(assign.expression, state, true))), + (o.toGamma.toVar(state) -> Left(rhsGamma)) + ), + state ), - state + state, + false ) case assign: ArrayAssignment => val rhsGamma = computeGamma(assign.expression, state) - 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 - ) + 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(s"Unhandled statement(wp exec): $stmt (${stmt.getClass})") @@ -349,6 +369,8 @@ object Exec { 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)) @@ -439,7 +461,50 @@ object Exec { def getRely(exp: Expression, state: State) = { val evalExp = eval(exp, state, false) - val p = eval( + 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( @@ -484,7 +549,6 @@ object Exec { state, true ) - p } def getL(id: Identifier, state: State): Expression = id match { @@ -493,12 +557,20 @@ object Exec { case _: IdAccess | _: VarAccess => id match { case id: IdAccess => - getL(id.ident, state).subst( - (Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true))), state) + eval( + getL(id.ident, state).subst( + (Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true))), state) + ), + state, + true ) case id: VarAccess => - getL(id.ident, state).subst( - (Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true))), state) + eval( + getL(id.ident, state).subst( + (Map(Id.indexId.toVar(state) -> Left(eval(id.index, state, true))), state) + ), + state, + true ) } case id: Identifier => @@ -510,13 +582,17 @@ object Exec { } def primed(p: Expression, state: State) = - eval(p, state, false).subst( - ( - (state.arrayIds + Id.memId) - .map(id => id.toVar(state) -> Left(id.toPrime.toVar(state))) - .toMap, - state - ) + eval( + eval(p, state, false).subst( + ( + (state.arrayIds + Id.memId) + .map(id => id.toVar(state) -> Left(id.toPrime.toVar(state))) + .toMap, + state + ) + ), + state, + false ) def stableR(p: Expression, state: State) = @@ -560,18 +636,10 @@ object Exec { 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 subst = Map( - (Id.memId.toVar(state) -> Left(Id.memId.toVar(state).toNought)), - (Id.memId.toPrime.toVar(state) -> Left(Id.memId.toVar(state))) - ) - */ val gPrime = guar.subst((subst, state)) val _subst = Map[Expression, Left[Expression, Nothing]](Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) - // val _subst = vars.map(v => v.toNought -> Left(v)).toMap - // val _subst = Map(Id.memId.toVar(state).toNought -> Left(Id.memId.toVar(state))) println(wp(eval(gPrime, state, true), a, state)) - wp(eval(gPrime, state, true), a, state).subst((_subst, state)) + eval(wp(eval(gPrime, state, true), a, state).subst((_subst, state)), state, true) } def guar(a: ArrayAssignment, state: State) = { @@ -588,9 +656,9 @@ object Exec { ) 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 gPrime = eval(guar.subst((subst, state)), state, true) val _subst = vars.map(v => v.toNought.asInstanceOf[Var] -> Left(v)).toMap[Expression, Left[Expression, Nothing]] - wp(gPrime, a, state).subst((_subst, state)) + eval(wp(gPrime, a, state).subst((_subst, state)), state, true) } def computeGamma(exp: Expression, state: State): Expression = { diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index d8e79b9..325f66a 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -124,8 +124,6 @@ case class VarAccess(name: Var, index: Expression) extends Variable { // TODO document/comment def subst(su: Subst) = { - // TODO not happy with filter - // println(s"$index -> ${index.subst((su._1.filter { case (v, _) => v.expType == TInt }, su._2))}") 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 { @@ -167,10 +165,10 @@ case class VarAccess(name: Var, index: Expression) extends Variable { case (p, (v: Var, Left(e))) => { // TODO handle _i this.index match { - case _ if v.ident == Id.indexId => p - case v: Var if (su._2.addrs.get(v.ident.getBase).get != v) => p - case _ if (name.index != v.index) => p - case _ => VarStore(p, su._2.addrs.get(v.ident.getBase).get, e) + case _ if v.ident == Id.indexId => p + case v: Var if (su._2.addrs.get(v.ident.getBase).get != v.ident) => p + case _ if (name.index != v.index) => p + case _ => VarStore(p, su._2.addrs.get(v.ident.getBase).get, e) } } case (p, (Dereference(v: Var), Left(e))) => From f17899715dc3774ea0093551489b7a327e03fb52 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Sun, 28 Feb 2021 11:16:40 +1000 Subject: [PATCH 22/25] Forgot to commit! --- README.md | 1 + tests/rg/seqlock/read | 1 - tests/rg/treiber/put | 7 +++++-- wptool/src/wptool/Exec.scala | 19 +++++++++---------- wptool/src/wptool/Expression.scala | 16 +++++++++++++--- wptool/src/wptool/SMT.scala | 1 + wptool/src/wptool/Statement.scala | 3 ++- wptool/src/wptool/WPTool.scala | 2 +- wptool/src/wptool/package.scala | 19 +++++++++++++++---- 9 files changed, 47 insertions(+), 22 deletions(-) diff --git a/README.md b/README.md index 85f88b9..1b48bfd 100644 --- a/README.md +++ b/README.md @@ -142,5 +142,6 @@ The logic for the weak memory model is currently not implemented ### 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/rg/seqlock/read b/tests/rg/seqlock/read index 4661f37..9b03a6d 100644 --- a/tests/rg/seqlock/read +++ b/tests/rg/seqlock/read @@ -18,7 +18,6 @@ _Guar: (z' == z) do _invariant: Gamma_r1 -// _invariant: Gamma_r1 && ((z == r1) => Gamma_r2) { do _invariant: Gamma_r1 diff --git a/tests/rg/treiber/put b/tests/rg/treiber/put index 508ceb5..55d9610 100644 --- a/tests/rg/treiber/put +++ b/tests/rg/treiber/put @@ -1,3 +1,5 @@ +// TODO this example fails + global obj n: _Field: val _L: n.level == 1 @@ -20,8 +22,9 @@ _L: l == 1 global var l: _L: TRUE -_Rely: TRUE -_Guar: TRUE // (n.level == 0) => (n'.level == 0) +// _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; diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index ceb711f..a8fe37c 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -23,6 +23,7 @@ object Exec { block.children.map(c => { val res = exec(c, state) if (c.atomic) + // TODO should there be a guaranttee check? res.copy(Qs = res.Qs.map(q => q.copy(pred = rImplies(q.pred, state)))) else res }), @@ -59,7 +60,7 @@ object Exec { ) .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") @@ -442,21 +443,20 @@ object Exec { expr } + private def skipMemLocs(v: Variable) = v match { + case v: Var if (v.ident.memLoc) => false + case v => true + } + def getBaseVars(vars: Set[Variable]): Set[Variable] = vars - .filter { - case v: Var if (v.ident.memLoc) => false - case _ => true - } + .filter(skipMemLocs) .map(v => v.getBase.resetIndex match { case v: VarAccess => v.name case v @ _ => v } ) - def getBaseVariables(vars: Set[Variable]): Set[Variable] = vars.map(v => v.getBase.resetIndex) - // def getBaseArrays(vars: Set[VarAccess]): Set[VarAccess] = - // vars.filter(v => v.name.ident.getBase != Id.memId).map(v => v.getBase.resetIndex) - // def getBaseMems(vars: Set[VarAccess]): Set[VarAccess] = vars.filter(v => v.name.ident.getBase == Id.memId).map(v => v.getBase.resetIndex) + 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, false) @@ -638,7 +638,6 @@ object Exec { 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))) - println(wp(eval(gPrime, state, true), a, state)) eval(wp(eval(gPrime, state, true), a, state).subst((_subst, state)), state, true) } diff --git a/wptool/src/wptool/Expression.scala b/wptool/src/wptool/Expression.scala index 325f66a..86bdd6d 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -166,9 +166,10 @@ case class VarAccess(name: Var, index: Expression) extends Variable { // TODO handle _i this.index match { case _ if v.ident == Id.indexId => p - case v: Var if (su._2.addrs.get(v.ident.getBase).get != v.ident) => 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, su._2.addrs.get(v.ident.getBase).get, e) + case _ => + VarStore(p, eval(su._2.addrs.get(v.ident.getBase).get, su._2), e) } } case (p, (Dereference(v: Var), Left(e))) => @@ -177,7 +178,11 @@ case class VarAccess(name: Var, index: Expression) extends Variable { 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)), su._2.addrs.get(v.ident.getBase).get), e) + 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 { @@ -189,6 +194,11 @@ case class VarAccess(name: Var, index: Expression) extends Variable { } } + 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)) diff --git a/wptool/src/wptool/SMT.scala b/wptool/src/wptool/SMT.scala index 4f15bf0..233e356 100644 --- a/wptool/src/wptool/SMT.scala +++ b/wptool/src/wptool/SMT.scala @@ -63,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) diff --git a/wptool/src/wptool/Statement.scala b/wptool/src/wptool/Statement.scala index 6c1ee52..7d6a748 100644 --- a/wptool/src/wptool/Statement.scala +++ b/wptool/src/wptool/Statement.scala @@ -189,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 { @@ -210,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/WPTool.scala b/wptool/src/wptool/WPTool.scala index c7aac7d..7607a3f 100644 --- a/wptool/src/wptool/WPTool.scala +++ b/wptool/src/wptool/WPTool.scala @@ -155,7 +155,7 @@ object WPTool { if (debug) println("L: " + _state.L) if (debug) println("Indicies: " + _state.indicies) - checkVcs(_state.Qs, (gammaSubstr, state), 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 3c89ff1..6b22e1b 100644 --- a/wptool/src/wptool/package.scala +++ b/wptool/src/wptool/package.scala @@ -69,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) @@ -83,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, @@ -107,6 +117,7 @@ package object wptool { debug, simplify ) + */ def printFalseVcs(preds: List[PredInfo]) = { println("Failing VCs") From 970125838373872f2c55a0e31399dcff9288ba8c Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Fri, 9 Jul 2021 14:41:10 +1000 Subject: [PATCH 23/25] Declassification --- tests/declassify/avg | 16 ++++++++++++++++ tests/declassify/if1 | 16 ++++++++++++++++ tests/declassify/neg/avg1 | 16 ++++++++++++++++ tests/declassify/neg/avg2 | 16 ++++++++++++++++ tests/declassify/neg/if1 | 16 ++++++++++++++++ working-tests/array0 | 11 ----------- wptool/src/wptool/Exec.scala | 14 +++++++++++--- wptool/src/wptool/Expression.scala | 8 ++++++++ wptool/src/wptool/Parser.grammar | 4 ++++ wptool/src/wptool/Scanner.flex | 1 + 10 files changed, 104 insertions(+), 14 deletions(-) create mode 100644 tests/declassify/avg create mode 100644 tests/declassify/if1 create mode 100644 tests/declassify/neg/avg1 create mode 100644 tests/declassify/neg/avg2 create mode 100644 tests/declassify/neg/if1 delete mode 100644 working-tests/array0 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/working-tests/array0 b/working-tests/array0 deleted file mode 100644 index 0ade55a..0000000 --- a/working-tests/array0 +++ /dev/null @@ -1,11 +0,0 @@ -global array a[2]: -_L: FALSE -_Rely: TRUE -_Guar: TRUE - -_Rely: TRUE -_Guar: TRUE - -a[0] = 1; -a[0] = 2; -assert a[0] == 2; diff --git a/wptool/src/wptool/Exec.scala b/wptool/src/wptool/Exec.scala index a8fe37c..e3d2528 100644 --- a/wptool/src/wptool/Exec.scala +++ b/wptool/src/wptool/Exec.scala @@ -425,6 +425,7 @@ object Exec { 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), @@ -662,18 +663,25 @@ object Exec { def computeGamma(exp: Expression, state: State): Expression = { val expEval = eval(exp, state, false) - constructForall( + val basePred = constructForall( expEval.vars - .map(v => + .map(v => { eval( BinOp.pred("||", v.toGamma(state), getL(v.ident, state)), // BinOp.pred("||", VarAccess(Id.memId.toGamma.toVar(state), Id.getAddr(v.ident, state)), getL(v.ident, state)), state, true ) // Default to high - ) + + }) .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 86bdd6d..a22beff 100644 --- a/wptool/src/wptool/Expression.scala +++ b/wptool/src/wptool/Expression.scala @@ -299,6 +299,14 @@ case class CompareAndSwap(x: Id, e1: Expression, e2: Expression) extends Express 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) diff --git a/wptool/src/wptool/Parser.grammar b/wptool/src/wptool/Parser.grammar index a029ed9..41dc8f7 100644 --- a/wptool/src/wptool/Parser.grammar +++ b/wptool/src/wptool/Parser.grammar @@ -35,6 +35,8 @@ %terminals ASSERT; %terminals CAS; +%terminals DECLASSIFY; + %terminals INVARIANT, GAMMA, GAMMA_0, RELY, GUAR; %terminals LPRED; %terminals PT; @@ -169,6 +171,7 @@ boolexpr | 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); :} + | 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 @@ -202,6 +205,7 @@ intexpr // 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("+", TInt.instance(), TInt.instance(), a); :} | MINUS intexpr.a @ PREFIX {: return new PreOp("-", TInt.instance(), TInt.instance(), a); :} diff --git a/wptool/src/wptool/Scanner.flex b/wptool/src/wptool/Scanner.flex index b8962f6..56eabe9 100644 --- a/wptool/src/wptool/Scanner.flex +++ b/wptool/src/wptool/Scanner.flex @@ -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); } From 8daf5ed92c7ace2937afe3866ec58b1cf3605455 Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Mon, 12 Jul 2021 10:12:38 +1000 Subject: [PATCH 24/25] Readme --- README.md | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 88c8ea8..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,10 +134,6 @@ _invariant: TRUE ## TODOs ### Unsupported language features Below is an inconclusive list of unsupported language features. - * Pointers - * Dynamic allocation - - * Dynamic thread creation * Objects From 06b107920d500825b18b607f6fbb6b21c75fbdcc Mon Sep 17 00:00:00 2001 From: TomCranitch Date: Mon, 12 Jul 2021 11:58:46 +1000 Subject: [PATCH 25/25] Declassify caslev put --- tests/declassify/put | 51 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 tests/declassify/put 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;