Issue 448

.github/workflows/main.yml

@@ -41,9 +41,12 @@ jobs:
             docker pull artifactory.galois.com:5025/pate/pate:refs-heads-master || \
             echo "No latest image found"
 
+      # Docker on our self-hosted runners doesn't populate TARGETPLATFORM so we
+      # set it manually via build-arg. We need this to pass our platform check
+      # in the Dockerfile.
       - name: Build Docker Image
         run: |
-          docker build . \
+          docker build --platform linux/amd64 --build-arg TARGETPLATFORM=linux/amd64 . \
             --cache-from artifactory.galois.com:5025/pate/pate:${GITHUB_REF//\//\-} \
             --cache-from artifactory.galois.com:5025/pate/pate:refs-heads-master \
             -t pate

Dockerfile

@@ -1,5 +1,8 @@
 ## Clone git into image
-FROM --platform=linux/amd64 ubuntu:20.04 as gitbase
+FROM ubuntu:20.04 AS gitbase
+
+ARG TARGETPLATFORM
+RUN if [ "${TARGETPLATFORM}" != "linux/amd64" ]; then echo "TARGETPLATFORM '${TARGETPLATFORM}' is not supported, use '--platform linux/amd64'"; exit 1; fi
 
 RUN apt update && apt install -y ssh
 RUN apt install -y git
@@ -30,7 +33,7 @@ RUN find . -name .gitignore -exec rm {} \;
 
 
 ## Build project in image
-FROM --platform=linux/amd64 ubuntu:20.04
+FROM ubuntu:20.04
 ENV GHC_VERSION=9.6.2
 ENV TZ=America/Los_Angeles
 RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone
@@ -43,13 +46,13 @@ RUN apt-get install -y yices2
 
 RUN curl https://downloads.haskell.org/~ghcup/x86_64-linux-ghcup -o /usr/bin/ghcup && chmod +x /usr/bin/ghcup
 RUN mkdir -p /root/.ghcup && ghcup install-cabal
-RUN ghcup install ghc ${GHC_VERSION} && ghcup set ghc ${GHC_VERSION} 
+RUN ghcup install ghc ${GHC_VERSION} && ghcup set ghc ${GHC_VERSION}
 
 RUN apt install locales
 RUN locale-gen en_US.UTF-8
-ENV LANG en_US.UTF-8
-ENV LANGUAGE en_US:en
-ENV LC_ALL en_US.UTF-8
+ENV LANG=en_US.UTF-8
+ENV LANGUAGE=en_US:en
+ENV LC_ALL=en_US.UTF-8
 
 
 ######################################################################
@@ -82,7 +85,7 @@ RUN cabal v2-build what4
 # crucible
 COPY --from=gitbase /home/src/submodules/crucible /home/src/submodules/crucible
 RUN cabal v2-build crucible
- 
+
 # arm-asl-parser
 COPY --from=gitbase /home/src/submodules/arm-asl-parser /home/src/submodules/arm-asl-parser
 RUN cabal v2-build asl-parser
@@ -114,7 +117,7 @@ RUN cabal v2-build binary-symbols flexdis86
 #mutual dependency between these submodules
 # macaw
 COPY --from=gitbase /home/src/submodules/macaw /home/src/submodules/macaw
- 
+
 # macaw-loader
 COPY --from=gitbase /home/src/submodules/macaw-loader /home/src/submodules/macaw-loader
 RUN cabal v2-build macaw-base macaw-loader macaw-semmc

README.rst

@@ -12,7 +12,7 @@ The fastest way to get started is to build the Docker image and use the tool via
 
 First, build the Docker image with the command::
 
-  docker build . -t pate
+  docker build --platform linux/amd64 . -t pate
 
 Next, run the verifier on an example::
 
@@ -87,7 +87,7 @@ The verifier accepts the following command line arguments::
   --read-only-segments ARG Mark segments as read-only (0-indexed) when loading
                            ELF
   --script FILENAME        Save macaw CFGs to the provided directory
-  --assume-stack-scope     Add additional assumptions about stack frame scoping 
+  --assume-stack-scope     Add additional assumptions about stack frame scoping
                            during function calls (unsafe)
   --ignore-warnings ARG    Don't raise any of the given warning types
   --always-classify-return Always resolve classifier failures by assuming
@@ -107,13 +107,14 @@ If you have a ``tar`` file of a Docker image of the verifier, you can install it
 
 To run the verifier via Docker after this::
 
-  docker run --rm -it pate --help
+  docker run --rm -it --platform linux/amd64 pate --help
 
 To make use of the verifier with Docker, it is useful to map a directory on your local filesystem into the Docker container to be able to save output files. Assuming that your original and patched binaries are ``original.exe`` and ``patched.exe``, respectively::
 
   mkdir VerifierData
   cp original.exe patched.exe VerifierData/
-  docker run --rm -it -v `pwd`/VerifierData`:/VerifierData pate \
+  docker run --rm -it --platform linux/amd64 \
+             -v `pwd`/VerifierData`:/VerifierData pate \
              --original /VerifierData/original.exe \
              --patched /VerifierData/patched.exe \
              --proof-summary-json /VerifierData/report.json \

docs/user-manual/build.tex

@@ -19,7 +19,7 @@ \subsection{Recommended: Docker Container Image}
   git clone [email protected]:GaloisInc/pate.git
   cd pate
   git submodule update --init
-  docker build . -t pate
+  docker build --platform linux/amd64 . -t pate
 \end{verbatim}
 
 \pate{} may subsequently be used via Docker, such as:

pate.cabal

@@ -112,6 +112,7 @@ library
                        Pate.Verification.DemandDiscovery,
                        Pate.Verification.Domain,
                        Pate.Verification.ExternalCall,
+                       Pate.Verification.FnBindings,
                        Pate.Verification.InlineCallee,
                        Pate.Verification.MemoryLog,
                        Pate.Verification.Override,

src/Data/Parameterized/SetF.hs

@@ -47,12 +47,14 @@ module Data.Parameterized.SetF
   , fromSet
   , map
   , ppSetF
+  , asSet
   ) where
 
 import Prelude hiding (filter, null, map)
 import qualified Data.List as List
 import           Data.Parameterized.Classes
 import qualified Data.Foldable as Foldable
