Toplevel rust translation (#1905)

* Add translate_rust_type so we can call the function from the command line

* Last details to get rust translation working at the toplevel

* add example file

* Better descriptions

* Remove comments

* Improve description for heapster_parse_test

* Description was on the wrong function

* Deduplicating functions parseFunPermFromRust and parseSome3FunPermFromRust

* Fix the arguments

* Generalize un3SomeFunPerm

* wrap line to 80 columns

* Simplify expression (and add alignment)

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/RustTypes.hs

@@ -898,24 +898,24 @@ instance PermPretty Some3FunPerm where
   permPrettyM (Some3FunPerm fun_perm) = permPrettyM fun_perm
 
 -- | Try to convert a 'Some3FunPerm' to a 'SomeFunPerm' at a specific type
-un3SomeFunPerm :: CruCtx args -> TypeRepr ret -> Some3FunPerm ->
-                  RustConvM (SomeFunPerm args ret)
+un3SomeFunPerm :: (Fail.MonadFail m) => CruCtx args -> TypeRepr ret -> Some3FunPerm ->
+                  m (SomeFunPerm args ret)
 un3SomeFunPerm args ret (Some3FunPerm fun_perm)
   | Just Refl <- testEquality args (funPermArgs fun_perm)
   , Just Refl <- testEquality ret (funPermRet fun_perm) =
     return $ SomeFunPerm fun_perm
 un3SomeFunPerm args ret (Some3FunPerm fun_perm) =
-  rsPPInfo >>= \ppInfo ->
-  fail $ renderDoc $ vsep
-  [ pretty "Unexpected LLVM type for function permission:"
-  , permPretty ppInfo fun_perm
-  , pretty "Actual LLVM type of function:"
-    <+> PP.group (permPretty ppInfo args) <+> pretty "=>"
-    <+> PP.group (permPretty ppInfo ret)
-  , pretty "Expected LLVM type of function:"
-    <+> PP.group (permPretty ppInfo (funPermArgs fun_perm))
-    <+> pretty "=>"
-    <+> PP.group (permPretty ppInfo (funPermRet fun_perm)) ]
+  let ppInfo = emptyPPInfo in
+    fail $ renderDoc $ vsep
+    [ pretty "Unexpected LLVM type for function permission:"
+    , permPretty ppInfo fun_perm
+    , pretty "Actual LLVM type of function:"
+      <+> PP.group (permPretty ppInfo args) <+> pretty "=>"
+      <+> PP.group (permPretty ppInfo ret)
+    , pretty "Expected LLVM type of function:"
+      <+> PP.group (permPretty ppInfo (funPermArgs fun_perm))
+      <+> pretty "=>"
+      <+> PP.group (permPretty ppInfo (funPermRet fun_perm)) ]
 
 -- | This is the more general form of 'funPerm3FromArgLayout, where there can be
 -- ghost variables in the 'ArgLayout'
@@ -1548,18 +1548,24 @@ rsConvertFun _ _ _ _ = fail "rsConvertFun: unsupported Rust function type"
 parseFunPermFromRust :: (Fail.MonadFail m, 1 <= w, KnownNat w) =>
                         PermEnv -> prx w -> CruCtx args -> TypeRepr ret ->
                         String -> m (SomeFunPerm args ret)
-parseFunPermFromRust env w args ret str
+parseFunPermFromRust env w args ret str =
+  do get3SomeFunPerm <- parseSome3FunPermFromRust env w str
+     un3SomeFunPerm args ret get3SomeFunPerm
+
+
+-- | Just like `parseFunPermFromRust`, but returns a `Some3FunPerm`
+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) $
-    do some_fun_perm <-
-         rsConvertFun w abi (Generics
-                             (rust_ls1 ++ rust_ls2) rust_tvars wc span) fn_tp
-       un3SomeFunPerm args ret some_fun_perm
+    rsConvertFun w abi (Generics (rust_ls1 ++ rust_ls2) rust_tvars wc span) fn_tp
 
   | Just i <- findIndex (== '>') str
   , (gen_str, _) <- splitAt (i+1) str
@@ -1570,7 +1576,7 @@ parseFunPermFromRust env w args ret str
   , (_, fn_str) <- splitAt (i+1) str
   , Left err <- parse @(Ty Span) (inputStreamFromString fn_str) =
     fail ("Error parsing generics: " ++ show err)
-parseFunPermFromRust _ _ _ _ str =
+parseSome3FunPermFromRust _ _ str =
     fail ("Malformed Rust type: " ++ str)
 
 -- | Parse a polymorphic Rust type declaration and convert it to a Heapster

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
@@ -1040,6 +1042,19 @@ 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
+        liftIO $ putStrLn $ permPrettyString emptyPPInfo 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

@@ -4328,6 +4328,14 @@ 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 a Rust function type and print the equivalent Heapser type. "
+    , "Ideal for learning how Rust types are translated into Heapster. "
+    ]
+
   , prim "heapster_parse_test"
     "LLVMModule -> String -> String -> TopLevel ()"
     (bicVal heapster_parse_test)

src/SAWScript/Value.hs

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