Skip to content

Commit

Permalink
Semantics: add havoc and slightly fix array unsoundness
Browse files Browse the repository at this point in the history 
This implements havoc by making assignment targets optional.

Also fixed a typo in the array normalisation.  See #114 for the
remaining array problem.
  • Loading branch information
@MattWindsor91
MattWindsor91 committed Dec 2, 2016
1 parent d45b0c8 commit ea8af51
Show file tree
Hide file tree
Showing 4 changed files with 196 additions and 95 deletions.
17 changes: 15 additions & 2 deletions Model.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,8 +59,8 @@ module Types =
/// <typeparam name="L">The type of lvalues.</typeparam>
/// <typeparam name="RV">The type of rvalue variables.</typeparam>
type Microcode<'L, 'RV> when 'RV : equality =
/// <summary>An assignment.</summary>
| Assign of lvalue : 'L * rvalue : Expr<'RV>
/// <summary>An assignment, perhaps nondeterministic.</summary>
| Assign of lvalue : 'L * rvalue : Expr<'RV> option
/// <summary>A diverging assertion.</summary>
| Assume of assumption : BoolExpr<'RV>
/// <summary>A conditional.</summary>
Expand Down Expand Up @@ -200,6 +200,19 @@ module Types =
DeferredChecks : DeferredCheck list }


/// <summary>
/// Creates a deterministic assign.
/// </summary>
let ( *<- ) (lv : 'L) (rv : Expr<'RV>) : Microcode<'L, 'RV> =
Assign (lv, Some rv)

/// <summary>
/// Creates a nondeterministic assign.
/// </summary>
let havoc (lv : 'L) : Microcode<'L, 'RV> =
Assign (lv, None)


/// <summary>
/// Pretty printers for the model.
/// </summary>
Expand Down
41 changes: 21 additions & 20 deletions Modeller.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -421,6 +421,7 @@ let mkPrim (name : string) (results : TypedVar list) (args : TypedVar list)
: PrimSemantics =
{ Name = name; Results = results; Args = args; Body = body }


/// <summary>
/// The core semantic function for the imperative language.
/// </summary>
Expand All @@ -442,70 +443,70 @@ let coreSemantics : PrimSemanticsMap =
(mkPrim "ICAS" [ Int "destA"; Int "testA" ] [ Int "destB"; Int "testB"; Int "set" ]
[ Branch
(iEq (IVar "destB") (IVar "testB"),
[ Assign (Int "destA", Int (IVar "set"))
Assign (Int "testA", Int (IVar "testB")) ],
[ Assign (Int "destA", Int (IVar "destB"))
Assign (Int "testA", Int (IVar "destB")) ] ) ] )
[ Int "destA" *<- Int (IVar "set")
Int "testA" *<- Int (IVar "testB") ],
[ Int "destA" *<- Int (IVar "destB")
Int "testA" *<- Int (IVar "destB") ] ) ] )
// Boolean CAS
(mkPrim "BCAS" [ Bool "destA"; Bool "testA" ] [ Bool "destB"; Bool "testB"; Bool "set" ]
[ Branch
(bEq (BVar "destB") (BVar "testB"),
[ Assign (Bool "destA", Bool (BVar "set"))
Assign (Bool "testA", Bool (BVar "testB")) ],
[ Assign (Bool "destA", Bool (BVar "destB"))
Assign (Bool "testA", Bool (BVar "destB")) ] ) ] )
[ Bool "destA" *<- Bool (BVar "set")
Bool "testA" *<- Bool (BVar "testB") ],
[ Bool "destA" *<- Bool (BVar "destB")
Bool "testA" *<- Bool (BVar "destB") ] ) ] )
(*
* Atomic load
*)
// Integer load
(mkPrim "!ILoad" [ Int "dest" ] [ Int "src" ]
[ Assign (Int "dest", Int (IVar "src")) ] )
[ Int "dest" *<- Int (IVar "src") ] )

// Integer load-and-increment
(mkPrim "!ILoad++" [ Int "dest"; Int "srcA" ] [ Int "srcB" ]
[ Assign (Int "dest", Int (IVar "srcB"))
Assign (Int "srcA", Int (mkAdd2 (IVar "srcB") (IInt 1L))) ] )
[ Int "dest" *<- Int (IVar "srcB")
Int "srcA" *<- Int (mkAdd2 (IVar "srcB") (IInt 1L)) ] )

