diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 9b67b98f3e..c9af375cbb 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -3138,7 +3138,7 @@ thought of as additional global state that is visible only to the verifier. Ghost state with a given name can be declared at the top level with the following function: -* `llvm_declare_ghost_state : String -> TopLevel Ghost` +* `declare_ghost_state : String -> TopLevel Ghost` Ghost state variables do not initially have any particluar type, and can store data of any type. Given an existing ghost variable the following diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index 73891254fb..cea4608664 100644 Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ diff --git a/examples/ghost/ghost.saw b/examples/ghost/ghost.saw index 3e1dba3071..685ed46c45 100644 --- a/examples/ghost/ghost.saw +++ b/examples/ghost/ghost.saw @@ -16,7 +16,7 @@ let example_spec counter : CrucibleSetup () = do { }; let main : TopLevel () = do { - counter <- llvm_declare_ghost_state "ctr"; + counter <- declare_ghost_state "ctr"; m <- llvm_load_module "simple.bc"; next <- llvm_unsafe_assume_spec m "next" (next_spec counter); diff --git a/intTests/test_ghost/test.saw b/intTests/test_ghost/test.saw index 24b38a02dd..951a09423d 100644 --- a/intTests/test_ghost/test.saw +++ b/intTests/test_ghost/test.saw @@ -26,7 +26,7 @@ let f_spec (counter : Ghost) : CrucibleSetup () = do { }; let main : TopLevel () = do { - counter <- llvm_declare_ghost_state "counter"; + counter <- declare_ghost_state "counter"; m <- llvm_load_module "test.bc"; get_and_increment_ov <- llvm_unsafe_assume_spec m "get_and_increment" (get_and_increment_spec counter); diff --git a/intTests/test_ghost_branch_00/test.saw b/intTests/test_ghost_branch_00/test.saw index 78d1b77983..3fa4841445 100644 --- a/intTests/test_ghost_branch_00/test.saw +++ b/intTests/test_ghost_branch_00/test.saw @@ -25,7 +25,7 @@ let g_spec : CrucibleSetup () = do { }; let main : TopLevel () = do { - x <- llvm_declare_ghost_state "x"; + x <- declare_ghost_state "x"; m <- llvm_load_module "test.bc"; f_lt_ov <- llvm_unsafe_assume_spec m "f" (f_lt_spec x); f_ge_ov <- llvm_unsafe_assume_spec m "f" (f_ge_spec x); diff --git a/intTests/test_ghost_branch_01/test.saw b/intTests/test_ghost_branch_01/test.saw index 6d41b68b25..87b13e5ec1 100644 --- a/intTests/test_ghost_branch_01/test.saw +++ b/intTests/test_ghost_branch_01/test.saw @@ -28,7 +28,7 @@ let h_spec : CrucibleSetup () = do { }; let main : TopLevel () = do { - x <- llvm_declare_ghost_state "x"; + x <- declare_ghost_state "x"; m <- llvm_load_module "test.bc"; get_ov <- llvm_unsafe_assume_spec m "get" (get_spec x); f_ov <- llvm_unsafe_assume_spec m "f" (f_spec x); diff --git a/intTests/test_ghost_branch_02/test.saw b/intTests/test_ghost_branch_02/test.saw index 55f5eb8047..3efffb984d 100644 --- a/intTests/test_ghost_branch_02/test.saw +++ b/intTests/test_ghost_branch_02/test.saw @@ -21,7 +21,7 @@ let g_spec : CrucibleSetup () = do { }; let main : TopLevel () = do { - x <- llvm_declare_ghost_state "x"; + x <- declare_ghost_state "x"; m <- llvm_load_module "test.bc"; f_lt_ov <- llvm_unsafe_assume_spec m "f" (f_lt_spec x); f_ge_ov <- llvm_unsafe_assume_spec m "f" (f_ge_spec x); diff --git a/intTests/test_ghost_branch_03/test.saw b/intTests/test_ghost_branch_03/test.saw index 30f7373e5f..3f6bfd5393 100644 --- a/intTests/test_ghost_branch_03/test.saw +++ b/intTests/test_ghost_branch_03/test.saw @@ -28,7 +28,7 @@ let h_spec : CrucibleSetup () = do { }; let main : TopLevel () = do { - x <- llvm_declare_ghost_state "x"; + x <- declare_ghost_state "x"; m <- llvm_load_module "test.bc"; get_ov <- llvm_unsafe_assume_spec m "get" (get_spec x); f_ov <- llvm_unsafe_assume_spec m "f" (f_spec x); diff --git a/intTests/test_ghost_types_00/test.saw b/intTests/test_ghost_types_00/test.saw index f88faaef10..fc61fe0a86 100644 --- a/intTests/test_ghost_types_00/test.saw +++ b/intTests/test_ghost_types_00/test.saw @@ -23,7 +23,7 @@ let h_spec : CrucibleSetup () = do { }; let main : TopLevel () = do { - x <- llvm_declare_ghost_state "x"; + x <- declare_ghost_state "x"; m <- llvm_load_module "test.bc"; f_ov <- llvm_unsafe_assume_spec m "f" (f_spec x); // This spec should probably use a different variable, but doesn't: diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 279c3acddd..ed3e3d92ff 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -39,6 +39,7 @@ import Data.IORef import Data.List (isPrefixOf, isInfixOf, sort) import qualified Data.Map as Map import Data.Maybe (fromMaybe) +import Data.Parameterized.Classes (KnownRepr(..)) import Data.Set (Set) import qualified Data.Set as Set import Data.Text (Text) @@ -115,6 +116,9 @@ import qualified Cryptol.Utils.Ident as C (mkIdent, packModName, textToModName, PrimIdent(..)) import qualified Cryptol.Utils.RecordMap as C (recordFromFields) +-- crucible +import Lang.Crucible.CFG.Common (freshGlobalVar) + import qualified SAWScript.SBVParser as SBV import SAWScript.ImportAIG @@ -471,7 +475,7 @@ print_goal_inline noInline = execTactic $ tacticId $ \goal -> do opts <- getTopLevelPPOpts - let opts' = opts { ppNoInlineMemo = sort noInline } + let opts' = opts { ppNoInlineMemo = sort noInline } sc <- getSharedContext nenv <- io (scGetNamingEnv sc) let output = prettySequent opts' nenv (goalSequent goal) @@ -2462,3 +2466,11 @@ writeVerificationSummary = do JSON -> jsonVerificationSummary Pretty -> prettyVerificationSummary ppOpts nenv in io $ writeFile f' $ formatSummary summary + +declare_ghost_state :: + String -> + TopLevel SV.Value +declare_ghost_state name = + do allocator <- getHandleAlloc + global <- liftIO (freshGlobalVar allocator (Text.pack name) knownRepr) + return (SV.VGhostVar global) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index f70e250bc4..0977cb7570 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -43,7 +43,6 @@ module SAWScript.Crucible.LLVM.Builtins , llvm_spec_size , llvm_spec_solvers , llvm_ghost_value - , llvm_declare_ghost_state , llvm_equal , llvm_points_to , llvm_conditional_points_to @@ -2791,14 +2790,6 @@ llvm_equal (getAllLLVM -> val1) (getAllLLVM -> val2) = } Setup.addCondition (MS.SetupCond_Equal md val1 val2) -llvm_declare_ghost_state :: - String -> - TopLevel Value -llvm_declare_ghost_state name = - do allocator <- getHandleAlloc - global <- liftIO (Crucible.freshGlobalVar allocator (Text.pack name) knownRepr) - return (VGhostVar global) - llvm_ghost_value :: MS.GhostGlobal -> TypedTerm -> diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index bc28517c76..7360ca5f39 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3598,16 +3598,21 @@ primitives = Map.fromList ] -- Ghost state support - , prim "llvm_declare_ghost_state" + , prim "declare_ghost_state" "String -> TopLevel Ghost" - (pureVal llvm_declare_ghost_state) + (pureVal declare_ghost_state) Current [ "Allocates a unique ghost variable." ] + , prim "llvm_declare_ghost_state" + "String -> TopLevel Ghost" + (pureVal declare_ghost_state) + Deprecated + [ "Legacy alternative name for `declare_ghost_state`." ] , prim "crucible_declare_ghost_state" "String -> TopLevel Ghost" - (pureVal llvm_declare_ghost_state) - Current - [ "Legacy alternative name for `llvm_declare_ghost_state`." ] + (pureVal declare_ghost_state) + Deprecated + [ "Legacy alternative name for `declare_ghost_state`." ] , prim "llvm_ghost_value" "Ghost -> Term -> LLVMSetup ()"