Merge pull request #1919 from GaloisInc/T1914

`SetupValue`: Use proper TTG-style extension fields
GaloisInc · Sep 1, 2023 · 62100c0 · 62100c0
2 parents d565fe6 + 5a47ded
commit 62100c0
Show file tree

Hide file tree

Showing 19 changed files with 1,080 additions and 568 deletions.
diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs
@@ -635,11 +635,11 @@ substMethodSpec sc sm ms = do
         MS.SetupVar _ -> return sv
         MS.SetupTerm tt -> MS.SetupTerm <$> goTypedTerm tt
         MS.SetupNull _ -> return sv
-        MS.SetupStruct b packed svs -> MS.SetupStruct b packed <$> mapM goSetupValue svs
+        MS.SetupStruct b svs -> MS.SetupStruct b <$> mapM goSetupValue svs
         MS.SetupArray b svs -> MS.SetupArray b <$> mapM goSetupValue svs
         MS.SetupElem b sv idx -> MS.SetupElem b <$> goSetupValue sv <*> pure idx
         MS.SetupField b sv name -> MS.SetupField b <$> goSetupValue sv <*> pure name
-        MS.SetupCast v _ _ -> case v of {}
+        MS.SetupCast v _ -> case v of {}
         MS.SetupUnion v _ _ -> case v of {}
         MS.SetupGlobal _ _ -> return sv
         MS.SetupGlobalInitializer _ _ -> return sv
@@ -677,14 +677,14 @@ regToSetup bak p eval shp rv = go shp rv
 
     go :: forall tp. TypeShape tp -> RegValue sym tp ->
         BuilderT sym t (OverrideSim p sym MIR rtp args ret) (MS.SetupValue MIR)
-    go (UnitShape _) () = return $ MS.SetupStruct () False []
+    go (UnitShape _) () = return $ MS.SetupStruct () []
     go (PrimShape _ btpr) expr = do
         -- Record all vars used in `expr`
         cache <- use msbVisitCache
         visitExprVars cache expr $ \var -> do
             msbPrePost p . seVars %= Set.insert (Some var)
         liftIO $ MS.SetupTerm <$> eval btpr expr
-    go (TupleShape _ _ flds) rvs = MS.SetupStruct () False <$> goFields flds rvs
+    go (TupleShape _ _ flds) rvs = MS.SetupStruct () <$> goFields flds rvs
     go (ArrayShape _ _ shp) vec = do
         svs <- case vec of
             MirVector_Vector v -> mapM (go shp) (toList v)
@@ -695,7 +695,7 @@ regToSetup bak p eval shp rv = go shp rv
         return $ MS.SetupArray () svs
     go (StructShape _ _ flds) (AnyValue tpr rvs)
       | Just Refl <- testEquality tpr shpTpr =
-        MS.SetupStruct () False <$> goFields flds rvs
+        MS.SetupStruct () <$> goFields flds rvs
       | otherwise = error $ "regToSetup: type error: expected " ++ show shpTpr ++
         ", but got Any wrapping " ++ show tpr
       where shpTpr = StructRepr $ fmapFC fieldShapeType flds

diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs
@@ -356,7 +356,7 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
   where
     go :: forall tp. TypeShape tp -> RegValue sym tp -> MS.SetupValue MIR ->
         MirOverrideMatcher sym ()
-    go (UnitShape _) () (MS.SetupStruct () False []) = return ()
+    go (UnitShape _) () (MS.SetupStruct () []) = return ()
     go (PrimShape _ _btpr) expr (MS.SetupTerm tt) = do
         loc <- use MS.osLocation
         exprTerm <- liftIO $ eval expr
@@ -390,14 +390,14 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
                         ("mismatch on " ++ show (W4.exprType expr) ++ ": expected " ++
                             show (W4.printSymExpr val))
                         ""