+import qualified Control.Lens as L
 
 import qualified Prettyprinter as PP
 import           Prettyprinter ( (<+>) )
@@ -150,6 +152,11 @@ toSet (SetF s) = unsafeCoerce s
 fromSet :: (OrdF f, Ord (f tp)) => Set (f tp) -> SetF f tp
 fromSet s = SetF (unsafeCoerce s)
 
+asSet ::
+  (OrdF f, Ord (f tp)) =>
+  L.Lens' (SetF f tp) (Set (f tp))
+asSet f sf = fmap fromSet (f (toSet sf))
+
 map ::
   (OrdF g) => (f tp -> g tp) -> SetF f tp -> SetF g tp
 map f (SetF s) = SetF (S.map (\(AsOrd v) -> AsOrd (f v)) s)  

src/Pate/AssumptionSet.hs

@@ -138,6 +138,11 @@ instance OrdF (W4.SymExpr sym) => PEM.ExprMappable sym (AssumptionSet sym) where
         return $ MapF.singleton k' v'
     return $ mkAssumptionSet sym ps' (foldr (mergeExprSetFMap (Proxy @sym)) MapF.empty bs')
 
+instance PEM.ExprFoldable sym (AssumptionSet sym) where
+  foldExpr sym f (AssumptionSet ps bs) acc =
+    PEM.withSymExprFoldable @W4.BaseBoolType sym $
+      PEM.foldExpr sym f ps acc >>= PEM.foldExpr sym f bs
+
 instance forall sym. W4S.SerializableExprs sym => W4S.W4Serializable sym (AssumptionSet sym) where
   w4Serialize (AssumptionSet ps bs) | SetF.null ps, MapF.null bs = W4S.w4Serialize True
   w4Serialize (AssumptionSet ps bs) | [p] <- SetF.toList ps, MapF.null bs = W4S.w4SerializeF p
