diff --git a/heapster-saw/examples/rust_just_translation.saw b/heapster-saw/examples/rust_just_translation.saw new file mode 100644 index 0000000000..9d8035e3b7 --- /dev/null +++ b/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 { Ok (X), Err (Y) }"; + +// Infallable type +heapster_define_llvmshape env "Infallible" 64 "" "falsesh"; + +// Sum type +heapster_define_rust_type env "pub enum Sum { Left (X), Right (Y) }"; + +// The Option type +heapster_define_rust_type env "pub enum Option { 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]) -> ()"; diff --git a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs index 9e3a3ace7d..8dad282f13 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs +++ b/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,7 +1548,16 @@ 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) <- @@ -1556,10 +1565,7 @@ parseFunPermFromRust env w args ret 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 diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs index 1326c7f5a8..252b70c0dc 100644 --- a/src/SAWScript/HeapsterBuiltins.hs +++ b/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 diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 8fd5bd5c16..72ddc16582 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -4253,6 +4253,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) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 0294d00b02..3951205cc8 100644 --- a/src/SAWScript/Value.hs +++ b/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)