// Integer load-and-decrement
(mkPrim "!ILoad--" [ Int "dest"; Int "srcA" ] [ Int "srcB" ]
[ Assign (Int "dest", Int (IVar "srcB"))
Assign (Int "srcA", Int (mkSub2 (IVar "srcB") (IInt 1L))) ] )
[ Int "dest" *<- Int (IVar "srcB")
Int "srcA" *<- Int (mkSub2 (IVar "srcB") (IInt 1L)) ] )

// Integer increment
(mkPrim "!I++" [ Int "srcA" ] [ Int "srcB" ]
[ Assign (Int "srcA", Int (mkAdd2 (IVar "srcB") (IInt 1L))) ] )
[ Int "srcA" *<- Int (mkAdd2 (IVar "srcB") (IInt 1L)) ] )

// Integer decrement
(mkPrim "!I--" [ Int "srcA" ] [ Int "srcB" ]
[ Assign (Int "srcA", Int (mkSub2 (IVar "srcB") (IInt 1L))) ] )
[ Int "srcA" *<- Int (mkSub2 (IVar "srcB") (IInt 1L)) ] )

// Boolean load
(mkPrim "!BLoad" [ Bool "dest" ] [ Bool "src" ]
[ Assign (Bool "dest", Bool (BVar "src")) ] )
[ Bool "dest" *<- Bool (BVar "src") ] )

(*
* Atomic store
*)

// Integer store
(mkPrim "!IStore" [ Int "dest" ] [ Int "src" ]
[ Assign (Int "dest", Int (IVar "src")) ] )
[ Int "dest" *<- Int (IVar "src") ] )

// Boolean store
(mkPrim "!BStore" [ Bool "dest" ] [ Bool "src" ]
[ Assign (Bool "dest", Bool (BVar "src")) ] )
[ Bool "dest" *<- Bool (BVar "src") ] )

(*
* Local set
*)

// Integer local set
(mkPrim "!ILSet" [ Int "dest" ] [ Int "src" ]
[ Assign (Int "dest", Int (IVar "src")) ] )
[ Int "dest" *<- Int (IVar "src") ] )

// Boolean store
(mkPrim "!BLSet" [ Bool "dest" ] [ Bool "src" ]
[ Assign (Bool "dest", Bool (BVar "src")) ] )
[ Bool "dest" *<- Bool (BVar "src") ] )