@@ -166,6 +171,11 @@ data NamedAsms sym (nm :: Symbol) =
 instance W4S.SerializableExprs sym => W4S.W4Serializable sym (NamedAsms sym nm) where
   w4Serialize (NamedAsms asm) = W4S.w4Serialize asm
 
+instance PEM.ExprFoldable sym (NamedAsms sym nm) where
+  foldExpr sym f (NamedAsms asm) acc = PEM.foldExpr sym f asm acc
+
+instance PEM.ExprFoldableF sym (NamedAsms sym)
+
 instance PEM.ExprMappable sym (NamedAsms sym nm) where
   mapExpr sym f (NamedAsms asm) = NamedAsms <$> PEM.mapExpr sym f asm
 

src/Pate/Discovery/ParsedFunctions.hs

@@ -78,8 +78,62 @@ import Data.List (isPrefixOf)
 
 data ParsedBlocks arch = forall ids. ParsedBlocks [MD.ParsedBlock arch ids]
 
+data CachedFunInfo arch (bin :: PBi.WhichBinary) = CachedFunInfo
+  { 
+    cachedDfi :: Some (MD.DiscoveryFunInfo arch)
+  -- we take a snapshot of any state that affects macaw's code discovery so
+  -- we can check if the cached result is still valid on a hit
+  , cachedOverride :: Maybe (PB.AbsStateOverride arch)
+  -- FIXME: technically we can scope these to the current function body, but
+  -- these are added infrequently enough that it's probably not worth it
+  , cachedExtraJumps :: ExtraJumps arch
+  , cachedExtraTargets :: Set.Set (MM.ArchSegmentOff arch)
+  }
+
+cachedFunInfo ::
+  forall arch bin ids.
+  ParsedFunctionMap arch bin ->
+  ParsedFunctionState arch bin -> 
+  MD.DiscoveryFunInfo arch ids -> 
+  CachedFunInfo arch bin
+cachedFunInfo pfm st dfi = CachedFunInfo (Some dfi) (Map.lookup addr (absStateOverrides pfm)) (extraEdges st) (extraTargets st)
+  where
+    addr :: MM.ArchSegmentOff arch
+    addr = MD.discoveredFunAddr dfi
+
+-- | Add a function entry to the cache, taking a snapshot of any relevant
+--  state so we can validate the cached entry on retrieval
+addFunctionEntry ::
+  ParsedFunctionMap arch bin ->
+  PB.FunctionEntry arch bin ->
+  MD.DiscoveryFunInfo arch ids ->
+  ParsedFunctionState arch bin ->
+  ParsedFunctionState arch bin
+addFunctionEntry pfm fe dfi st = st { parsedFunctionCache = Map.insert fe (cachedFunInfo pfm st dfi) (parsedFunctionCache st ) }
+
+
+-- | Fetch a cached discovery result for a function entry. Returns 'Nothing' if any relevant state in either the 'ParsedFunctionMap'
+--   or the 'ParsedFunctionState' has changed since the entry was computed (i.e. the cached entry is potentially invalid and
+--   needs to be re-computed).
+lookupFunctionEntry ::
+  MM.ArchConstraints arch =>
+  ParsedFunctionMap arch bin ->
+  ParsedFunctionState arch bin ->
+  PB.FunctionEntry arch bin ->
+  Maybe (Some (MD.DiscoveryFunInfo arch))
+lookupFunctionEntry pfm st fe = case Map.lookup fe (parsedFunctionCache st) of
+  Just cachedInfo | 
+      Some dfi <- cachedDfi cachedInfo
+    , mov <- Map.lookup (MD.discoveredFunAddr dfi) (absStateOverrides pfm)
+    , mov == cachedOverride cachedInfo
+    , extraEdges st == cachedExtraJumps cachedInfo
+    , extraTargets st == cachedExtraTargets cachedInfo
+    -> Just (Some dfi)
+  _ -> Nothing
+
+
 data ParsedFunctionState arch bin =
