From ca05b5b3a396dacfe6d5a99d51f5c0a12396f9f1 Mon Sep 17 00:00:00 2001 From: Matt Windsor Date: Fri, 3 Feb 2017 17:26:21 +0000 Subject: [PATCH] Refactor and fix environments in modelling. --- Examples/PassGH/arc.cvf | 13 +- Examples/PassGH/clhLock.cvf | 2 +- Examples/PassGH/lclist.cvf | 4 +- Examples/PassGH/spinLock.cvf | 4 +- Examples/PassGH/ticketLock.cvf | 8 +- Modeller.fs | 296 +++++++++++++++------------------ ModellerTests.fs | 15 +- Var.fs | 113 +++++++++++++ 8 files changed, 267 insertions(+), 188 deletions(-) diff --git a/Examples/PassGH/arc.cvf b/Examples/PassGH/arc.cvf index f642c3d..b7b6eb0 100644 --- a/Examples/PassGH/arc.cvf +++ b/Examples/PassGH/arc.cvf @@ -19,9 +19,8 @@ thread Int c, pval; method init() { {| emp |} - // TODO: broken local command syntax. - ret = %{new ArcNode}; - <%{[|ret|].count := 1}>; + <{ ret = %{new ArcNode}; + %{[|ret|].count := 1}; }>; {| arc(ret) |} } @@ -33,16 +32,14 @@ method clone(ArcNode x) { method print(ArcNode x) { {| arc(x) |} - // TODO: broken local command syntax. - pval = %{ [|x|].val }; + ; {| arc(x) |} } method drop(ArcNode x) { {| arc(x) |} - // TODO: broken local command syntax. - c = %{ [|x|].count }; - <%{ [|x|].count := [|x|].count - 1 }>; + <{ c = %{ [|x|].count }; + %{ [|x|].count := [|x|].count - 1 }; }>; {| countCopy(x, c) |} if (c == 1) { {| countCopy(x, 1) |} diff --git a/Examples/PassGH/clhLock.cvf b/Examples/PassGH/clhLock.cvf index 4fec047..aa55048 100644 --- a/Examples/PassGH/clhLock.cvf +++ b/Examples/PassGH/clhLock.cvf @@ -23,7 +23,7 @@ method lock(Node mynode) { {| queued(mynode, mypred) |} do { {| queued(mynode, mypred) |} - test = %{ [|mypred|].lock }; + ; {| if test then queued(mynode, mypred) else holdLock(mynode, mypred) |} } while (test); {| holdLock(mynode, mypred) |} diff --git a/Examples/PassGH/lclist.cvf b/Examples/PassGH/lclist.cvf index c15ce85..17f9ab9 100644 --- a/Examples/PassGH/lclist.cvf +++ b/Examples/PassGH/lclist.cvf @@ -21,11 +21,11 @@ method deleteVal(int v) { {| wf(v) * isHead(prev) |} <{ %{ waitLock([|prev|]); takeLock([|prev|]) }; }>; {| wf(v) * has1LockAnon(prev) * isHead(prev) |} - curr = %{ [|prev|].next }; + < curr = %{ [|prev|].next } >; {| wf(v) * has1Lock(prev, curr) * isHead(prev) |} <{ %{ waitLock([|curr|]); takeLock([|curr|]) }; }>; {| wf(v) * has2Lock(prev, curr) |} - cv = %{ [|curr|].val }; + < cv = %{ [|curr|].val } >; {| wf(v) * has2Lock(prev,curr) * isVal(curr, cv) |} while (cv < v ) { {| wf(v) * wf(cv) * has2Lock(prev, curr) * isVal(curr, cv) |} diff --git a/Examples/PassGH/spinLock.cvf b/Examples/PassGH/spinLock.cvf index e7e444c..c6c2860 100644 --- a/Examples/PassGH/spinLock.cvf +++ b/Examples/PassGH/spinLock.cvf @@ -13,7 +13,7 @@ view newLock(Lock x), holdLock(Lock x), isLock(Lock x); method newLock() { {| emp |} - ret = %{new Lock}; + ; {| newLock(ret) |} <%{[|ret|].lock := false}>; {| isLock(ret) |} @@ -25,7 +25,7 @@ method lock(Lock x) { {| isLock(x) |} test = false; {| if test == false then isLock(x) else False() |} - test = %{ CAS_to_true([|x|]) }; + ; {| if test == false then isLock(x) else holdLock(x) |} } while (test == false); {| holdLock(x) |} diff --git a/Examples/PassGH/ticketLock.cvf b/Examples/PassGH/ticketLock.cvf index 7e48514..eac0617 100644 --- a/Examples/PassGH/ticketLock.cvf +++ b/Examples/PassGH/ticketLock.cvf @@ -13,7 +13,7 @@ view newLock(Lock x), holdTick(Lock x, int t), holdLock(Lock x), isLock(Lock x); method newLock() { {| emp |} - ret = %{new Lock}; + ; {| newLock(ret) |} <%{[|ret|].ticket := 0; [|ret|].serving := 0}>; {| isLock(ret) |} @@ -21,12 +21,12 @@ method newLock() { method lock(Lock x) { {| isLock(x) |} - t = %{ [|x|].ticket }; - <%{ [|x|].ticket := [|x|].ticket + 1 }>; + <{ t = %{ [|x|].ticket }; + %{ [|x|].ticket := [|x|].ticket + 1 }; }>; {| holdTick(x, t) |} do { {| holdTick(x, t) |} - s = %{ [|x|].serving }; + ; {| if s == t then holdLock(x) else holdTick(x, t) |} } while (s != t); {| holdLock(x) |} diff --git a/Modeller.fs b/Modeller.fs index 4b91802..3461c69 100644 --- a/Modeller.fs +++ b/Modeller.fs @@ -12,6 +12,7 @@ open Starling.Core.Definer open Starling.Core.TypeSystem open Starling.Core.Expr open Starling.Core.Var +open Starling.Core.Var.Env open Starling.Core.Var.VarMap open Starling.Core.Symbolic open Starling.Core.Model @@ -57,13 +58,9 @@ module Types = /// type MethodContext = { /// - /// The environment of visible shared variables. + /// The environment of visible variables. /// - SharedVars : VarMap - /// - /// The environment of visible thread-local variables. - /// - ThreadVars : VarMap + Env : Env /// /// A definer containing the visible view prototypes. /// @@ -623,10 +620,9 @@ let checkBoolIsNormalType (bool : TypedBoolExpr<'Var>) /// to be modified by a post-processing function. /// /// -/// -/// The VarMap of variables bound where this expression -/// occurs. Usually, but not always, these are the thread-local -/// variables. +/// The of variables in the program. +/// +/// The level of variable scope at which this expression occurs. /// /// /// A function to transform any variables after they are looked-up, @@ -648,8 +644,8 @@ let checkBoolIsNormalType (bool : TypedBoolExpr<'Var>) /// expression depend on . /// let rec modelExpr - (env : VarMap) - (idxEnv : VarMap) + (env : Env) + (scope : Scope) (varF : Var -> 'var) (e : Expression) : Result>, ExprError> = @@ -663,15 +659,15 @@ let rec modelExpr (varF >> Reg >> ok) (tliftOverCTyped >> tliftToExprDest) >> mapMessages BadSub) - (wrapMessages Var (VarMap.lookup env) v) + (wrapMessages Var (Env.lookup env scope) v) | Symbolic sym -> fail (AmbiguousSym sym) (* If we have an array, then work out what the type of the array's elements are, then walk back from there. *) | ArraySubscript (arr, idx) -> - let arrR = modelArrayExpr env idxEnv varF arr - // Indices always have to be of type 'int'. - let idxuR = modelIntExpr idxEnv idxEnv varF idx + let arrR = modelArrayExpr env scope varF arr + // Indices always have to be of type 'int', and be in local scope. + let idxuR = modelIntExpr env (indexScopeOf scope) varF idx let idxR = bind (checkIntIsNormalType >> mapMessages ExprBadType) idxuR lift2 @@ -684,8 +680,8 @@ let rec modelExpr (* We can use the active patterns above to figure out whether we * need to treat this expression as arithmetic or Boolean. *) - | ArithExp' _ -> lift (liftTypedSub Expr.Int) (modelIntExpr env idxEnv varF e) - | BoolExp' _ -> lift (liftTypedSub Expr.Bool) (modelBoolExpr env idxEnv varF e) + | ArithExp' _ -> lift (liftTypedSub Expr.Int) (modelIntExpr env scope varF e) + | BoolExp' _ -> lift (liftTypedSub Expr.Bool) (modelBoolExpr env scope varF e) | _ -> failwith "unreachable[modelExpr]" /// @@ -695,10 +691,9 @@ let rec modelExpr /// See modelExpr for more information. /// /// -/// -/// The VarMap of variables bound where this expression -/// occurs. Usually, but not always, these are the thread-local -/// variables. +/// The of variables in the program. +/// +/// The level of variable scope at which this expression occurs. /// /// /// A function to transform any variables after they are looked-up, @@ -723,13 +718,13 @@ let rec modelExpr /// . /// and modelBoolExpr - (env : VarMap) - (idxEnv : VarMap) + (env : Env) + (scope : Scope) (varF : Var -> 'var) (expr : Expression) : Result>, ExprError> = - let mi = modelIntExpr env idxEnv varF - let me = modelExpr env idxEnv varF - let ma = modelArrayExpr env idxEnv varF + let mi = modelIntExpr env scope varF + let me = modelExpr env scope varF + let ma = modelArrayExpr env scope varF let rec mb e : Result>, ExprError> = match e.Node with @@ -750,15 +745,17 @@ and modelBoolExpr (v, TypeMismatch (expected = Fuzzy "bool", got = Exact (typeOf vr))))) - (wrapMessages Var (VarMap.lookup env) v) + (wrapMessages Var (Env.lookup env scope) v) | Symbolic sa -> - // Symbols have an indefinite subtype. - lift (fun a -> indefBool (BVar (Sym a))) (tryMapSym me sa) + (* Symbols have an indefinite subtype, and can include thread-local + scope. *) + lift + (fun a -> indefBool (BVar (Sym a))) + (tryMapSym (modelExpr env (symbolicScopeOf scope) varF) sa) | ArraySubscript (arr, idx) -> let arrR = ma arr - // Indices always have to be of type 'int'. - // Bind array index using its own environment. - let idxuR = modelIntExpr idxEnv idxEnv varF idx + // Indices always have to be of type 'int', and in local scope. + let idxuR = modelIntExpr env (indexScopeOf scope) varF idx let idxR = bind (checkIntIsNormalType >> mapMessages ExprBadType) idxuR bind2 @@ -784,7 +781,7 @@ and modelBoolExpr match o with | And -> mkAnd2 | Or -> mkOr2 - | Imp -> mkImpl + | Imp -> mkImplies | _ -> failwith "unreachable[modelBoolExpr::BoolIn]" (* Both sides of the expression need to be unifiable to the @@ -824,14 +821,9 @@ and modelBoolExpr /// See modelExpr for more information. /// /// -/// -/// The VarMap of variables bound where this expression -/// occurs. Usually, but not always, these are the thread-local -/// variables. -/// -/// -/// The VarMap of variables available to any array subscripts in this -/// expression. This is almost always the thread-local variables. +/// The of variables in the program. +/// +/// The level of variable scope at which this expression occurs. /// /// /// A function to transform any variables after they are looked-up, @@ -852,12 +844,12 @@ and modelBoolExpr /// . /// and modelIntExpr - (env : VarMap) - (idxEnv : VarMap) + (env : Env) + (scope : Scope) (varF : Var -> 'var) (expr : Expression) : Result>, ExprError> = - let me = modelExpr env idxEnv varF - let ma = modelArrayExpr env idxEnv varF + let me = modelExpr env scope varF + let ma = modelArrayExpr env scope varF let rec mi e = match e.Node with @@ -868,7 +860,7 @@ and modelIntExpr * arithmetic type. *) v - |> wrapMessages Var (VarMap.lookup env) + |> wrapMessages Var (Env.lookup env scope) |> bind (function | Typed.Int (ty, vn) -> ok (mkTypedSub ty (IVar (Reg (varF vn)))) @@ -880,12 +872,13 @@ and modelIntExpr (expected = Fuzzy "int", got = Exact (typeOf vr))))) | Symbolic sa -> // Symbols have indefinite subtype. - lift (fun a -> indefInt (IVar (Sym a))) (tryMapSym me sa) + lift + (fun a -> indefInt (IVar (Sym a))) + (tryMapSym (modelExpr env (symbolicScopeOf scope) varF) sa) | ArraySubscript (arr, idx) -> let arrR = ma arr - // Indices always have to be of type 'int'. - // Bind array index using its own environment. - let idxuR = modelIntExpr idxEnv idxEnv varF idx + // Indices always have to be of type 'int' and local scope. + let idxuR = modelIntExpr env (indexScopeOf scope) varF idx let idxR = bind (checkIntIsNormalType >> mapMessages ExprBadType) idxuR bind2 @@ -928,14 +921,9 @@ and modelIntExpr /// See modelExpr for more information. /// /// -/// -/// The VarMap of variables bound where this expression -/// occurs. Usually, but not always, these are the thread-local -/// variables. -/// -/// -/// The VarMap of variables available to any array subscripts in this -/// expression. This is almost always the thread-local variables. +/// The of variables in the program. +/// +/// The level of variable scope at which this expression occurs. /// /// /// A function to transform any variables after they are looked-up, @@ -956,12 +944,12 @@ and modelIntExpr /// . /// and modelArrayExpr - (env : VarMap) - (idxEnv : VarMap) + (env : Env) + (scope : Scope) (varF : Var -> 'var) (expr : Expression) : Result>, ExprError> = - let mi = modelIntExpr env idxEnv varF + let mi = modelIntExpr env scope varF let rec ma e = match e.Node with @@ -970,7 +958,7 @@ and modelArrayExpr * array type. *) v - |> wrapMessages Var (VarMap.lookup env) + |> wrapMessages Var (Env.lookup env scope) |> bind (function | Typed.Array (t, vn) -> ok (mkTypedSub t (AVar (Reg (varF vn)))) @@ -987,8 +975,8 @@ and modelArrayExpr fail (AmbiguousSym sym) | ArraySubscript (arr, idx) -> let arrR = ma arr - // Indices always have to be of type 'int'. - let idxuR = modelIntExpr idxEnv idxEnv varF idx + // Indices always have to be of type 'int' and in local scope. + let idxuR = modelIntExpr env Thread varF idx let idxR = bind (checkIntIsNormalType >> mapMessages ExprBadType) idxuR bind2 @@ -1057,9 +1045,8 @@ let makeIteratorMap : TypedVar option -> VarMap = | Some (Int (t, v)) -> Map.ofList [ v, Type.Int (t, ()) ] | _ -> failwith "Iterator in iterated views must be Int type" -/// Produces the environment created by interpreting the viewdef vds using the -/// view prototype map vpm. -let rec localEnvOfViewDef (vds : DView) : Result = +/// Produces the environment created by interpreting the viewdef vds. +let rec varMapOfViewDef (vds : DView) : Result = let makeFuncMap { Func = {Params = ps}; Iterator = it } = VarMap.ofTypedVarSeq ps >>= (VarMap.combine (makeIteratorMap it)) @@ -1069,25 +1056,24 @@ let rec localEnvOfViewDef (vds : DView) : Result = mapMessages ViewError.BadVar singleMap -/// Produces the variable environment for the constraint whose viewdef is v. -let envOfViewDef (svars : VarMap) : DView -> Result = - localEnvOfViewDef >> bind (VarMap.combine svars >> mapMessages SVarConflict) - /// Converts a single constraint to its model form. let modelViewDef - (svars : VarMap) + (env : Env) (vprotos : FuncDefiner) (av : ViewSignature, ad : Expression option) : Result<(DView * SVBoolExpr option), ModelError> = trial { let! vms = wrapMessages CEView (modelViewSignature vprotos) av let v = vms |> Multiset.toFlatList - let! e = envOfViewDef svars v |> mapMessages (curry CEView av) + let! e = mapMessages (curry CEView av) (varMapOfViewDef v) + + let scope = WithMap (e, Shared) + let! d = match ad with | Some dad -> dad - |> wrapMessages CEExpr (modelBoolExpr e e id) + |> wrapMessages CEExpr (modelBoolExpr env scope id) |> bind (checkBoolIsNormalType >> mapMessages (fun t -> CEExpr (dad, ExprBadType t))) |> lift Some | None _ -> ok None @@ -1264,18 +1250,18 @@ let modelViewDefs /// Models an AFunc as a CFunc. let modelCFunc - ({ ViewProtos = protos; ThreadVars = tvars } : MethodContext) + (ctx : MethodContext) (afunc : Func) = // First, make sure this AFunc actually has a prototype // and the correct number of parameters. afunc - |> lookupFunc protos + |> lookupFunc ctx.ViewProtos |> bind (fun proto -> // First, model the AFunc's parameters. afunc.Params |> Seq.map (fun e -> e - |> modelExpr tvars tvars id + |> modelExpr ctx.Env Thread id |> mapMessages (curry ViewError.BadExpr e)) |> collect // Then, put them into a VFunc. @@ -1300,7 +1286,7 @@ let rec modelCView (ctx : MethodContext) : View -> Result = not a subtype. *) let teR = wrapMessages ViewError.BadExpr - (modelBoolExpr ctx.ThreadVars ctx.ThreadVars id) + (modelBoolExpr ctx.Env Thread id) e let eR = bind @@ -1328,72 +1314,78 @@ let rec modelCView (ctx : MethodContext) : View -> Result = /// Models a Boolean lvalue given a potentially valid expression and /// environment. /// -/// The environment used for variables in the lvalue. -/// The environment used for indexes in the lvalue. +/// The of variables in the program. +/// +/// The level of variable scope at which this expression occurs. +/// /// A function that marks (or doesn't mark) vars. /// The possible lvalue to model. /// If the subject is a valid lvalue, the result expression. let modelBoolLValue - (env : VarMap) (idxEnv : VarMap) (marker : Var -> 'Var) (ex : Expression) + (env : Env) (scope : Scope) (marker : Var -> 'Var) (ex : Expression) : Result>, PrimError> = match ex with | RValue r -> fail (NeedLValue r) - | LValue l -> wrapMessages BadExpr (modelBoolExpr env idxEnv marker) l + | LValue l -> wrapMessages BadExpr (modelBoolExpr env scope marker) l // Models a boolean // in an analogous way to ``modelIntLValueOrSymbol`` let modelBoolLValueOrSymbol - (env : VarMap) (idxEnv : VarMap) (marker : Var -> 'Var) (ex : Expression) + (env : Env) (scope : Scope) (marker : Var -> 'Var) (ex : Expression) : Result>, PrimError> = match ex with | RValue r -> match r.Node with - | Symbolic _ -> wrapMessages BadExpr (modelBoolExpr env idxEnv marker) r + | Symbolic _ -> wrapMessages BadExpr (modelBoolExpr env scope marker) r | _ -> fail (NeedLValue r) - | LValue l -> wrapMessages BadExpr (modelBoolExpr env idxEnv marker) l + | LValue l -> wrapMessages BadExpr (modelBoolExpr env scope marker) l /// /// Models an integer lvalue given a potentially valid expression and /// environment. /// -/// The environment used for variables in the lvalue. -/// The environment used for indexes in the lvalue. +/// The of variables in the program. +/// +/// The level of variable scope at which this expression occurs. +/// /// A function that marks (or doesn't mark) vars. /// The possible lvalue to model. /// If the subject is a valid lvalue, the result expression. let modelIntLValue - (env : VarMap) (idxEnv : VarMap) (marker : Var -> 'Var) (ex : Expression) + (env : Env) (scope : Scope) (marker : Var -> 'Var) (ex : Expression) : Result>, PrimError> = match ex with | RValue r -> fail (NeedLValue r) - | LValue l -> wrapMessages BadExpr (modelIntExpr env idxEnv marker) l + | LValue l -> wrapMessages BadExpr (modelIntExpr env scope marker) l /// Model an expr that's either an IntLValue or a Symbolic Command let modelIntLValueOrSymbol - (env : VarMap) (idxEnv : VarMap) (marker : Var -> 'Var) (ex : Expression) + (env : Env) (scope : Scope) (marker : Var -> 'Var) (ex : Expression) : Result>, PrimError> = match ex with | RValue r -> match r.Node with - | Symbolic _ -> wrapMessages BadExpr (modelIntExpr env idxEnv marker) r + | Symbolic _ -> wrapMessages BadExpr (modelIntExpr env scope marker) r | _ -> fail (NeedLValue r) - | LValue l -> wrapMessages BadExpr (modelIntExpr env idxEnv marker) l + | LValue l -> wrapMessages BadExpr (modelIntExpr env scope marker) l /// /// Models an lvalue given a potentially valid expression and /// environment. /// -/// The environment of variables used for the lvalue. -/// The environment used for indexes in the lvalue. +/// The of variables in the program. +/// +/// The level of variable scope at which this expression occurs. +/// /// A function that marks (or doesn't mark) vars. /// The possible lvalue to model. /// If the subject is a valid lvalue, the result expression. let modelLValue - (env : VarMap) (idxEnv : VarMap) (marker : Var -> 'Var) (ex : Expression) + (env : Env) (scope : Scope) (marker : Var -> 'Var) (ex : Expression) : Result>, PrimError> = match ex with | RValue r -> fail (NeedLValue r) - | LValue l -> wrapMessages BadExpr (modelExpr env idxEnv marker) l + | LValue l -> wrapMessages BadExpr (modelExpr env scope marker) l /// Converts a Boolean load to a Prim. let modelBoolLoad @@ -1420,8 +1412,8 @@ let modelBoolLoad (Exact (typedBoolToType srcE))) bind2 modelWithExprs - (modelBoolLValue ctx.ThreadVars ctx.ThreadVars id dest) - (modelBoolLValue ctx.SharedVars ctx.ThreadVars id src) + (modelBoolLValue ctx.Env Thread id dest) + (modelBoolLValueOrSymbol ctx.Env Shared id src) /// Converts an integer load to a Prim. let modelIntLoad @@ -1460,16 +1452,9 @@ let modelIntLoad (Exact (typedIntToType dstE)) (Exact (typedIntToType srcE))) - // for symbolics, use combined environment for input variables - match combine ctx.ThreadVars ctx.SharedVars with - // { there might be a nicer way of doing this - | Bad [] -> Bad [] - | Bad (x :: xs) -> mergeMessages (List.map SymVarError xs) <| fail (SymVarError x) - // } - | Ok(rv, _) -> - bind2 modelWithExprs - (modelIntLValue ctx.ThreadVars ctx.ThreadVars id dest) - (modelIntLValueOrSymbol rv ctx.ThreadVars id src) + bind2 modelWithExprs + (modelIntLValue ctx.Env Thread id dest) + (modelIntLValueOrSymbol ctx.Env Shared id src) /// Converts a Boolean store to a Prim. let modelBoolStore @@ -1495,14 +1480,9 @@ let modelBoolStore (Exact (typedBoolToType dstE)) (Exact (typedBoolToType srcE))) - // for symbolics, use combined environment for input variables - match combine ctx.ThreadVars ctx.SharedVars with - | Bad [] -> Bad [] - | Bad (x :: xs) -> mergeMessages (List.map SymVarError xs) <| fail (SymVarError x) - | Ok(rv, _) -> - bind2 modelWithExprs - (modelBoolLValue ctx.SharedVars ctx.ThreadVars id dest) - (modelBoolLValueOrSymbol rv ctx.ThreadVars id src) + bind2 modelWithExprs + (modelBoolLValue ctx.Env Shared id dest) + (wrapMessages BadExpr (modelBoolExpr ctx.Env Thread id) src) /// Converts an integral store to a Prim. let modelIntStore @@ -1542,20 +1522,20 @@ let modelIntStore (Exact (typedIntToType srcE))) bind2 modelWithExprs - (modelIntLValue ctx.SharedVars ctx.ThreadVars id dest) - (wrapMessages BadExpr (modelIntExpr ctx.ThreadVars ctx.ThreadVars id) src) + (modelIntLValue ctx.Env Shared id dest) + (wrapMessages BadExpr (modelIntExpr ctx.Env Thread id) src) /// /// Models an Int and checks that it is type-compatible with another type. /// let modelIntWithType (rtype : Type) - (env : VarMap) - (idxEnv : VarMap) + (env : Env) + (scope : Scope) (expr : Expression) : Result>, PrimError> = // TODO(CaptainHayashi): proper doc comment. - let eR = wrapMessages BadExpr (modelIntExpr env idxEnv id) expr + let eR = wrapMessages BadExpr (modelIntExpr env scope id) expr let checkType e = let etype = typedIntToType e @@ -1569,12 +1549,12 @@ let modelIntWithType /// let modelBoolWithType (rtype : Type) - (env : VarMap) - (idxEnv : VarMap) + (env : Env) + (scope : Scope) (expr : Expression) : Result>, PrimError> = // TODO(CaptainHayashi): proper doc comment. - let eR = wrapMessages BadExpr (modelBoolExpr env idxEnv id) expr + let eR = wrapMessages BadExpr (modelBoolExpr env scope id) expr let checkType e = let etype = typedBoolToType e @@ -1604,7 +1584,7 @@ let modelCAS when primTypeRecsCompatible dr tr -> // set has to be type-compatible with destLV, of course. let setR = - modelBoolWithType (typeOf destLV) ctx.ThreadVars ctx.ThreadVars set + modelBoolWithType (typeOf destLV) ctx.Env Thread set let modelWithSet setE = command "BCAS" [ destLV; testLV ] @@ -1614,7 +1594,7 @@ let modelCAS when primTypeRecsCompatible dr tr -> // set has to be type-compatible with destLV, of course. let setR = - modelIntWithType (typeOf destLV) ctx.ThreadVars ctx.ThreadVars set + modelIntWithType (typeOf destLV) ctx.Env Thread set let modelWithSet setE = command "ICAS" [ destLV; testLV ] @@ -1625,10 +1605,8 @@ let modelCAS Arbitrarily single out test as the cause of it. *) fail (primTypeMismatch test (Exact (typeOf d)) (Exact (typeOf t))) - let mdl vars = modelLValue vars ctx.ThreadVars id - bind2 modelWithDestAndTest - (mdl ctx.SharedVars dest) - (mdl ctx.ThreadVars test) + let mdl scope = modelLValue ctx.Env scope id + bind2 modelWithDestAndTest (mdl Shared dest) (mdl Thread test) /// /// Gets the underlying variable of an lvalue. @@ -1647,12 +1625,15 @@ let rec varOfLValue (lv : Expression) : Var = /// Tries to get the type of an lvalue. /// /// The map in which the lvalue's variable exists. +/// +/// The level of variable scope to lookup the lvalue in. +/// /// The lvalue-candidate whose type is needed. /// /// If the lvalue has a valid type, the type of that lvalue; otherwise, /// None. /// -let typeOfLValue (env : VarMap) (lv : Expression) : Type option = +let typeOfLValue (env : Env) (scope : Scope) (lv : Expression) : Type option = (* We can get the type by traversing the lvalue up to its underlying variable, chaining together a sequence of 'matcher functions' that respond to the various transformations (subscripts etc.) to that variable by peeling off @@ -1672,7 +1653,7 @@ let typeOfLValue (env : VarMap) (lv : Expression) : Type option = (* We've found a variable x. Its type is available in env. However, if we walked through some []s to get here, we need to apply the matcher sequence to extract the eventual element type. *) - Option.bind (typeOf >> matcher) (VarMap.tryLookup env v) + Option.bind (typeOf >> matcher) (Env.tryLookup env scope v) | ArraySubscript (arr, _) -> (* If we find x[i], get the type t(x) and then make a note to extract t(x)'s element type. So, if arr is of type int[], we will get int. *) @@ -1696,13 +1677,13 @@ let modelFetch let rec findModeller d = match d with | LValue _ -> - match (typeOfLValue ctx.SharedVars d) with + match (typeOfLValue ctx.Env Shared d) with | Some (Typed.Int _) -> ok modelIntStore | Some (Typed.Bool _) -> ok modelBoolStore | Some (Typed.Array (_)) -> fail (PrimNotImplemented "array fetch") | None -> - match (typeOfLValue ctx.ThreadVars d) with + match (typeOfLValue ctx.Env Thread d) with | Some (Typed.Int _) -> ok modelIntLoad | Some (Typed.Bool _) -> ok modelBoolLoad | Some (Typed.Array (_)) @@ -1735,11 +1716,11 @@ let modelPostfix (ctx : MethodContext) (operand : Expression) (mode : FetchMode) | Decrement, Typed.Int _ -> ok (command "!I--" [ opE ] [ opE ]) | _, Typed.Array (_) -> fail (PrimNotImplemented "array postfix") bind modelWithOperand - (modelLValue ctx.SharedVars ctx.ThreadVars id operand) + (modelLValue ctx.Env Shared id operand) /// Converts a single atomic command from AST to part-commands. -let rec modelAtomic : MethodContext -> Atomic -> Result = - fun ctx a -> +let rec modelAtomic + (ctx : MethodContext) (a : Atomic) : Result = let prim = match a.Node with | CompareAndSwap(dest, test, set) -> modelCAS ctx dest test set @@ -1748,32 +1729,19 @@ let rec modelAtomic : MethodContext -> Atomic -> Result | Id -> ok (command "Id" [] []) | Assume e -> e - |> wrapMessages BadExpr (modelBoolExpr ctx.ThreadVars ctx.ThreadVars id) + |> wrapMessages BadExpr (modelBoolExpr ctx.Env Thread id) |> lift (typedBoolToExpr >> List.singleton >> command "Assume" []) | Havoc var -> - let allVarsR = - mapMessages SymVarError (VarMap.combine ctx.ThreadVars ctx.SharedVars) - let varMR = - bind - (fun allVars -> - mapMessages SymVarError - (VarMap.lookup allVars var)) - allVarsR + let varMR = mapMessages SymVarError (Env.lookup ctx.Env Full var) lift (fun varM -> Intrinsic (IntrinsicCommand.Havoc varM)) varMR | SymAtomic sym -> // TODO(CaptainHayashi): split out. - let allVarsR = - mapMessages SymVarError (VarMap.combine ctx.ThreadVars ctx.SharedVars) let symMR = - bind - (fun allVars -> - (tryMapSym - (wrapMessages BadExpr - (modelExpr allVars ctx.ThreadVars id)) - sym)) - allVarsR + (tryMapSym + (wrapMessages BadExpr (modelExpr ctx.Env Full id)) + sym) lift SymC symMR lift @@ -1794,7 +1762,7 @@ and modelAssign let modelWithDest destM = match destM with | Int (dt, d) -> - let srcR = modelIntExpr ctx.ThreadVars ctx.ThreadVars id src + let srcR = modelIntExpr ctx.Env Thread id src let modelWithSrc srcE = match unifyPrimTypeRecs [ dt; srcE.SRec ] with | Some dst -> @@ -1813,7 +1781,7 @@ and modelAssign (Exact (typedIntToType srcE))) bind modelWithSrc (mapMessages (curry BadExpr src) srcR) | Bool (dt, d) -> - let srcR = modelBoolExpr ctx.ThreadVars ctx.ThreadVars id src + let srcR = modelBoolExpr ctx.Env Thread id src let modelWithSrc srcE = match unifyPrimTypeRecs [ dt; srcE.SRec ] with | Some dst -> @@ -1836,7 +1804,7 @@ and modelAssign (* The permitted type of src depends on the type of dest. (Maybe, if the dest is ambiguous, we should invert this?) *) - let destResult = modelLValue ctx.ThreadVars ctx.ThreadVars id dest + let destResult = modelLValue ctx.Env Thread id dest bind modelWithDest destResult /// Creates a partially resolved axiom for an if-then-else. @@ -1849,7 +1817,7 @@ and modelITE let iuR = wrapMessages BadITECondition - (modelBoolExpr ctx.ThreadVars ctx.ThreadVars id) + (modelBoolExpr ctx.Env Thread id) i // An if condition needs to be of type 'bool', not a subtype. let iR = @@ -1884,7 +1852,7 @@ and modelWhile let euR = wrapMessages BadWhileCondition - (modelBoolExpr ctx.ThreadVars ctx.ThreadVars id) + (modelBoolExpr ctx.Env Thread id) e // While conditions have to be of type 'bool', not a subtype. let eR = @@ -2101,6 +2069,7 @@ let model // Make variable maps out of the shared and thread variable definitions. let! svars = modelVarMap types collated.SharedVars "shared" let! tvars = modelVarMap types collated.ThreadVars "thread" + let env = Env.env tvars svars let desugaredMethods, unknownProtos = desugar tvars collated.Methods @@ -2108,12 +2077,11 @@ let model let! cprotos = convertViewProtos types collated.VProtos let! vprotos = modelViewProtos (Seq.append cprotos unknownProtos) - let! constraints = modelViewDefs svars vprotos collated + let! constraints = modelViewDefs env vprotos collated let mctx = { ViewProtos = vprotos - SharedVars = svars - ThreadVars = tvars } + Env = env } let! axioms = desugaredMethods |> Map.toSeq diff --git a/ModellerTests.fs b/ModellerTests.fs index a365906..a40cabb 100644 --- a/ModellerTests.fs +++ b/ModellerTests.fs @@ -49,13 +49,11 @@ let shared = let context = { ViewProtos = ticketLockProtos - SharedVars = Map.empty - ThreadVars = environ } + Env = Env.env environ Map.empty } let sharedContext = { ViewProtos = ticketLockProtos - SharedVars = shared - ThreadVars = environ } + Env = Env.env environ shared } module ViewPass = @@ -121,15 +119,17 @@ module ArithmeticExprs = open Starling.Lang.Modeller.Pretty let check (env : VarMap) (ast : Expression) (expectedExpr : TypedIntExpr>) = + let e = Env.env environ env assertOkAndEqual expectedExpr - (modelIntExpr env environ id ast) + (modelIntExpr e Env.Shared id ast) (printExprError >> printUnstyled) let checkFail (env : VarMap) (ast : Expression) (expectedErrors : ExprError list) = + let e = Env.env environ env assertFail expectedErrors - (modelIntExpr env environ id ast) + (modelIntExpr e Env.Shared id ast) (stripTypeRec >> printIntExpr (printSym printVar) >> printUnstyled) [] @@ -243,7 +243,8 @@ module ArithmeticExprs = module BooleanExprs = let check (env : VarMap) (ast : Expression) (expectedExpr : TypedBoolExpr>) = - let actualBoolExpr = okOption <| modelBoolExpr env environ id ast + let e = Env.env environ env + let actualBoolExpr = okOption <| modelBoolExpr e Env.Shared id ast AssertAreEqual(Some expectedExpr, actualBoolExpr) [] diff --git a/Var.fs b/Var.fs index 6bf248d..f98d1be 100644 --- a/Var.fs +++ b/Var.fs @@ -205,6 +205,119 @@ module VarMap = Seq.map (fun (name, ty) -> withType ty name) (Map.toSeq vmap) +/// +/// Module for variable environments. +/// +module Env = + /// + /// A full variable environment. + /// + type Env = + { /// The set of thread-local variables. + TVars : VarMap + /// The set of shared variables. + SVars : VarMap } + + /// + /// Creates an . + /// + /// The thread-local variable map. + /// The shared variable map. + /// An environment with the given variable maps. + let env tvars svars = { TVars = tvars; SVars = svars } + + /// + /// A variable scope. + /// + type Scope = + | /// Look up variables in thread-local scope. + Thread + | /// + /// Look up variables in shared scope. + /// Switch to thread scope for indices, and full scope for + /// symbols. + /// + Shared + | /// Look up variables in local first, then shared. + Full + | /// + /// Look up variables in the given local map first, then the next + /// scope. + /// + WithMap of map : VarMap * rest : Scope + + /// + /// Given a scope, return the appropriate scope for indices. + /// + /// The scope to change for indices. + /// The appropriate symbol scope. + let rec indexScopeOf (scope : Scope) : Scope = + match scope with + | WithMap (map, rest) -> WithMap (map, indexScopeOf rest) + | x -> Thread + + /// + /// Given a scope, return the appropriate scope for symbolics. + /// + /// + /// This function exists because, when processing a shared-scope + /// expression and encountering a symbol, we allow thread-local + /// variables to appear in the symbol body. + /// + /// + /// The scope to change for symbols. + /// The appropriate symbol scope. + let rec symbolicScopeOf (scope : Scope) : Scope = + match scope with + | WithMap (map, rest) -> WithMap (map, symbolicScopeOf rest) + | Shared -> Full + | x -> x + + /// + /// Looks up a variable in an environment. + /// + /// The to look up. + /// The scope at which to look up. + /// The variable to look up. + /// + /// A Chessie result in terms of , containing + /// the variable record on success. + /// + let rec lookup (env : Env) (scope : Scope) (var : Var) + : Result, VarMapError> = + match scope with + | Thread -> + VarMap.lookup env.TVars var + | Shared -> + VarMap.lookup env.SVars var + | Full -> + (* Currently, the order doesn't matter as both are disjoint. + However, one day, it might, in which case the thread scope is + 'closer' to program code. *) + match VarMap.lookup env.TVars var with + | Ok (x, e) -> Ok (x, e) + | _ -> + // TODO(MattWindsor91): handle errors properly + VarMap.lookup env.SVars var + | WithMap (map, rest) -> + match VarMap.lookup map var with + | Ok (x, e) -> Ok (x, e) + | _ -> lookup env rest var + + /// + /// Tries to look up a variable in an environment. + /// + /// The to look up. + /// The scope at which to look up. + /// The variable to look up. + /// + /// An option, containing the variable record on success. + /// + let tryLookup (env : Env) (scope : Scope) (var : Var) + : CTyped option = + okOption (lookup env scope var) + + (* * Variable constructors *)