Toplevel rust translation

heapster-saw/examples/rust_just_translation.saw

@@ -0,0 +1,87 @@
+// This file demonstrates how to use the `heapster_trans_rust_type`
+// command to translate rust signatures to heapster.
+enable_experimental;
+
+// Integer types This is wrong... we don't need an environment. 
+env <- heapster_init_env_from_file "rust_data.sawcore" "rust_data.bc";
+
+print "Define Rust types.";
+/***
+ *** Types
+ ***/
+
+// Integer types
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+heapster_define_perm env "int32" " " "llvmptr 32" "exists x:bv 32.eq(llvmword(x))";
+heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
+heapster_define_perm env "int1" " " "llvmptr 1" "exists x:bv 1.eq(llvmword(x))";
+
+heapster_define_llvmshape env "u64" 64 "" "fieldsh(int64<>)";
+heapster_define_llvmshape env "u32" 64 "" "fieldsh(32,int32<>)";
+heapster_define_llvmshape env "u8" 64 "" "fieldsh(8,int8<>)";
+
+heapster_define_llvmshape env "usize" 64 "" "fieldsh(int64<>)";
+heapster_define_llvmshape env "char" 64 "" "fieldsh(32,int32<>)";
+
+// bool type
+heapster_define_llvmshape env "bool" 64 "" "fieldsh(1,int1<>)";
+
+// Box type
+heapster_define_llvmshape env "Box" 64 "T:llvmshape 64" "ptrsh(T)";
+
+// Result type
+heapster_define_rust_type env "pub enum Result<X,Y> { Ok (X), Err (Y) }";
+
+// Infallable type
+heapster_define_llvmshape env "Infallible" 64 "" "falsesh";
+
+// Sum type
+heapster_define_rust_type env "pub enum Sum<X,Y> { Left (X), Right (Y) }";
+
+// The Option type
+heapster_define_rust_type env "pub enum Option<X> { None, Some (X) }";
+
+
+print "";
+print "-----------------------------------------------";
+print "Translate 'unit'";
+print "Rust: \n<> fn () -> ()";
+print "Heapster:";
+heapster_trans_rust_type env "<> fn () -> ()";
+
+print "";
+print "-----------------------------------------------";
+print "Translate 'add'";
+print "Rust: \n<> fn (x:u64, y:u64) -> u64";
+print "Heapster:";
+heapster_trans_rust_type env "<> fn (x:u64, y:u64) -> u64";
+
+
+print "";
+print "-----------------------------------------------";
+print "Translate 'Ptr add'";
+print "Rust: \n<'a,'b> fn (x:&'a u64, y:&'a u64) -> u64";
+print "Heapster:";
+heapster_trans_rust_type env "<'a,'b> fn (x:&'a u64, y:&'a u64) -> u64";
+
+print "";
+print "-----------------------------------------------";
+print "Translate 'array length'";
+print "Rust: \n<'a> fn (x:&'a [u64]) -> u64";
+print "Heapster:";
+heapster_trans_rust_type env "<'a> fn (x:&'a [u64]) -> u64";
+
+
+print "";
+print "-----------------------------------------------";
+print "Translate 'add two array'";
+print "Rust: \n<'a, 'b, 'c> fn (l1:&'a [u64], l2:&'b [u64]) -> &'c [u64]";
+print "Heapster:";
+heapster_trans_rust_type env "<'a, 'b, 'c> fn (l1:&'a [u64], l2:&'b [u64]) -> &'c [u64]";
+
+print "";
+print "-----------------------------------------------";
+print "Translate 'add two array in place'";
+print "Rust: \n<'a, 'b> fn (l1:&'a mut[u64], l2:&'b [u64]) -> ()";
+print "Heapster:";
+heapster_trans_rust_type env "<'a, 'b> fn (l1:&'a mut[u64], l2:&'b [u64]) -> ()";

heapster-saw/src/Verifier/SAW/Heapster/PermParser.hs

@@ -211,6 +211,20 @@ parseFunPermStringMaybeRust nm w env args ret str =
     Just '<' -> parseFunPermFromRust env w args ret str
     _ -> parseFunPermString nm env args ret str
 
+-- -- | Just like `parseFunPermStringMaybeRust` but usese `parseSome3FunFromRust`
+-- parseSome3FunPermStringMaybeRust ::
+--   (1 <= w, KnownNat w, Fail.MonadFail m) =>
+--   String                {- ^ object name                -} ->
+--   prx w                 {- ^ pointer bit-width proxy    -} ->
+--   PermEnv               {- ^ permission environment     -} ->
+--   String                {- ^ input text                 -} ->
+--   m Some3FunPerm
+-- parseSome3FunPermStringMaybeRust nm w env str =
+--   case find (\c -> c == '<' || c == '(') str of
+--     Just '<' -> parseSome3FunPermFromRust env w str
+--     _ -> parseFunPermString nm env args ret str
+
+
 -- | Parse a 'SomeNamedShape' from the given 'String'. This 'SomeNamedShape'
 -- must be a valid Rust @struct@ or @enum@ declaration given in Rust syntax.
 -- The @w@ argument gives the bit width of pointers in the current\

heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs

@@ -1573,6 +1573,34 @@ parseFunPermFromRust env w args ret str
 parseFunPermFromRust _ _ _ _ str =
     fail ("Malformed Rust type: " ++ str)
 
