Merge pull request #519 from siddharthist/tosv-array-length-msg

Allow pointers to one past the end of allocations
GaloisInc · Aug 5, 2019 · 206f6e1 · 206f6e1
2 parents 78625e2 + 828e04f
commit 206f6e1
Show file tree

Hide file tree

Showing 3 changed files with 70 additions and 61 deletions.
diff --git a/src/SAWScript/Crucible/Common/Override.hs b/src/SAWScript/Crucible/Common/Override.hs
@@ -151,7 +151,7 @@ data OverrideFailureReason ext
   | BadReturnSpecification (Some Crucible.TypeRepr)
     -- ^ type mismatch in return specification
   | NonlinearPatternNotSupported
-  | BadEqualityComparison String -- ^ Comparison on an undef value
+  | BadEqualityComparison -- ^ Comparison on an undef value
   | BadPointerLoad (Either (MS.PointsTo ext) PP.Doc) PP.Doc
     -- ^ @loadRaw@ failed due to type error
   | StructuralMismatch PP.Doc PP.Doc (Maybe (ExtType ext)) (ExtType ext)
@@ -194,9 +194,8 @@ ppOverrideFailureReason rsn = case rsn of
     ]
   NonlinearPatternNotSupported ->
     PP.text "nonlinear pattern not supported"
-  BadEqualityComparison globName ->
-    PP.text "global initializer containing `undef` compared for equality:" PP.<$$>
-    (PP.indent 2 (PP.text globName))
+  BadEqualityComparison ->
+    PP.text "value containing `undef` compared for equality"
   BadPointerLoad pointsTo msg ->
     PP.text "error when loading through pointer that" PP.<+>
     PP.text "appeared in the override's points-to precondition(s):" PP.<$$>

diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -850,61 +850,67 @@ matchArg ::
   SetupValue (Crucible.LLVM arch)         {- ^ expected specification value          -} ->
   OverrideMatcher (LLVM arch) md ()
 
-matchArg opts sc cc cs prepost actual expectedTy expected@(SetupTerm expectedTT)
-  | Cryptol.Forall [] [] tyexpr <- ttSchema expectedTT
-  , Right tval <- Cryptol.evalType mempty tyexpr
-  = do sym      <- Ov.getSymInterface
-       failMsg  <- mkStructuralMismatch opts cc sc cs actual expected expectedTy
-       realTerm <- valueToSC sym (cs ^. MS.csLoc) failMsg tval actual
-       matchTerm sc cc (cs ^. MS.csLoc) prepost realTerm (ttTerm expectedTT)
-
--- match the fields of struct point-wise
-matchArg opts sc cc cs prepost (Crucible.LLVMValStruct xs) (Crucible.StructType fields) (SetupStruct () _ zs) =
-  sequence_
-    [ matchArg opts sc cc cs prepost x y z
-       | ((_,x),y,z) <- zip3 (V.toList xs)
-                             (V.toList (Crucible.fiType <$> Crucible.siFields fields))
-                             zs ]
-
-matchArg opts sc cc cs prepost actual expectedTy g@(SetupGlobalInitializer () n) = do
-  (globInitTy, globInitVal) <- resolveSetupValueLLVM opts cc sc cs g
-  sym <- Ov.getSymInterface
-  if expectedTy /= globInitTy
-  then failure (cs ^. MS.csLoc) =<<
-         mkStructuralMismatch opts cc sc cs actual g expectedTy
-  else liftIO (Crucible.testEqual sym globInitVal actual) >>=
-    \case
-      Nothing -> failure (cs ^. MS.csLoc) (BadEqualityComparison n)
-      Just pred_ ->
-        addAssert pred_ =<<
-          notEqual prepost opts (cs ^. MS.csLoc) cc sc cs g actual
-
-matchArg opts sc cc cs prepost actual@(Crucible.LLVMValInt blk off) expectedTy setupval =
-  case setupval of
-    SetupVar var | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth ->
-      do assignVar cc (cs ^. MS.csLoc) var (Crucible.LLVMPointer blk off)
-
-    SetupNull () | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth ->
-      do sym <- Ov.getSymInterface
-         p   <- liftIO (Crucible.ptrIsNull sym Crucible.PtrWidth (Crucible.LLVMPointer blk off))
-         addAssert p =<<
-           notEqual prepost opts (cs ^. MS.csLoc) cc sc cs setupval actual
-
-    SetupGlobal () name | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth ->
-      do let mem = cc^.ccLLVMEmptyMem
-         sym  <- Ov.getSymInterface
-         ptr2 <- liftIO $ Crucible.doResolveGlobal sym mem (L.Symbol name)
-         pred_ <- liftIO $
-           Crucible.ptrEq sym Crucible.PtrWidth (Crucible.LLVMPointer blk off) ptr2
-         addAssert pred_ =<<
-           notEqual prepost opts (cs ^. MS.csLoc) cc sc cs setupval actual
+matchArg opts sc cc cs prepost actual expectedTy expected =
+  case (actual, expectedTy, expected) of
+    (_, _, SetupTerm expectedTT)
+      | Cryptol.Forall [] [] tyexpr <- ttSchema expectedTT
+      , Right tval <- Cryptol.evalType mempty tyexpr
+        -> do sym      <- Ov.getSymInterface
+              failMsg  <- mkStructuralMismatch opts cc sc cs actual expected expectedTy
+              realTerm <- valueToSC sym (cs ^. MS.csLoc) failMsg tval actual
+              matchTerm sc cc (cs ^. MS.csLoc) prepost realTerm (ttTerm expectedTT)
+
+    -- match the fields of struct point-wise
+    (Crucible.LLVMValStruct xs, Crucible.StructType fields, SetupStruct () _ zs) ->
+      sequence_
+        [ matchArg opts sc cc cs prepost x y z
+        | ((_,x),y,z) <- zip3 (V.toList xs)
+                              (V.toList (Crucible.fiType <$> Crucible.siFields fields))
+                              zs ]
+
+    (_, Crucible.PtrType _, SetupElem () _ _) -> resolveAndMatch
+    (_, Crucible.PtrType _, SetupField () _ _) -> resolveAndMatch
+    (_, _, SetupGlobalInitializer () _) -> resolveAndMatch
+
+    (Crucible.LLVMValInt blk off, _, _) ->
+      case expected of
+        SetupVar var | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth ->
+          do assignVar cc (cs ^. MS.csLoc) var (Crucible.LLVMPointer blk off)
+
+        SetupNull () | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth ->
+          do sym <- Ov.getSymInterface
+             p   <- liftIO (Crucible.ptrIsNull sym Crucible.PtrWidth (Crucible.LLVMPointer blk off))
+             addAssert p =<<
+               notEqual prepost opts (cs ^. MS.csLoc) cc sc cs expected actual
+
+        SetupGlobal () name | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth ->
+          do let mem = cc^.ccLLVMEmptyMem
+             sym  <- Ov.getSymInterface
+             ptr2 <- liftIO $ Crucible.doResolveGlobal sym mem (L.Symbol name)
+             pred_ <- liftIO $
+               Crucible.ptrEq sym Crucible.PtrWidth (Crucible.LLVMPointer blk off) ptr2
+             addAssert pred_ =<<
+               notEqual prepost opts (cs ^. MS.csLoc) cc sc cs expected actual
+
+        _ -> failure (cs ^. MS.csLoc) =<<
+              mkStructuralMismatch opts cc sc cs actual expected expectedTy
 
     _ -> failure (cs ^. MS.csLoc) =<<
