wip

GaloisInc · Dec 20, 2022 · 5452f6d · 5452f6d
1 parent 9770e7a
commit 5452f6d
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 4 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/what4 b/deps/what4
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -1696,9 +1696,22 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val =
                                  instantiateExtMatchTerm sc cc md prepost arr_tm $ ttTerm expected_arr_tm
                                  return Nothing
 
-                            _ -> return $ Just errMsg
+                            Nothing
+                              | sz_nat == 0 ->
+                                do off_type_tm <- liftIO $ scBitvector sc $ natValue ?ptrWidth
+                                   byte_width_tm <- liftIO $ scNat sc 8
+                                   byte_type_tm <- liftIO $ scBitvector sc 8
 
-                     _ -> return $ Just errMsg
+                                   zero_byte_tm <- liftIO $ scBvNat sc byte_width_tm =<< scNat sc 0
+                                   zero_arr_const_tm <- liftIO $ scArrayConstant sc off_type_tm byte_type_tm zero_byte_tm
+
+                                   instantiateExtMatchTerm sc cc md prepost zero_arr_const_tm $ ttTerm expected_arr_tm
+
+                                   return Nothing
+
+                              | otherwise -> return $ Just errMsg
+
+                     Nothing -> return $ Just errMsg
 
 -- | Like 'matchPointsToValue', but specifically geared towards the needs
 -- of fields within bitfields. In particular, this performs all of the
+2 −4		.github/workflows/gen_matrix.pl
+8 −4		.github/workflows/test.yml
+5 −5		README.md
+4 −0		what4/CHANGES.md
+7 −1		what4/README.md
+2 −0		what4/src/What4/Expr/App.hs
+54 −13		what4/src/What4/Expr/Builder.hs
+88 −6		what4/src/What4/Interface.hs
+6 −0		what4/src/What4/ProblemFeatures.hs
+47 −0		what4/src/What4/Protocol/Online.hs
+6 −0		what4/src/What4/Protocol/SExp.hs
+452 −16		what4/src/What4/Protocol/SMTLib2.hs
+1 −1		what4/src/What4/Protocol/SMTLib2/Parse.hs
+5 −1		what4/src/What4/Protocol/SMTLib2/Response.hs
+46 −3		what4/src/What4/Protocol/SMTLib2/Syntax.hs
+110 −2		what4/src/What4/Protocol/SMTWriter.hs
+184 −0		what4/src/What4/Serialize/FastSExpr.hs
+436 −0		what4/src/What4/Serialize/Log.hs
+162 −0		what4/src/What4/Serialize/Normalize.hs
+1,070 −0		what4/src/What4/Serialize/Parser.hs
+779 −0		what4/src/What4/Serialize/Printer.hs
+259 −0		what4/src/What4/Serialize/SETokens.hs
+139 −0		what4/src/What4/Solver/CVC5.hs
+15 −0		what4/src/What4/Solver/Yices.hs
+94 −2		what4/src/What4/Solver/Z3.hs
+127 −0		what4/src/What4/Utils/Serialize.hs
+155 −0		what4/test/Abduct.hs
+58 −0		what4/test/ExprsTest.hs
+129 −0		what4/test/InvariantSynthesis.hs
+58 −0		what4/test/SerializeTestUtils.hs
+20 −0		what4/test/SerializeTests.hs
+242 −0		what4/test/SymFnTests.hs
+61 −0		what4/what4.cabal