Merge pull request #717 from GaloisInc/bh-bugfixes

Various bugfixes
GaloisInc · May 19, 2020 · eeef9a1 · eeef9a1
2 parents f991bb4 + 1d20150
commit eeef9a1
Show file tree

Hide file tree

Showing 7 changed files with 779 additions and 701 deletions.
diff --git a/src/SAWScript/Crucible/Common/Override.hs b/src/SAWScript/Crucible/Common/Override.hs
@@ -180,10 +180,10 @@ ppOverrideFailureReason ::
   ) => OverrideFailureReason ext -> PP.Doc
 ppOverrideFailureReason rsn = case rsn of
   AmbiguousPointsTos pts ->
-    PP.text "ambiguous collection of points-to assertions" PP.<$$>
+    PP.text "LHS of points-to assertion(s) not reachable via points-tos from inputs/outputs:" PP.<$$>
     (PP.indent 2 $ PP.vcat (map PP.pretty pts))
   AmbiguousVars vs ->
-    PP.text "ambiguous collection of variables" PP.<$$>
+    PP.text "Fresh variable(s) not reachable via points-tos from function inputs/outputs:" PP.<$$>
     (PP.indent 2 $ PP.vcat (map MS.ppTypedTerm vs))
   BadTermMatch x y ->
     PP.text "terms do not match" PP.<$$>

diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -995,6 +995,13 @@ matchArg opts sc cc cs prepost actual expectedTy expected = do
               realTerm <- valueToSC sym (cs ^. MS.csLoc) failMsg tval actual
               matchTerm sc cc (cs ^. MS.csLoc) prepost realTerm (ttTerm expectedTT)
 
+    -- match arrays point-wise
+    (Crucible.LLVMValArray _ xs, Crucible.ArrayType _len y, SetupArray () zs)
+      | V.length xs >= length zs ->
+        sequence_
+          [ matchArg opts sc cc cs prepost x y z
+          | (x, z) <- zip (V.toList xs) zs ]
+
     -- match the fields of struct point-wise
     (Crucible.LLVMValStruct xs, Crucible.StructType fields, SetupStruct () _ zs) ->
       sequence_

diff --git a/src/SAWScript/MGU.hs b/src/SAWScript/MGU.hs
@@ -625,7 +625,7 @@ inferRecDecls ds =
                  $ sequence [ withExprPos pos $ inferE (patternLName p, e)
                             | Decl pos p _ e <- ds
                             ]
-     sequence_ $ zipWith (constrainTypeWithPattern (error "FIXME")) ts pats'
+     sequence_ $ zipWith (constrainTypeWithPattern (patternLName (head pats))) ts pats'
      ess <- generalize es ts
      return [ Decl pos p (Just s) e1
             | (pos, p, (e1, s)) <- zip3 (map getPos ds) pats ess

diff --git a/stack.ghc-8.4.yaml b/stack.ghc-8.4.yaml
@@ -57,5 +57,7 @@ extra-deps:
   - yaml-0.11.2.0
   - libyaml-0.1.2
   - aeson-1.4.3.0
+  - QuickCheck-2.14
+  - splitmix-0.0.4
 resolver: lts-12.26
 allow-newer: false
diff --git a/stack.ghc-8.6.yaml b/stack.ghc-8.6.yaml
@@ -53,5 +53,7 @@ extra-deps:
   - config-value-0.6.3.1
   - simple-get-opt-0.3
   - base-orphans-0.8.2
+  - QuickCheck-2.14
+  - splitmix-0.0.4
 resolver: lts-14.3
 allow-newer: false
diff --git a/stack.ghc-8.8.yaml b/stack.ghc-8.8.yaml
@@ -46,5 +46,7 @@ extra-deps:
   - base-orphans-0.8.2
   - base-compat-0.10.5
   - json-0.10
+  - QuickCheck-2.14
+  - splitmix-0.0.4
 resolver: lts-15.1
 allow-newer: false