-           mkStructuralMismatch opts cc sc cs actual setupval expectedTy
+           mkStructuralMismatch opts cc sc cs actual expected expectedTy
 
-matchArg opts sc cc cs _prepost actual expectedTy expected = do
-  failure (cs ^. MS.csLoc) =<<
-    mkStructuralMismatch opts cc sc cs actual expected expectedTy
+  where
+    resolveAndMatch = do
+      (ty, val) <- resolveSetupValueLLVM opts cc sc cs expected
+      sym  <- Ov.getSymInterface
+      if expectedTy /= ty
+      then failure (cs ^. MS.csLoc) =<<
+            mkStructuralMismatch opts cc sc cs actual expected expectedTy
+      else liftIO (Crucible.testEqual sym val actual) >>=
+        \case
+          Nothing -> failure (cs ^. MS.csLoc) BadEqualityComparison
+          Just pred_ ->
+            addAssert pred_ =<<
+              notEqual prepost opts (cs ^. MS.csLoc) cc sc cs expected actual
 
 ------------------------------------------------------------------------
 

diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -199,15 +199,19 @@ typeOfSetupValue' cc env nameEnv val =
       typeOfSetupValue' cc env nameEnv (SetupElem () v i)
     SetupElem () v i ->
       do memTy <- typeOfSetupValue cc env nameEnv v
-         let msg = "typeOfSetupValue: crucible_elem requires pointer to struct or array"
+         let msg = "typeOfSetupValue: crucible_elem requires pointer to struct or array, found " ++ show memTy
          case memTy of
            Crucible.PtrType symTy ->
              case let ?lc = lc in Crucible.asMemType symTy of
                Right memTy' ->
                  case memTy' of
                    Crucible.ArrayType n memTy''
-                     | fromIntegral i < n -> return (Crucible.PtrType (Crucible.MemType memTy''))
-                     | otherwise -> fail $ "typeOfSetupValue: array type index out of bounds: " ++ show (i, n)
+                     | fromIntegral i <= n -> return (Crucible.PtrType (Crucible.MemType memTy''))
+                     | otherwise -> fail $ unwords $
+                         [ "typeOfSetupValue: array type index out of bounds"
+                         , "(index: " ++ show i ++ ")"
+                         , "(array length: " ++ show n ++ ")"
+                         ]
                    Crucible.StructType si ->
                      case Crucible.siFieldInfo si i of
                        Just fi -> return (Crucible.PtrType (Crucible.MemType (Crucible.fiType fi)))
@@ -284,14 +288,14 @@ resolveSetupVal cc env tyenv nameEnv val =
       resolveSetupVal cc env tyenv nameEnv (SetupElem () v i)
     SetupElem () v i ->
       do memTy <- typeOfSetupValue cc tyenv nameEnv v
-         let msg = "resolveSetupVal: crucible_elem requires pointer to struct or array"
+         let msg = "resolveSetupVal: crucible_elem requires pointer to struct or array, found " ++ show memTy
          delta <- case memTy of
            Crucible.PtrType symTy ->
              case let ?lc = lc in Crucible.asMemType symTy of
                Right memTy' ->
                  case memTy' of
                    Crucible.ArrayType n memTy''
-                     | fromIntegral i < n -> return (fromIntegral i * Crucible.memTypeSize dl memTy'')
+                     | fromIntegral i <= n -> return (fromIntegral i * Crucible.memTypeSize dl memTy'')
                    Crucible.StructType si ->
                      case Crucible.siFieldOffset si i of
                        Just d -> return d