From edf735c15b76b3329293d14044ba4c64194a9918 Mon Sep 17 00:00:00 2001
From: Chris Phifer <cphifer@galois.com>
Date: Tue, 20 Apr 2021 16:49:53 -0500
Subject: [PATCH 1/3] Skeleton of and documentation for Rust type command

---
 src/SAWScript/HeapsterBuiltins.hs | 5 +++++
 src/SAWScript/Interpreter.hs      | 8 ++++++++
 2 files changed, 13 insertions(+)

diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs
index 6d4c744e92..e5931943bc 100644
--- a/src/SAWScript/HeapsterBuiltins.hs
+++ b/src/SAWScript/HeapsterBuiltins.hs
@@ -28,6 +28,7 @@ module SAWScript.HeapsterBuiltins
        , heapster_define_reachability_perm
        , heapster_define_perm
        , heapster_define_llvmshape
+       , heapster_define_rust_type
        , heapster_block_entry_hint
        , heapster_gen_block_perms_hint
        , heapster_join_point_hint
@@ -531,6 +532,10 @@ heapster_define_llvmshape _bic _opts henv nm w_int args_str sh_str =
      let env' = withKnownNat w $ permEnvAddDefinedShape env nm args mb_sh
      liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'
 
+heapster_define_rust_type :: BuiltinContext -> Options -> HeapsterEnv ->
+                             String -> TopLevel ()
+heapster_define_rust_type _bic _opts _henv _str = fail "Not yet implemented"
+
 -- | Add Heapster type-checking hint for some blocks in a function given by
 -- name. The blocks to receive the hint are those specified in the list, or all
 -- blocks if the list is empty.
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index ef2306f567..8dfa40b5e8 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -2829,6 +2829,14 @@ primitives = Map.fromList
     , " such that nm<x1,...,xn> is equivalent to the permission p."
     ]
 
+  , prim "heapster_define_rust_type"
+    "HeapsterEnv -> String -> TopLevel HeapsterEnv"
+    (bicVal heapster_define_rust_type)
+    Experimental
+    [ "heapster_define_rust_type env tp defines a Heapster LLVM shape from tp,"
+    , "a string representing a top-level struct or enum definition."
+    ]
+
   , prim "heapster_block_entry_hint"
     "HeapsterEnv -> String -> Int -> String -> String -> String -> TopLevel ()"
     (bicVal heapster_block_entry_hint)

From 386135d085b5fdc59daf1e6047c5a95249a3918f Mon Sep 17 00:00:00 2001
From: Chris Phifer <cphifer@galois.com>
Date: Wed, 21 Apr 2021 11:45:46 -0500
Subject: [PATCH 2/3] Fist crack at implementing SAW command

---
 src/SAWScript/HeapsterBuiltins.hs | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs
index e5931943bc..73f7bfc57c 100644
--- a/src/SAWScript/HeapsterBuiltins.hs
+++ b/src/SAWScript/HeapsterBuiltins.hs
@@ -532,9 +532,25 @@ heapster_define_llvmshape _bic _opts henv nm w_int args_str sh_str =
      let env' = withKnownNat w $ permEnvAddDefinedShape env nm args mb_sh
      liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'
 
+-- | Define a new named LLVM shape from a Rust type declaration
 heapster_define_rust_type :: BuiltinContext -> Options -> HeapsterEnv ->
                              String -> TopLevel ()
-heapster_define_rust_type _bic _opts _henv _str = fail "Not yet implemented"
+heapster_define_rust_type _bic _opts henv str =
+  -- NOTE: Looking at first LLVM module to determine pointer width. Need to
+  -- think more to determine if this is always a safe thing to do (e.g. are
+  -- there ever circumstances where different modules have different pointer
+  -- widths?)
+  do Some lm <- failOnNothing ("No LLVM modules found")
+                              (listToMaybe $ heapsterEnvLLVMModules henv)
+     let w = llvmModuleArchReprWidth lm
+     leq_proof <- case decideLeq (knownNat @1) w of
+       Left pf -> return pf
+       Right _ -> fail "LLVM arch width is 0!"
+     env <- liftIO $ readIORef (heapsterEnvPermEnvRef henv)
+     withKnownNat w $ withLeqProof leq_proof $
+       do nsh <- parseRustTypeString env w str
+          let env' = permEnvAddNamedShape env nsh
+          liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'
 
 -- | Add Heapster type-checking hint for some blocks in a function given by
 -- name. The blocks to receive the hint are those specified in the list, or all

From 5f611a77b9f088d0b73fc3c5cea2b52a766a6716 Mon Sep 17 00:00:00 2001
From: Chris Phifer <cphifer@galois.com>
Date: Thu, 22 Apr 2021 11:45:18 -0500
Subject: [PATCH 3/3] Correct type issues in rust type definition command

---
 src/SAWScript/HeapsterBuiltins.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs
index 7ff359f135..6d36bde16c 100644
--- a/src/SAWScript/HeapsterBuiltins.hs
+++ b/src/SAWScript/HeapsterBuiltins.hs
@@ -613,7 +613,7 @@ heapster_define_rust_type _bic _opts henv str =
        Right _ -> fail "LLVM arch width is 0!"
      env <- liftIO $ readIORef (heapsterEnvPermEnvRef henv)
      withKnownNat w $ withLeqProof leq_proof $
-       do nsh <- parseRustTypeString env w str
+       do SomeNamedShape nsh <- parseRustTypeString env w str
           let env' = permEnvAddNamedShape env nsh
           liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'