(*
* Assumptions
Expand Down
55 changes: 33 additions & 22 deletions Semantics.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -106,8 +106,8 @@ module Pretty =
/// of an variable have been modified by a command.
/// </summary>
type Write =
/// <summary>The entire lvalue has been written to.</summary>
| Entire of newVal : Expr<Sym<Var>>
/// <summary>The entire lvalue has been written to or havoc'd.</summary>
| Entire of newVal : Expr<Sym<Var>> option
/// <summary>
/// Only certain parts of the lvalue have been written to,
/// and their recursive write records are enclosed.
Expand All @@ -127,7 +127,7 @@ type Write =
/// <param name="map">The write map being extended.</param>
/// <returns>The extended write map.</returns>
let markWrite (var : TypedVar) (idxPath : IntExpr<Sym<Var>> list)
(value : Expr<Sym<Var>>)
(value : Expr<Sym<Var>> option)
(map : Map<TypedVar, Write>)
: Map<TypedVar, Write> =
(* First, consider what it means to add an index write to an index write
Expand Down Expand Up @@ -218,7 +218,7 @@ let varAndIdxPath (expr : Expr<Sym<Var>>)
/// </summary>
/// <param name="assigns">The assignment list to investigate.</param>
/// <returns>The write map for that microcode list.</returns>
let makeWriteMap (assigns : (Expr<Sym<Var>> * Expr<Sym<Var>>) list)
let makeWriteMap (assigns : (Expr<Sym<Var>> * Expr<Sym<Var>> option) list)
: Map<TypedVar, Write> =
let addToWriteMap map (lv, rv) =
// TODO(CaptainHayashi): complain if lv isn't a lvalue?
Expand All @@ -234,7 +234,7 @@ let makeWriteMap (assigns : (Expr<Sym<Var>> * Expr<Sym<Var>>) list)
/// and a list of (unpartitioned) microcode branches.
/// </returns>
let partitionMicrocode (instrs : Microcode<Expr<Sym<Var>>, Sym<Var>> list)
: ((Expr<Sym<Var>> * Expr<Sym<Var>>) list
: ((Expr<Sym<Var>> * Expr<Sym<Var>> option) list
* BoolExpr<Sym<Var>> list
* (BoolExpr<Sym<Var>>
* Microcode<Expr<Sym<Var>>, Sym<Var>> list
Expand Down Expand Up @@ -278,36 +278,41 @@ let mkIdx (eltype : Type) (length : int option) (arr : ArrayExpr<Sym<Var>>)
/// <returns>
/// The assignments in entire-variable form, in arbitrary order.
/// </returns>
let normaliseAssigns (assigns : (Expr<Sym<Var>> * Expr<Sym<Var>>) list)
: Result<(TypedVar * Expr<Sym<Var>>) list, Error> =
let normaliseAssigns (assigns : (Expr<Sym<Var>> * Expr<Sym<Var>> option) list)
: Result<(TypedVar * Expr<Sym<Var>> option) list, Error> =
// First, we convert the assigns to a write map.
let wmap = makeWriteMap assigns
(* Then, each item in the write map represents an assignment.
We need to convert each write map entry into an array update or a
direct value. *)
let rec translateRhs lhs =
function
let rec translateRhs lhs (value : Write) =
match value with
| Entire v -> ok v
| Indices ixmap ->
// TODO(CaptainHayashi): proper errors.
match lhs with
| Array (eltype, length, alhs) ->
let addUpdate
(index : IntExpr<Sym<Var>>, value : Write) (lhs' : Expr<Sym<Var>>)
: Result<Expr<Sym<Var>>, Error> =
let addUpdate
(index : IntExpr<Sym<Var>>, value : Write) (lhs' : Expr<Sym<Var>> option)
: Result<Expr<Sym<Var>> option, Error> =
(* TODO(CaptainHayashi): currently, if an array update havocs,
any future updates also havoc. This perhaps throws too much
information away! *)
match lhs' with
| None -> ok None
| Some (Array (eltype, length, alhs)) ->
(* Need to translate any further subscripts inside value.
But, to do that, we need to know what the LHS of those
subscripts is! *)
let vlhs = mkIdx eltype length alhs index
let vrhsResult = translateRhs vlhs value
lift
(fun vrhs ->
Expr.Array
(eltype, length,
AUpd (eltype, length, alhs, index, vrhs)))
(Option.map
(fun vrhs ->
Expr.Array
(eltype, length,
AUpd (eltype, length, alhs, index, vrhs))))
vrhsResult
seqBind addUpdate lhs (Map.toSeq ixmap)
| _ -> fail (BadSemantics "tried to index into a non-array")
| _ -> fail (BadSemantics "tried to index into a non-array")
seqBind addUpdate (Some lhs) (Map.toSeq ixmap)

let translateAssign (lhs : TypedVar, rhs) =
// lhs is a typed variable here, but must be an expression for the above
Expand Down Expand Up @@ -411,7 +416,10 @@ let traverseMicrocode
let tml = tchainL tm id

match mc with
| Assign (lv, rv) -> tchain2 ltrav rtrav Assign ctx (lv, rv)
| Assign (lv, Some rv) ->
tchain2 ltrav rtrav (pairMap id Some >> Assign) ctx (lv, rv)
| Assign (lv, None) ->
tchain ltrav (flip mkPair None >> Assign) ctx lv
| Assume assumption -> tchain brtrav Assume ctx assumption
| Branch (i, t, e) -> tchain3 brtrav tml tml Branch ctx (i, t, e)
tm
Expand Down Expand Up @@ -485,7 +493,10 @@ let rec markedMicrocodeToBool
: BoolExpr<Sym<MarkedVar>> =
let translateInstr instr =
match instr with
| Assign (x, y) -> mkEq (mkVarExp (mapCTyped Reg x)) y
// Havoc
| Assign (x, None) -> BTrue
// Deterministic assignment
| Assign (x, Some y) -> mkEq (mkVarExp (mapCTyped Reg x)) y
| Assume x -> x
| Branch (i, t, e) ->
let tX = markedMicrocodeToBool t
Expand Down
Loading

0 comments on commit ea8af51

Please sign in to comment.