From 147209be192ae3f4dbd7db0ffc4909eeea034e06 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 16 Feb 2022 16:22:01 -0800 Subject: [PATCH 1/2] Make `goal_eval_unint` handle functions with arguments of type `Nat`. We can now make functions like `take` and `drop` uninterpreted. Fixes #1588. --- saw-core-what4/src/Verifier/SAW/Simulator/What4.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index 232d685758..d23043c761 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -1519,6 +1519,10 @@ mkArgTerm sc ty val = do x <- termOfTValue sc tval pure (ArgTermConst x) + (_, VNat n) -> + do x <- scNat sc n + pure (ArgTermConst x) + _ -> fail $ "could not create uninterpreted function argument of type " ++ show ty termOfTValue :: SharedContext -> TValue (What4 sym) -> IO Term From 60e5a48930041eeda472dc8d35748e36529bf801 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 16 Feb 2022 18:10:10 -0800 Subject: [PATCH 2/2] Support `bvToNat` in uninterpreted functions. This lets `goal_eval_unint` and `w4_unint` work with functions like `at`. Fixes #1591. --- saw-core-what4/src/Verifier/SAW/Simulator/What4.hs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index d23043c761..f106645b9e 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -961,6 +961,8 @@ applyUnintApp sym app0 v = VCtorApp i ps xv -> foldM (applyUnintApp sym) app' =<< traverse force (ps++xv) where app' = suffixUnintApp ("_" ++ (Text.unpack (identBaseName (primName i)))) app0 VNat n -> return (suffixUnintApp ("_" ++ show n) app0) + VBVToNat w v' -> applyUnintApp sym app' v' + where app' = suffixUnintApp ("_" ++ show w) app0 TValue (suffixTValue -> Just s) -> return (suffixUnintApp s app0) VFun _ _ -> @@ -1399,6 +1401,7 @@ data ArgTerm -- ^ length, element type, list, index | ArgTermPairLeft ArgTerm | ArgTermPairRight ArgTerm + | ArgTermBVToNat Natural ArgTerm -- | Reassemble a saw-core term from an 'ArgTerm' and a list of parts. -- The length of the list should be equal to the number of @@ -1468,6 +1471,10 @@ reconstructArgTerm atrm sc ts = do (x1, ts1) <- parse at1 ts0 x <- scPairRight sc x1 return (x, ts1) + ArgTermBVToNat w at1 -> + do (x1, ts1) <- parse at1 ts0 + x <- scBvToNat sc w x1 + pure (x, ts1) parseList :: [ArgTerm] -> [Term] -> IO ([Term], [Term]) parseList [] ts0 = return ([], ts0) @@ -1523,6 +1530,11 @@ mkArgTerm sc ty val = do x <- scNat sc n pure (ArgTermConst x) + (_, VBVToNat w v) -> + do let w' = fromIntegral w -- FIXME: make w :: Natural to avoid fromIntegral + x <- mkArgTerm sc (VVecType w' VBoolType) v + pure (ArgTermBVToNat w' x) + _ -> fail $ "could not create uninterpreted function argument of type " ++ show ty termOfTValue :: SharedContext -> TValue (What4 sym) -> IO Term