+
+-- | Just like `parseFunPermFromRust`, but doesn't take `args` and `ret`.
+-- usefull to translate rust when there is no LLVM module (e.g. from command line)
+parseSome3FunPermFromRust :: (Fail.MonadFail m, 1 <= w, KnownNat w) =>
+                        PermEnv -> prx w ->
+                        String -> m Some3FunPerm
+parseSome3FunPermFromRust env w str
+  | Just i <- findIndex (== '>') str
+  , (gen_str, fn_str) <- splitAt (i+1) str
+  , Right (Generics rust_ls1 rust_tvars wc span) <-
+      parse (inputStreamFromString gen_str)
+  , Right (BareFn _ abi rust_ls2 fn_tp _) <-
+      parse (inputStreamFromString fn_str) =
+    runLiftRustConvM (mkRustConvInfo env) $
+    rsConvertFun w abi (Generics (rust_ls1 ++ rust_ls2) rust_tvars wc span) fn_tp
+
+  | Just i <- findIndex (== '>') str
+  , (gen_str, _) <- splitAt (i+1) str
+  , Left err <- parse @(Generics Span) (inputStreamFromString gen_str) =
+    fail ("Error parsing generics: " ++ show err)
+
+  | Just i <- findIndex (== '>') str
+  , (_, fn_str) <- splitAt (i+1) str
+  , Left err <- parse @(Ty Span) (inputStreamFromString fn_str) =
+    fail ("Error parsing generics: " ++ show err)
+parseSome3FunPermFromRust _ _ str =
+    fail ("Malformed Rust type: " ++ str)
+
 -- | Parse a polymorphic Rust type declaration and convert it to a Heapster
 -- shape
 -- Note: No CruCtx / TypeRepr as arguments for now

src/SAWScript/HeapsterBuiltins.hs

@@ -48,6 +48,7 @@ module SAWScript.HeapsterBuiltins
        , heapster_find_trait_method_symbol
        , heapster_assume_fun
        , heapster_assume_fun_rename
+       , heapster_translate_rust_type
        , heapster_assume_fun_rename_prim
        , heapster_assume_fun_multi
        , heapster_set_event_type
@@ -124,6 +125,7 @@ import Verifier.SAW.Heapster.Permissions
 import Verifier.SAW.Heapster.SAWTranslation
 import Verifier.SAW.Heapster.IRTTranslation
 import Verifier.SAW.Heapster.PermParser
+import Verifier.SAW.Heapster.RustTypes (parseSome3FunPermFromRust, Some3FunPerm(..))
 import Verifier.SAW.Heapster.ParsedCtx
 import qualified Verifier.SAW.Heapster.IDESupport as HIDE
 import Verifier.SAW.Heapster.LLVMGlobalConst
@@ -1020,7 +1022,7 @@ heapster_assume_fun_rename _bic _opts henv nm nm_to perms_string term_string =
   do Some lm <- failOnNothing ("Could not find symbol: " ++ nm)
                               (lookupModContainingSym henv nm)
      sc <- getSharedContext
-     let w = llvmModuleArchReprWidth lm
+     let w = llvmModuleArchReprWidth lm -- Should hardcode 64
      leq_proof <- case decideLeq (knownNat @1) w of
        Left pf -> return pf
        Right _ -> fail "LLVM arch width is 0!"
@@ -1040,6 +1042,23 @@ heapster_assume_fun_rename _bic _opts henv nm nm_to perms_string term_string =
                                            (globalOpenTerm term_ident)
         liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env''
 
+heapster_translate_rust_type :: BuiltinContext -> Options -> HeapsterEnv ->
+                                String -> TopLevel ()
+heapster_translate_rust_type _bic _opts henv perms_string =
+  do env <- liftIO $ readIORef $ heapsterEnvPermEnvRef henv
+     let w64 = (knownNat @64::NatRepr 64)
+     leq_proof <- case decideLeq (knownNat @1) w64 of
+       Left pf -> return pf
+       Right _ -> fail "LLVM arch width is 0!"
+     withKnownNat w64 $ withLeqProof leq_proof $ do
+        Some3FunPerm fun_perm <-
+          parseSome3FunPermFromRust env w64 perms_string
+          --parseFunPermStringMaybeRust "permissions" w64 env args ret perms_string
+        liftIO $ putStrLn $ permPrettyString emptyPPInfo fun_perm
+
+        -- Lookup a how to print to io & and, looking into permissions.hs
+          -- for permPrettyString and pass an empty ppInfo to print 'fun_perm'
+
 -- | Create a new SAW core primitive named @nm@ with type @tp@ in the module
 -- associated with the supplied Heapster environment, and return its identifier
 insPrimitive :: HeapsterEnv -> String -> Term -> TopLevel Ident

src/SAWScript/Interpreter.hs

@@ -4253,11 +4253,18 @@ primitives = Map.fromList
     [ "Tell Heapster whether to perform its translation-time checks of the "
     , "well-formedness of type-checking proofs" ]
 
+  , prim "heapster_trans_rust_type"
+    "HeapsterEnv -> String -> TopLevel ()"
+    (bicVal heapster_translate_rust_type)
+    Experimental
+    [ "Parse and print back a set of Heapster permissions for a function"
+    ]
+
   , prim "heapster_parse_test"
     "LLVMModule -> String -> String -> TopLevel ()"
     (bicVal heapster_parse_test)
     Experimental
-    [ "Parse and print back a set of Heapster permissions for a function"
+    [ "Parse the Rust signature for a function and print the equivalent Heapser type. Ideal for learning how Rust types are translated into Heapster. "
     ]
 
   , prim "heapster_dump_ide_info"

src/SAWScript/Value.hs

@@ -977,7 +977,7 @@ instance FromValue a => FromValue (TopLevel a) where
       v1 <- withPosition pos (fromValue m1)
       m2 <- applyValue v2 v1
       fromValue m2
-    fromValue _ = error "fromValue TopLevel"
+    fromValue v = error $ "fromValue TopLevel:" <> show v
 
 instance IsValue a => IsValue (ProofScript a) where
     toValue m = VProofScript (fmap toValue m)