Add declare_ghost_state, deprecate llvm_declare_ghost_state

We want to be able to declare ghost state in all SAW language backends, so we
now use a more general `declare_ghost_state` name for the command to reflect
this. The old `llvm_declare_ghost_state` command is now deprecated in favor of
`declare_ghost_state`.

This is one part of an eventual fix for #1929.

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

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);

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);

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);

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);

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);

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);

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:

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)

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 ->

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 ()"