-  ParsedFunctionState { parsedFunctionCache :: Map.Map (PB.FunctionEntry arch bin) (Some (MD.DiscoveryFunInfo arch))
+  ParsedFunctionState { parsedFunctionCache :: Map.Map (PB.FunctionEntry arch bin) (CachedFunInfo arch bin)
                       , discoveryState :: MD.DiscoveryState arch
                       , extraTargets :: Set.Set (MM.ArchSegmentOff arch)
                       , extraEdges :: ExtraJumps arch
@@ -132,7 +186,6 @@ addExtraTarget pfm tgt = do
     False -> do
       IORef.modifyIORef' (parsedStateRef pfm) $ \st' -> 
         st' { extraTargets = Set.insert tgt (extraTargets st')}
-      flushCache pfm
 
 getExtraTargets ::
   ParsedFunctionMap arch bin ->
@@ -141,16 +194,6 @@ getExtraTargets pfm = do
   st <- IORef.readIORef (parsedStateRef pfm)
   return $ extraTargets st
 
-flushCache ::
-  MM.ArchConstraints arch =>
-  ParsedFunctionMap arch bin ->
-  IO ()
-flushCache pfm = do
-  st <- IORef.readIORef (parsedStateRef pfm)
-  let ainfo = MD.archInfo (discoveryState st)
-  IORef.modifyIORef' (parsedStateRef pfm) $ \st' -> 
-    st' { parsedFunctionCache = mempty, discoveryState = initDiscoveryState pfm ainfo }
-
 isUnsupportedErr :: T.Text -> Bool
 isUnsupportedErr err = 
      T.isPrefixOf "UnsupportedInstruction" err 
@@ -231,16 +274,12 @@ addExtraEdges ::
 addExtraEdges pfm es = do
   mapM_ addTgt (Map.elems es)
   IORef.modifyIORef' (parsedStateRef pfm) $ \st' -> 
-    st' { extraEdges = Map.merge Map.preserveMissing Map.preserveMissing (Map.zipWithMaybeMatched (\_ l r -> Just (l <> r))) es (extraEdges st')}
+    st' { extraEdges = Map.merge Map.preserveMissing Map.preserveMissing (Map.zipWithMaybeMatched (\_ l r -> Just (l <> r))) es (extraEdges st') }
   where
     addTgt :: ExtraJumpTarget arch -> IO ()
     addTgt = \case
       DirectTargets es' -> mapM_ (addExtraTarget pfm) (Set.toList es')
-      -- we need to flush the cache here to ensure that we re-check the block at the
-      -- call site(s) after adding this as a return
-      ReturnTarget -> flushCache pfm
-      -- a call shouldn't require special treatment since it won't introduce
-      -- any edges
+      ReturnTarget -> return ()
       DirectCall{} -> return ()
 
 -- | Apply the various overrides to the architecture definition before returning the discovery state
