diff --git a/AST.fs b/AST.fs index edd652c..d1500fa 100644 --- a/AST.fs +++ b/AST.fs @@ -73,6 +73,10 @@ module Types = | Assume of Expression // | SymAtomic of symbol : Symbolic // %{xyz}(x, y) | Havoc of var : string // havoc var + | ACond of + cond : Expression + * trueBranch : Atomic list + * falseBranch : (Atomic list) option and Atomic = Node /// @@ -240,6 +244,43 @@ module Pretty = open Starling.Core.TypeSystem.Pretty open Starling.Core.Var.Pretty + /// + /// Hidden building-blocks for AST pretty-printers. + /// + module private Helpers = + /// Pretty-prints blocks with the given indent level (in spaces). + let printBlock (pCmd : 'Cmd -> Doc) (c : 'Cmd list) : Doc = + braced (ivsep (List.map (pCmd >> Indent) c)) + + /// + /// Pretty-prints an if-then-else. + /// + /// Pretty-printer for conditionals. + /// Pretty-printer for 'then'/'else' legs. + /// The conditional to print. + /// The 'then' leg to print. + /// The optional 'else' leg to print. + /// Type of conditionals. + /// Type of 'then'/'else' leg items. + /// + /// A capturing the if-then-else form. + /// + let printITE + (pCond : 'Cond -> Doc) + (pLeg : 'Leg -> Doc) + (cond : 'Cond) + (thenLeg : 'Leg list) + (elseLeg : ('Leg list) option) + : Doc = + syntaxStr "if" + <+> parened (pCond cond) + <+> printBlock pLeg thenLeg + <+> (maybe + Nop + (fun e -> syntaxStr "else" <+> printBlock pLeg e) + elseLeg) + + /// Pretty-prints Boolean operations. let printBinOp : BinOp -> Doc = function @@ -290,7 +331,7 @@ module Pretty = /// The symbolic to print. /// /// The resulting from printing . - /// + /// and printSymbolic (s : Symbolic) : Doc = String "%" <-> @@ -360,7 +401,7 @@ module Pretty = equality (printExpression dest) (printExpression src) /// Pretty-prints atomic actions. - let printAtomic' : Atomic' -> Doc = + let rec printAtomic' : Atomic' -> Doc = function | CompareAndSwap(l, f, t) -> func "CAS" [ printExpression l @@ -376,13 +417,9 @@ module Pretty = | Assume e -> func "assume" [ printExpression e ] | SymAtomic sym -> printSymbolic sym | Havoc var -> String "havoc" <+> String var - let printAtomic (x : Atomic) : Doc = printAtomic' x.Node - - /// Pretty-prints blocks with the given indent level (in spaces). - let printBlock (pCmd : 'cmd -> Doc) - (c : 'cmd list) - : Doc = - braced (ivsep (List.map (pCmd >> Indent) c)) + | ACond (cond = c; trueBranch = t; falseBranch = f) -> + Helpers.printITE printExpression printAtomic c t f + and printAtomic (x : Atomic) : Doc = printAtomic' x.Node /// Pretty-prints commands. let rec printCommand' (cmd : Command') : Doc = @@ -397,33 +434,33 @@ module Pretty = |> semiSep |> withSemi |> braced |> angled) yield! Seq.map (uncurry printAssign) qs } |> semiSep |> withSemi - | Command'.If(c, t, fo) -> - hsep [ "if" |> String |> syntax - c |> printExpression |> parened - t |> printBlock printCommand - (maybe Nop - (fun f -> - hsep - [ "else" |> String |> syntax - printBlock printCommand f ]) - fo) ] + | Command'.If(c, t, f) -> + Helpers.printITE printExpression printCommand c t f | Command'.While(c, b) -> hsep [ "while" |> String |> syntax c |> printExpression |> parened - b |> printBlock printCommand ] + b |> Helpers.printBlock printCommand ] | Command'.DoWhile(b, c) -> hsep [ "do" |> String |> syntax - b |> printBlock printCommand + b |> Helpers.printBlock printCommand "while" |> String |> syntax c |> printExpression |> parened ] |> withSemi | Command'.Blocks bs -> bs - |> List.map (printBlock printCommand) + |> List.map (Helpers.printBlock printCommand) |> hsepStr "||" | Command'.ViewExpr v -> printMarkedView printView v and printCommand (x : Command) : Doc = printCommand' x.Node + /// + /// Prints a command block. + /// + /// The block to print. + /// A capturing . + let printCommandBlock (block : Command list) : Doc = + Helpers.printBlock printCommand block + /// /// Pretty-prints a type literal. /// @@ -454,7 +491,7 @@ module Pretty = : Doc = hsep [ "method" |> String |> syntax printFunc (printParam >> syntaxIdent) s - printBlock pCmd b ] + Helpers.printBlock pCmd b ] /// Pretty-prints a general view prototype. let printGeneralViewProto (pParam : 'Param -> Doc)(vp : GeneralViewProto<'Param>) : Doc = diff --git a/Collator.fs b/Collator.fs index 2ade66e..5afdf59 100644 --- a/Collator.fs +++ b/Collator.fs @@ -80,7 +80,7 @@ module Pretty = vsep <| Seq.map (printScriptVar "shared") cs.SharedVars vsep <| Seq.map (printScriptVar "thread") cs.ThreadVars vsep <| Seq.map (uncurry printConstraint) cs.Constraints - printMap Indented String (printBlock printCommand) cs.Methods ] + printMap Indented String printCommandBlock cs.Methods ] // Add in search, but only if it actually exists. let all = @@ -188,7 +188,7 @@ module ParamDesugar = let rewriteAFunc { Name = n; Params = ps } = { Name = n; Params = List.map rewriteExpression ps } - let rewriteAtomic atom = + let rec rewriteAtomic atom = let rewriteAtomic' = function | CompareAndSwap (src, test, dest) -> @@ -202,6 +202,11 @@ module ParamDesugar = | SymAtomic sym -> SymAtomic (rewriteSymbolic sym) | Havoc v -> Havoc (rewriteVar v) + | ACond (cond = c; trueBranch = t; falseBranch = f) -> + ACond + (rewriteExpression c, + List.map rewriteAtomic t, + Option.map (List.map rewriteAtomic) f) { atom with Node = rewriteAtomic' atom.Node } let rewritePrimSet { PreAssigns = ps; Atomics = ts; PostAssigns = qs } = diff --git a/Command.fs b/Command.fs index 1901e17..6fb9ddc 100644 --- a/Command.fs +++ b/Command.fs @@ -107,6 +107,11 @@ module Types = | Stored of StoredCommand /// An entirely symbolic command. | SymC of Symbolic>> + /// A branching command. + | PrimBranch of + cond : BoolExpr> + * trueBranch : PrimCommand list + * falseBranch : (PrimCommand list) option override this.ToString() = sprintf "%A" this /// @@ -186,12 +191,14 @@ module Queries = /// true if the command is a no-op; /// false otherwise. /// - let isNop (prim : PrimCommand) : bool = + let rec isNop (prim : PrimCommand) : bool = match prim with // No Intrinsic commands are no-ops at the moment. | Intrinsic _ -> false | Stored { Results = ps } -> List.isEmpty ps | SymC _ -> false + | PrimBranch (trueBranch = t; falseBranch = f) -> + List.forall isNop t && maybe true (List.forall isNop) f /// /// Active pattern matching no-operation commands. @@ -237,14 +244,17 @@ module Queries = /// Combines the results of each command into a list of all results let commandResults cs = - // TODO(CaptainHayashi): are sym working variables really results? - let primResults prim = + let rec primResults prim = match prim with | Intrinsic (IAssign r) -> [ Expr.Int (r.TypeRec, r.LValue) ] | Intrinsic (BAssign r) -> [ Expr.Bool (r.TypeRec, r.LValue) ] | Intrinsic (Havoc v) -> [ mkVarExp (mapCTyped Reg v) ] | Stored { Results = rs } -> rs | SymC _ -> [] + // TODO(MattWindsor91): is this correct? + | PrimBranch (trueBranch = t; falseBranch = f) -> + concatMap primResults t + @ maybe [] (concatMap primResults) f List.fold (fun a c -> a @ primResults c) [] cs @@ -272,7 +282,7 @@ module Queries = | SymArg a -> Some a | _ -> None - let f prim = + let rec f prim = match prim with // TODO(CaptainHayashi): is this sensible!? | Stored { Args = xs } -> List.map symExprVars xs @@ -280,6 +290,10 @@ module Queries = | Intrinsic (IAssign { RValue = y } ) -> [ symExprVars (indefIntExpr y) ] | Intrinsic (BAssign { RValue = y } ) -> [ symExprVars (indefBoolExpr y) ] | Intrinsic (Havoc _) -> [] + // TODO(CaptainHayashi): is this sensible!? + | PrimBranch (trueBranch = t; falseBranch = fb) -> + concatMap f t @ maybe [] (concatMap f) fb + let vars = collect (concatMap f cmd) lift Set.unionMany vars @@ -454,11 +468,19 @@ module Pretty = <-> String "}" /// Pretty-prints a PrimCommand. - let printPrimCommand (prim : PrimCommand) : Doc = + let rec printPrimCommand (prim : PrimCommand) : Doc = match prim with | Intrinsic s -> printIntrinsicCommand s | Stored s -> printStoredCommand s | SymC s -> printSymCommand s + | PrimBranch (cond = c; trueBranch = t; falseBranch = f) -> + vsep + [ String "if" <+> printBoolExpr (printSym printVar) c + headed "then" (List.map printPrimCommand t) + maybe + Nop + (fun x -> headed "else" (List.map printPrimCommand x)) + f ] /// Pretty-prints a Command. let printCommand : Command -> Doc = List.map printPrimCommand >> semiSep diff --git a/Modeller.fs b/Modeller.fs index 7ab02d6..39a245a 100644 --- a/Modeller.fs +++ b/Modeller.fs @@ -166,6 +166,8 @@ module Types = | PrimNotImplemented of what : string /// Handling variables in symbolic prims caused an error. | SymVarError of err : VarMapError + /// An atomic branch contains a bad if-then-else condition. + | BadAtomicITECondition of expr: AST.Types.Expression * err: ExprError /// Represents an error when converting a method. type MethodError = @@ -378,6 +380,9 @@ module Pretty = | SymVarError err -> errorStr "error in translating symbolic command" <&> printVarMapError err + | BadAtomicITECondition (expr, err) -> + wrapped "if-then-else condition" (printExpression expr) + (printExprError err) /// Pretty-prints method errors. let printMethodError (err : MethodError) : Doc = @@ -1721,8 +1726,8 @@ let modelPostfix (ctx : MethodContext) (operand : Expression) (mode : FetchMode) /// Converts a single atomic command from AST to part-commands. let rec modelAtomic (ctx : MethodContext) (a : Atomic) : Result = - let prim = - match a.Node with + let rec prim n = + match n.Node with | CompareAndSwap(dest, test, set) -> modelCAS ctx dest test set | Fetch(dest, src, mode) -> modelFetch ctx dest src mode | Postfix(operand, mode) -> modelPostfix ctx operand mode @@ -1734,8 +1739,6 @@ let rec modelAtomic | Havoc var -> 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 symMR = @@ -1743,12 +1746,25 @@ let rec modelAtomic (wrapMessages BadExpr (modelExpr ctx.Env Full id)) sym) lift SymC symMR + | ACond (cond = c; trueBranch = t; falseBranch = f) -> + let cTMR = + wrapMessages BadExpr (modelBoolExpr ctx.Env Full id) c + // An if condition needs to be of type 'bool', not a subtype. + let cMR = + bind + (checkBoolIsNormalType + >> mapMessages (fun m -> BadAtomicITECondition (c, ExprBadType m))) + cTMR + let tMR = collect (List.map prim t) + let fMR = maybe (ok None) (List.map prim >> collect >> lift Some) f + lift3 (curry3 PrimBranch) cMR tMR fMR + lift (function | Stored cmd -> Stored { cmd with Node = Some a } | x -> x) - prim + (prim a) /// Converts a local variable assignment to a Prim. and modelAssign diff --git a/Optimiser.fs b/Optimiser.fs index ae19a5f..4882ac2 100644 --- a/Optimiser.fs +++ b/Optimiser.fs @@ -576,7 +576,7 @@ module Graph = | Ok (pvars, _) -> Seq.forall typedVarIsThreadLocal (Set.toSeq pvars) - let isLocalPrim prim = + let rec isLocalPrim prim = match prim with | // TODO(CaptainHayashi): too conservative? SymC _ -> false @@ -585,6 +585,10 @@ module Graph = | // TODO(CaptainHayashi): is this correct? Intrinsic (Havoc v) -> typedVarIsThreadLocal v | Stored { Args = ps } -> Seq.forall isLocalArg ps + | PrimBranch (trueBranch = t; falseBranch = f) -> + List.forall isLocalPrim t + && maybe true (List.forall isLocalPrim) f + List.forall isLocalPrim cmd diff --git a/Pretty.fs b/Pretty.fs index 3e01eff..b296734 100644 --- a/Pretty.fs +++ b/Pretty.fs @@ -57,6 +57,7 @@ let warning d = Styled([Yellow], d) let success d = Styled([Green], d) let inconclusive d = Styled([Blue], d) +let syntaxStr s = syntax (String s) let errorStr s = error (String s) let errorContextStr s = errorContext (String s) let errorInfoStr s = errorInfo (String s) diff --git a/Semantics.fs b/Semantics.fs index def4409..27c74ff 100644 --- a/Semantics.fs +++ b/Semantics.fs @@ -617,10 +617,10 @@ let microcodeRoutineToBool /// The map from command to microcode schemata. /// The primitive command to instantiate. /// -/// If the instantiation succeeded, the resulting list of parallel-composed +/// If the instantiation succeeded, the resulting list of /// instructions. /// -let instantiateToMicrocode +let rec instantiateToMicrocode (semantics : PrimSemanticsMap) (prim : PrimCommand) : Result>, Sym> list, Error> = @@ -650,6 +650,16 @@ let instantiateToMicrocode mapMessages Traversal (mapTraversal subInMCode s.Body) bind instantiate typeCheckedDefR + | PrimBranch (cond = c; trueBranch = t; falseBranch = f) -> + let inst = + List.map (instantiateToMicrocode semantics) + >> collect + >> lift List.concat + + lift2 + (fun tM fM -> [ Branch (c, tM, fM) ]) + (inst t) + (maybe (ok []) inst f) /// /// Translates a command to a multi-state Boolean expression.