-    go (TupleShape _ _ flds) rvs (MS.SetupStruct () False svs) = goFields flds rvs svs
+    go (TupleShape _ _ flds) rvs (MS.SetupStruct () svs) = goFields flds rvs svs
     go (ArrayShape _ _ shp) vec (MS.SetupArray () svs) = case vec of
         MirVector_Vector v -> zipWithM_ (\x y -> go shp x y) (toList v) svs
         MirVector_PartialVector pv -> forM_ (zip (toList pv) svs) $ \(p, sv) -> do
             rv <- liftIO $ readMaybeType sym "vector element" (shapeType shp) p
             go shp rv sv
         MirVector_Array _ -> error $ "matchArg: MirVector_Array NYI"
-    go (StructShape _ _ flds) (AnyValue tpr rvs) (MS.SetupStruct () False svs)
+    go (StructShape _ _ flds) (AnyValue tpr rvs) (MS.SetupStruct () svs)
       | Just Refl <- testEquality tpr shpTpr = goFields flds rvs svs
       | otherwise = error $ "matchArg: type error: expected " ++ show shpTpr ++
         ", but got Any wrapping " ++ show tpr
@@ -510,7 +510,7 @@ setupToReg :: forall sym t st fs tp.
 setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
   where
     go :: forall tp. TypeShape tp -> MS.SetupValue MIR -> IO (RegValue sym tp)
-    go (UnitShape _) (MS.SetupStruct _ False []) = return ()
+    go (UnitShape _) (MS.SetupStruct _ []) = return ()
     go (PrimShape _ btpr) (MS.SetupTerm tt) = do
         term <- liftIO $ SAW.scInstantiateExt sc termSub $ SAW.ttTerm tt
         Some expr <- termToExpr sym sc regMap term
@@ -519,11 +519,11 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
             Nothing -> error $ "setupToReg: expected " ++ show btpr ++ ", but got " ++
                 show (W4.exprType expr)
         return expr
-    go (TupleShape _ _ flds) (MS.SetupStruct _ False svs) = goFields flds svs
+    go (TupleShape _ _ flds) (MS.SetupStruct _ svs) = goFields flds svs
     go (ArrayShape _ _ shp) (MS.SetupArray _ svs) = do
         rvs <- mapM (go shp) svs
         return $ MirVector_Vector $ V.fromList rvs
-    go (StructShape _ _ flds) (MS.SetupStruct _ False svs) =
+    go (StructShape _ _ flds) (MS.SetupStruct _ svs) =
         AnyValue (StructRepr $ fmapFC fieldShapeType flds) <$> goFields flds svs
     go (TransparentShape _ shp) sv = go shp sv
     go (RefShape _ _ _ tpr) (MS.SetupVar alloc) = case Map.lookup alloc allocMap of

diff --git a/saw-script.cabal b/saw-script.cabal
@@ -146,13 +146,15 @@ library
     SAWScript.Crucible.Common.ResolveSetupValue
     SAWScript.Crucible.Common.Setup.Builtins
     SAWScript.Crucible.Common.Setup.Type
+    SAWScript.Crucible.Common.Setup.Value
 
     SAWScript.Crucible.LLVM.Builtins
     SAWScript.Crucible.LLVM.Boilerplate
     SAWScript.Crucible.LLVM.CrucibleLLVM
     SAWScript.Crucible.LLVM.Override
     SAWScript.Crucible.LLVM.MethodSpecIR
     SAWScript.Crucible.LLVM.ResolveSetupValue
+    SAWScript.Crucible.LLVM.Setup.Value
     SAWScript.Crucible.LLVM.Skeleton
     SAWScript.Crucible.LLVM.Skeleton.Builtins
     SAWScript.Crucible.LLVM.X86
@@ -162,11 +164,13 @@ library
     SAWScript.Crucible.JVM.MethodSpecIR
     SAWScript.Crucible.JVM.Override
     SAWScript.Crucible.JVM.ResolveSetupValue
+    SAWScript.Crucible.JVM.Setup.Value
 
     SAWScript.Crucible.MIR.Builtins
     SAWScript.Crucible.MIR.MethodSpecIR
     SAWScript.Crucible.MIR.Override
     SAWScript.Crucible.MIR.ResolveSetupValue
+    SAWScript.Crucible.MIR.Setup.Value
     SAWScript.Crucible.MIR.TypeShape
 
     SAWScript.Prover.Mode