From 04e3fb66ea206377423a8f9c2b47261ce0630fc2 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 10 Aug 2023 17:54:18 +0000 Subject: [PATCH] Treat terms that could not be reduced to concrete values as non-ground term instead of throwing an error during setup phase. This fixes the problem that `primitive` values cause failure in concrete evaluation. --- src/SAWScript/Crucible/JVM/ResolveSetupValue.hs | 17 +++++++++++------ .../Crucible/LLVM/ResolveSetupValue.hs | 17 +++++++++++------ 2 files changed, 22 insertions(+), 12 deletions(-) diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs index 253269eda4..e6bfad19bc 100644 --- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs @@ -30,6 +30,7 @@ module SAWScript.Crucible.JVM.ResolveSetupValue import Control.Lens import qualified Control.Monad.Catch as X +import Control.Exception (catch) import qualified Data.BitVector.Sized as BV import Data.Map (Map) import qualified Data.Map as Map @@ -265,9 +266,11 @@ resolveBitvectorTerm sym w tm = mx <- case getAllExts tm of -- concretely evaluate if it is a closed term [] -> - do modmap <- scGetModuleMap sc - let v = Concrete.evalSharedTerm modmap mempty mempty tm - pure (Just (Prim.unsigned (Concrete.toWord v))) + catch (do modmap <- scGetModuleMap sc + let v = Concrete.evalSharedTerm modmap mempty mempty tm + seq v (pure (Just (Prim.unsigned (Concrete.toWord v))))) + -- return Nothing if concrete evaluation results in an error + (\(_ :: Prim.EvalError) -> return Nothing) _ -> return Nothing case mx of Just x -> W4.bvLit sym w (BV.mkBV w x) @@ -280,9 +283,11 @@ resolveBoolTerm sym tm = mx <- case getAllExts tm of -- concretely evaluate if it is a closed term [] -> - do modmap <- scGetModuleMap sc - let v = Concrete.evalSharedTerm modmap mempty mempty tm - pure (Just (Concrete.toBool v)) + catch (do modmap <- scGetModuleMap sc + let v = Concrete.evalSharedTerm modmap mempty mempty tm + seq v (pure (Just (Concrete.toBool v)))) + -- return Nothing if concrete evaluation results in an error + (\(_ :: Prim.EvalError) -> return Nothing) _ -> return Nothing case mx of Just x -> return (W4.backendPred sym x) diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index 9223c5b909..367faf79ca 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -39,6 +39,7 @@ import Control.Lens ( (^.), view ) import Control.Monad import Control.Monad.Except import Control.Monad.State +import Control.Exception (catch) import qualified Data.BitVector.Sized as BV import Data.Maybe (fromMaybe, fromJust) @@ -734,9 +735,11 @@ resolveSAWPred cc tm = do (_,tm') <- rewriteSharedTerm sc ss tm mx <- case getAllExts tm' of -- concretely evaluate if it is a closed term - [] -> do modmap <- scGetModuleMap sc - let v = Concrete.evalSharedTerm modmap mempty mempty tm - pure (Just (Concrete.toBool v)) + [] -> catch (do modmap <- scGetModuleMap sc + let v = Concrete.evalSharedTerm modmap mempty mempty tm + seq v (pure (Just (Concrete.toBool v)))) + -- return Nothing if concrete evaluation results in an error + (\(_ :: Prim.EvalError) -> return Nothing) _ -> return Nothing case mx of Just x -> return $ W4.backendPred sym x @@ -764,9 +767,11 @@ resolveSAWSymBV cc w tm = let sc = saw_ctx st mx <- case getAllExts tm of -- concretely evaluate if it is a closed term - [] -> do modmap <- scGetModuleMap sc - let v = Concrete.evalSharedTerm modmap mempty mempty tm - pure (Just (Prim.unsigned (Concrete.toWord v))) + [] -> catch (do modmap <- scGetModuleMap sc + let v = Concrete.evalSharedTerm modmap mempty mempty tm + seq v (pure (Just (Prim.unsigned (Concrete.toWord v))))) + -- return Nothing if concrete evaluation results in an error + (\(_ :: Prim.EvalError) -> return Nothing) _ -> return Nothing case mx of Just x -> W4.bvLit sym w (BV.mkBV w x)