Merge pull request #1204 from GaloisInc/feature/rust-type-decls

Support building Heapster shapes from Rust type declarations

src/SAWScript/HeapsterBuiltins.hs

@@ -29,6 +29,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
@@ -596,6 +597,26 @@ 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 =
+  -- 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 SomeNamedShape 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
 -- blocks if the list is empty.

src/SAWScript/Interpreter.hs

@@ -2840,6 +2840,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)