Merge pull request #40 from GaloisInc/jhx/cond-write

Add conditional write support (useful for ARM)

.travis.yml

@@ -29,6 +29,8 @@ install:
 # Here starts the actual work to be performed for the package under test;
 # any command which exits with a non-zero exit code causes the build to fail.
 script:
+ # Build crucible with no -Werror
+ - stack build crucible
  # Build packages
  - stack build --ghc-options="-Wall -Werror"
  # Run tests

base/macaw-base.cabal

@@ -1,5 +1,5 @@
 name: macaw-base
-version: 0.3.4
+version: 0.3.5
 author: Galois, Inc.
 maintainer: jhendrix@galois.com
 build-type: Simple

base/src/Data/Macaw/AbsDomain/AbsState.hs

@@ -50,6 +50,7 @@ module Data.Macaw.AbsDomain.AbsState
   , stridedInterval
   , finalAbsBlockState
   , addMemWrite
+  , addCondMemWrite
   , transferValue
   , abstractULt
   , abstractULeq
@@ -1240,38 +1241,71 @@ addMemWrite :: ( RegisterInfo (ArchReg arch)
                -- ^ Current processor state.
             -> AbsProcessorState (ArchReg arch) ids
 addMemWrite a memRepr v r =
-  case (transferValue r a, transferValue r v) of
+  addCondMemWrite (\new _ -> new) a memRepr (transferValue r v) r
+
+-- | Update the processor state with a potential memory write.
+addCondMemWrite :: ( RegisterInfo r
+                   , MemWidth (RegAddrWidth r)
+                   , HasCallStack
+                   , r ~ ArchReg arch
+                   )
+                => (AbsValue (RegAddrWidth r) tp
+                    -> AbsValue (RegAddrWidth r) tp
+                    -> AbsValue (RegAddrWidth r) tp)
+                -- ^ Updaete function that takes new value, old value and returns value to insert.
+                -> Value arch ids (BVType (RegAddrWidth r))
+                -- ^ Address that we are writing to.
+                -> MemRepr tp
+                -- ^ Information about how value should be represented in memory.
+                -> AbsValue (RegAddrWidth r) tp
+               -- ^ Value to write to memory
+                -> AbsProcessorState r ids
+                -- ^ Current processor state.
+                -> AbsProcessorState r ids
+addCondMemWrite f a memRepr v_abs r =
+  case transferValue r a of
     -- (_,TopV) -> r
     -- We overwrite _some_ stack location.  An alternative would be to
     -- update everything with v.
-    (SomeStackOffset _, _) -> do
+    SomeStackOffset _ -> do
       let cur_ip = r^.absInitialRegs^.curIP
       debug DAbsInt ("addMemWrite: dropping stack at "
              ++ show (pretty cur_ip)
              ++ " via " ++ show (pretty a)
              ++" in SomeStackOffset case") $
         r & curAbsStack %~ pruneStack
-    (StackOffset _ s, v_abs) ->
+    StackOffset _ s ->
       let w = fromInteger (memReprBytes memRepr)
-          e = StackEntry memRepr v_abs
           stk0 = r^.curAbsStack
           -- Delete information about old assignment
           stk1 = Set.fold (\o m -> deleteRange o (o+w) m) stk0 s
           -- Add information about new assignment
           stk2 =
             case Set.toList s of
-              [o] | v_abs /= TopV -> Map.insert o e stk1
+              [o] | -- Skip if new value is top
+                    v_abs /= TopV
+                    -- Lookup existing value at tack
+                  , oldAbs <-
+                      case Map.lookup o stk0 of
+                        Just (StackEntry oldMemRepr old)
+                          | Just Refl <- testEquality memRepr oldMemRepr -> old
+                        _ -> top
+                    -- Computed merged value
+                  , mergedValue <- f v_abs oldAbs
+                    -- Insert only non-top values
+                  , mergedValue /= TopV ->
+                    Map.insert o (StackEntry memRepr mergedValue) stk1
               _ -> stk1
        in r & curAbsStack .~ stk2
     -- FIXME: nuke stack on an unknown address or Top?
     _ -> r
 
+-- | Returns true if return address is known to sit on stack.
 absStackHasReturnAddr :: AbsBlockState r -> Bool
 absStackHasReturnAddr s = isJust $ find isReturnAddr (Map.elems (s^.startAbsStack))
   where isReturnAddr (StackEntry _ ReturnAddr) = True
         isReturnAddr _ = False
 
-
 -- | Return state for after value has run.
 finalAbsBlockState :: forall a ids
                    .  ( RegisterInfo (ArchReg a)

base/src/Data/Macaw/Analysis/FunctionArgs.hs

@@ -520,6 +520,7 @@ stmtDemandedValues ctx stmt = demandConstraints ctx $
       | otherwise ->
           []
     WriteMem addr _ v -> [Some addr, Some v]
+    CondWriteMem cond addr _ v -> [Some cond, Some addr, Some v]
     InstructionStart _ _ -> []
     -- Comment statements have no specific value.
     Comment _ -> []

base/src/Data/Macaw/CFG/Block.hs

@@ -44,8 +44,6 @@ data TermStmt arch ids
     --
     -- The registers include the state of registers just before the terminal statement
     -- executes.
-    -- The address returns the address within the current function that this terminal
-    -- statement could return to (if any)
   | ArchTermStmt !(ArchTermStmt arch ids)
                  !(RegState (ArchReg arch) (Value arch ids))
 

base/src/Data/Macaw/CFG/Core.hs

@@ -1,7 +1,4 @@
 {-|
-Copyright        : (c) Galois, Inc 2015-2017
-Maintainer       : Joe Hendrix <jhendrix@galois.com>
-
 Defines data types needed to represent values, assignments, and statements from Machine code.
 
 This is a low-level CFG representation where the entire program is a
@@ -23,7 +20,6 @@ single CFG.
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
-
 module Data.Macaw.CFG.Core
   ( -- * Stmt level declarations
     Stmt(..)
@@ -55,6 +51,7 @@ module Data.Macaw.CFG.Core
   , mkRegStateM
   , mapRegsWith
   , traverseRegsWith
+  , traverseRegsWith_
   , zipWithRegState
   , ppRegMap
   -- * Pretty printing
@@ -416,6 +413,13 @@ traverseRegsWith :: Applicative m
                  -> m (RegState r g)
 traverseRegsWith f (RegState m) = RegState <$> MapF.traverseWithKey f m
 
+-- | Traverse the register state with the name of each register and value.
+traverseRegsWith_ :: Applicative m
+                  => (forall tp. r tp -> f tp -> m ())
+                  -> RegState r f
+                  -> m ()
+traverseRegsWith_ f (RegState m) = MapF.traverseWithKey_ f m
+
 -- | Traverse the register state with the name of each register and value.
 mapRegsWith :: Applicative m
                  => (forall tp. r tp -> f tp -> g tp)
@@ -713,21 +717,30 @@ instance ( RegisterInfo r
 data Stmt arch ids
    = forall tp . AssignStmt !(Assignment arch ids tp)
    | forall tp . WriteMem !(ArchAddrValue arch ids) !(MemRepr tp) !(Value arch ids tp)
-     -- ^ This denotes a write to memory, and consists of an address to write to, a `MemRepr` defining
+     -- ^ This denotes a write to memory, and consists of an address
-     -- how the value should be stored in memory, and the value to be written.
+     -- to write to, a `MemRepr` defining how the value should be
+     -- stored in memory, and the value to be written.
+  | forall tp .
+    CondWriteMem !(Value arch ids BoolType)
+                 !(ArchAddrValue arch ids)
+                 !(MemRepr tp)
+                 !(Value arch ids tp)
+     -- ^ This denotes a write to memory that only executes if the
+     -- condition is true.
    | InstructionStart !(ArchAddrWord arch) !Text
      -- ^ The start of an instruction
      --
-     -- The information includes the offset relative to the start of the block and the
+     -- The information includes the offset relative to the start of
-     -- disassembler output if available (or empty string if unavailable)
+     -- the block and the disassembler output if available (or empty
+     -- string if unavailable)
    | Comment !Text
      -- ^ A user-level comment
    | ExecArchStmt !(ArchStmt arch (Value arch ids))
      -- ^ Execute an architecture specific statement
    | ArchState !(ArchMemAddr arch) !(MapF.MapF (ArchReg arch) (Value arch ids))
-     -- ^ Address of an instruction and the *machine* registers that it updates
+     -- ^ Address of an instruction and the *machine* registers that
-     -- (with their associated macaw values after the execution of the
+     -- it updates (with their associated macaw values after the
-     -- instruction).
+     -- execution of the instruction).
 
 ppStmt :: ArchConstraints arch
        => (ArchAddrWord arch -> Doc)
@@ -737,7 +750,10 @@ ppStmt :: ArchConstraints arch
 ppStmt ppOff stmt =
   case stmt of
     AssignStmt a -> pretty a
-    WriteMem a _ rhs -> text "write_mem" <+> prettyPrec 11 a <+> ppValue 0 rhs
+    WriteMem     a _ rhs ->
+      text "write_mem" <+> prettyPrec 11 a <+> ppValue 0 rhs
+    CondWriteMem c a _ rhs ->
+      text "cond_write_mem" <+> prettyPrec 11 c <+> prettyPrec 11 a <+> ppValue 0 rhs
     InstructionStart off mnem -> text "#" <+> ppOff off <+> text (Text.unpack mnem)
     Comment s -> text $ "# " ++ Text.unpack s
     ExecArchStmt s -> ppArchStmt (ppValue 10) s

base/src/Data/Macaw/CFG/DemandSet.hs

@@ -110,6 +110,10 @@ addStmtDemands s =
     WriteMem addr _repr val -> do
       addValueDemands addr
       addValueDemands val
+    CondWriteMem cond addr _repr val -> do
+      addValueDemands cond
+      addValueDemands addr
+      addValueDemands val
     InstructionStart{} ->
       pure ()
     Comment _ ->
@@ -129,6 +133,7 @@ stmtNeeded :: AssignIdSet ids -> Stmt arch ids -> Bool
 stmtNeeded demandSet stmt =
   case stmt of
     AssignStmt a -> Set.member (Some (assignId a)) demandSet
+    CondWriteMem{} -> True
     WriteMem{} -> True
     InstructionStart{} -> True
     Comment{} -> True

base/src/Data/Macaw/CFG/Rewriter.hs

@@ -716,6 +716,11 @@ rewriteStmt s =
       tgtAddr <- rewriteValue addr
       tgtVal  <- rewriteValue val
       appendRewrittenStmt $ WriteMem tgtAddr repr tgtVal
+    CondWriteMem cond addr repr val -> do
+      tgtCond <- rewriteValue cond
+      tgtAddr <- rewriteValue addr
+      tgtVal  <- rewriteValue val
+      appendRewrittenStmt $ CondWriteMem tgtCond tgtAddr repr tgtVal
     Comment cmt ->
       appendRewrittenStmt $ Comment cmt
     InstructionStart off mnem ->

base/src/Data/Macaw/Discovery/AbsEval.hs

@@ -76,8 +76,10 @@ absEvalStmt info stmt = withArchConstraints info $
   case stmt of
     AssignStmt a ->
       modify $ addAssignment info a
-    WriteMem addr memRepr v ->
+    WriteMem addr memRepr v -> do
-      modify $ addMemWrite addr memRepr v
+      modify $ \s -> addMemWrite addr memRepr v s
+    CondWriteMem _cond addr memRepr v ->
+      modify $ \s -> addCondMemWrite lub addr memRepr (transferValue s v) s
     InstructionStart _ _ ->
       pure ()
     Comment{} ->

deps/crucible

@@ -1 +1 @@
-Subproject commit 75343267ccacfa9fdb71c82efdce12908ba5ca33
+Subproject commit 4908e20654a753f7f5799a062070ecd6fba44359

deps/parameterized-utils

@@ -1 +1 @@
-Subproject commit 05fa5d2a58dfd531ffab97b913ea108d910349d6
+Subproject commit e4fc7f5a7d58ce28b8b59c0d27358058fe096751

submodules/dismantle

@@ -1 +1 @@
-Subproject commit 8be3748b74daa44b11195203569ba91a3ac6b4fd
+Subproject commit 13979c7b863b0afc5cebdeaf7f3d94a929d07524

submodules/semmc

@@ -1 +1 @@
-Subproject commit 1cb5a6d182fcadbac2296893b713f3fedaaa408c
+Subproject commit 6b045557e3714d5c4037015b9ec1cf88558f239e

symbolic/src/Data/Macaw/Symbolic.hs

@@ -843,6 +843,12 @@ execMacawStmtExtension (SB.MacawArchEvalFn archStmtFn) mvar globs (MO.LookupFunc
       ptr <- tryGlobPtr sym mem globs (C.regValue ptr0)
       mem1 <- doWriteMem sym mem addrWidth memRep ptr (C.regValue v)
       pure ((), setMem st mvar mem1)
+    MacawCondWriteMem addrWidth memRep cond ptr0 v -> do
+      let sym = st^.C.stateSymInterface
+      mem <- getMem st mvar
+      ptr <- tryGlobPtr sym mem globs (C.regValue ptr0)
+      mem1 <- doCondWriteMem sym mem addrWidth memRep (C.regValue cond) ptr (C.regValue v)
+      pure ((), setMem st mvar mem1)
     MacawGlobalPtr w addr ->
       M.addrWidthClass w $ doGetGlobal st mvar globs addr
 

symbolic/src/Data/Macaw/Symbolic/CrucGen.hs

@@ -359,6 +359,16 @@ data MacawStmtExtension (arch :: K.Type)
     -> !(f (ToCrucibleType tp))
     -> MacawStmtExtension arch f C.UnitType
 
+  -- | Write to memory id  xonsiriob is true
+  MacawCondWriteMem
+    :: !(ArchAddrWidthRepr arch)
+    -> !(M.MemRepr tp)
+    -- Condition
+    -> !(f C.BoolType)
+    -> !(f (ArchAddrCrucibleType arch))
+    -> !(f (ToCrucibleType tp))
+    -> MacawStmtExtension arch f C.UnitType
+
   -- | Convert a literal address (from Macaw) into a pointer in the LLVM memory model
   MacawGlobalPtr
     :: !(ArchAddrWidthRepr arch)
@@ -489,9 +499,10 @@ instance (C.PrettyApp (MacawArchStmtExtension arch),
         -> (forall (x :: C.CrucibleType) . MacawStmtExtension arch f x -> Doc)
   ppApp f a0 =
     case a0 of
-      MacawReadMem _ r a     -> sexpr "macawReadMem"       [pretty r, f a]
+      MacawReadMem     _  r   a   -> sexpr "macawReadMem"      [pretty r, f a]
-      MacawCondReadMem _ r c a d -> sexpr "macawCondReadMem" [pretty r, f c, f a, f d ]
+      MacawCondReadMem _  r c a d -> sexpr "macawCondReadMem"  [pretty r, f c, f a, f d ]
-      MacawWriteMem _ r a v  -> sexpr "macawWriteMem"      [pretty r, f a, f v]
+      MacawWriteMem     _ r   a v -> sexpr "macawWriteMem"     [pretty r, f a, f v]
+      MacawCondWriteMem _ r c a v -> sexpr "macawCondWriteMem" [f c, pretty r, f a, f v]
       MacawGlobalPtr _ x -> sexpr "global" [ text (show x) ]
 
       MacawFreshSymbolic r -> sexpr "macawFreshSymbolic" [ text (show r) ]
@@ -519,6 +530,7 @@ instance C.TypeApp (MacawArchStmtExtension arch)
   appType (MacawReadMem _ r _) = memReprToCrucible r
   appType (MacawCondReadMem _ r _ _ _) = memReprToCrucible r
   appType (MacawWriteMem _ _ _ _) = C.knownRepr
+  appType MacawCondWriteMem{} = C.knownRepr
   appType (MacawGlobalPtr w _)
     | LeqProof <- addrWidthIsPos w = MM.LLVMPointerRepr (M.addrWidthNatRepr w)
   appType (MacawFreshSymbolic r) = typeToCrucible r
@@ -1178,6 +1190,12 @@ addMacawStmt baddr stmt =
       cval  <- valueToCrucible val
       w     <- archAddrWidth
       void $ evalMacawStmt (MacawWriteMem w repr caddr cval)
+    M.CondWriteMem cond addr repr val -> do
+      ccond <- valueToCrucible cond
+      caddr <- valueToCrucible addr
+      cval  <- valueToCrucible val
+      w     <- archAddrWidth
+      void $ evalMacawStmt (MacawCondWriteMem w repr ccond caddr cval)
     M.InstructionStart off t -> do
       -- Update the position
       modify' $ \s -> s { codeOff = off

symbolic/src/Data/Macaw/Symbolic/MemOps.hs

@@ -23,6 +23,7 @@ module Data.Macaw.Symbolic.MemOps
   , doReadMem
   , doCondReadMem
   , doWriteMem
+  , doCondWriteMem
   , doGetGlobal
   , doLookupFunctionHandle
   , doPtrToBits
@@ -805,3 +806,35 @@ doWriteMem sym mem ptrWidth memRep ptr val = hasPtrClass ptrWidth $
      let alignment = noAlignment -- default to byte alignment (FIXME)
      let memVal = resolveMemVal memRep ty val
      Mem.storeRaw sym mem ptr ty alignment memVal
+
+
+-- | Write a Macaw value to memory if a condition holds.
+--
+--     arg1 : Symbolic Interface
+--     arg2 : Heap prior to write
+--     arg3 : Width of ptr
+--     arg4 : What/how we are writing
+--     arg5 : Condition that must hold if we write.
+--     arg6 : Address to write to
+--     arg7 : Value to write
+doCondWriteMem ::
+  IsSymInterface sym =>
+  sym ->
+  MemImpl sym ->
+  M.AddrWidthRepr ptrW ->
+  MemRepr ty ->
+  Pred sym ->
+  LLVMPtr sym ptrW ->
+  RegValue sym (ToCrucibleType ty) ->
+  IO (MemImpl sym)
+doCondWriteMem sym mem ptrWidth memRep cond ptr val = hasPtrClass ptrWidth $
+  do ok <- isValidPtr sym mem ptrWidth ptr
+     condOk <- impliesPred sym cond ok
+     check sym condOk "doWriteMem" $
+       "Write to an invalid location: " ++ show (Mem.ppPtr ptr)
+     ty <- case memReprToStorageType (getEnd mem) memRep of
+             Left msg -> throwIO $ userError msg
+             Right tp -> pure tp
+     let alignment = noAlignment -- default to byte alignment (FIXME)
+     let memVal = resolveMemVal memRep ty val
+     Mem.condStoreRaw sym mem cond ptr ty alignment memVal

x86/src/Data/Macaw/X86.hs

@@ -580,6 +580,8 @@ x86DemandContext =
                 , archFnHasSideEffects = x86PrimFnHasSideEffects
                 }
 
+-- | Get the next IP that may run after this terminal and the abstract
+-- state denoting possible starting conditions when that code runs.
 postX86TermStmtAbsState :: (forall tp . X86Reg tp -> Bool)
                         -> Memory 64
                         -> AbsBlockState X86Reg