@@ -518,7 +557,7 @@ parsedFunctionContaining blk pfm@(ParsedFunctionMap pfmRef mCFGDir _pd _ _ _ _ _
   st <- getParsedFunctionState faddr pfm
 
   -- First, check if we have a cached set of blocks for this state
-  case Map.lookup (PB.blockFunctionEntry blk) (parsedFunctionCache st) of
+  case lookupFunctionEntry pfm st (PB.blockFunctionEntry blk) of
     Just sdfi -> return (Just sdfi)
     Nothing -> do
       -- Otherwise, run code discovery at this address
@@ -531,7 +570,10 @@ parsedFunctionContaining blk pfm@(ParsedFunctionMap pfmRef mCFGDir _pd _ _ _ _ _
       -- IORef that might be evaluated multiple times if there is a lot of
       -- contention. If that becomes a problem, we may want to change this
       -- to an MVar where we fully evaluate each result before updating it.
-      (_, Some dfi) <- atomicAnalysis faddr st
+      (st', Some dfi) <- atomicAnalysis faddr st
+      IORef.modifyIORef pfmRef $ \st_ -> 
+        st_ { parsedFunctionCache = parsedFunctionCache st' }
+
       --IORef.writeIORef pfmRef pfm'
       saveCFG mCFGDir (PB.blockBinRepr blk) dfi
       return (Just (Some dfi))
@@ -557,11 +599,10 @@ parsedFunctionContaining blk pfm@(ParsedFunctionMap pfmRef mCFGDir _pd _ _ _ _ _
         False -> do
           let rsn = MD.CallTarget faddr
           case incCompResult (MD.discoverFunction MD.defaultDiscoveryOptions faddr rsn (discoveryState st) []) of
-            (ds2, Some dfi) -> do
+            (_, Some dfi) -> do
                 entry <- resolveFunctionEntry (funInfoToFunEntry (PB.blockBinRepr blk) dfi pfm) pfm
-                return $ (st { parsedFunctionCache = Map.insert entry (Some dfi) (parsedFunctionCache st)
-                             , discoveryState = ds2
-                             }, Some dfi)
+                let st' = addFunctionEntry pfm entry dfi st
+                return $ (st', Some dfi)
     bin :: PBi.WhichBinaryRepr bin
     bin = PB.blockBinRepr blk
 

src/Pate/Equivalence/Condition.hs

@@ -148,6 +148,13 @@ instance PEM.ExprMappable sym (EquivalenceCondition sym arch v) where
     <*> PEM.mapExpr sym f c
     <*> PEM.mapExpr sym f d
 
+instance PEM.ExprFoldableF sym (MM.ArchReg arch) => PEM.ExprFoldable sym (EquivalenceCondition sym arch v) where
+  foldExpr sym f (EquivalenceCondition a b c d) acc =
+        PEM.foldExpr sym f a acc
+    >>= PEM.foldExpr sym f b
+    >>= PEM.foldExpr sym f c
+    >>= PEM.foldExpr sym f d
+
 instance PS.Scoped (EquivalenceCondition sym arch) where
   unsafeCoerceScope (EquivalenceCondition a b c d) = EquivalenceCondition a (PS.unsafeCoerceScope b) c d
 
@@ -234,6 +241,10 @@ instance PS.Scoped (RegisterCondition sym arch) where
 instance PEM.ExprMappable sym (RegisterCondition sym arch v) where
   mapExpr sym f (RegisterCondition cond) = RegisterCondition <$> MM.traverseRegsWith (\_ -> PEM.mapExpr sym f) cond
 
+instance PEM.ExprFoldableF sym (MM.ArchReg arch) => PEM.ExprFoldable sym (RegisterCondition sym arch v) where
+  foldExpr sym f (RegisterCondition cond) = PEM.foldExpr sym f (MM.regStateMap cond)
+
+
 trueRegCond ::
   W4.IsSymExprBuilder sym =>
   PA.ValidArch arch =>

src/Pate/Equivalence/Error.hs

@@ -172,6 +172,7 @@ data InnerEquivalenceError arch
   | forall e. X.Exception e => UnhandledException e
   | IncompatibleSingletonNodes (PB.ConcreteBlock arch PBi.Original) (PB.ConcreteBlock arch PBi.Patched)
   | SolverError X.SomeException
+  | ConcretizationFailure String
 
 errShortName :: MS.SymArchConstraints arch => InnerEquivalenceError arch -> String
 errShortName = \case