Toplevel rust translation #1905

scuellar · 2023-08-11T18:17:27Z

This PR adds a new command

heapster_trans_rust_type : HeapsterEnv -> String -> TopLevel ()

takes the Rust signature for a function and prints the equivalent Heapser type. It is ideal for learning and experimenting with the Rust -> Heapster translation.

The PR includes the file rust_just_translation.saw which demonstrates how to use the command to translate various functions. The file also demonstrates how to (a) create the necessary definitions to support rust and (b) create a proper, empty environment for the command to work.

The example can be ran from the examples folder with

cabal run saw rust_just_translation.saw

…line

eddywestbrook

Looks good overall! Please address the comments I made before we can approve this for merge.

eddywestbrook · 2023-08-14T16:38:05Z

src/SAWScript/HeapsterBuiltins.hs

@@ -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


This shouldn't actually be hard coded to 64, since it could potentially be useful to have it match some other architecture with a different bit width. Currently, the way to achieve that is to specify it in the Heapster environment. I could imagine making this an argument instead of requiring a Heapster environment, but the current approach seems easiest for now, so maybe just remove this comment?

eddywestbrook · 2023-08-14T16:44:04Z

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)


It's not that there is no LLVM module, it's that there is no specified LLVM function.

Also, it seems like the only place where args and ret are used in parseFunPermFromRust is in the call to un3SomeFunPerm, so, in order to remove all the code duplication between that function and this one, you should redefine parseFunPermFromRust to just call parseSome3FunPermFromRust and then pass the result to un3SomeFunPerm.

Fixed.

I removed the duplication and got it to typecheck. It looks right to me, but it's now doing runLiftRustConvM twice. That seems ok to me, but please make sure it's not introducing any efficiency problems.

Alternatively, I can make parseSome3FunPermFromRust take "lifting" function which can be instantiated to id and for un3SomeFunPerm.

Oh, right, I didn't notice that un3SomeFunPerm was inside RustConvM. It looks like that function could instead be changed to return an m (SomeFunPerm args ret) in any monad with a MonadFail instance, by using emptyPPInfo in place of rsPPInfo, since un3SomeFunPerm is only ever run at the top level, where the context is empty.

eddywestbrook · 2023-08-14T16:44:45Z

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`


Please don't leave these comments in the code.

eddywestbrook · 2023-08-14T16:45:22Z

src/SAWScript/HeapsterBuiltins.hs

+          --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


Please remove these comments from the code

eddywestbrook · 2023-08-14T16:45:34Z

src/SAWScript/HeapsterBuiltins.hs

+     withKnownNat w64 $ withLeqProof leq_proof $ do
+        Some3FunPerm fun_perm <-
+          parseSome3FunPermFromRust env w64 perms_string
+          --parseFunPermStringMaybeRust "permissions" w64 env args ret perms_string


Please remove this commented out line from the code

eddywestbrook · 2023-08-14T16:47:04Z

src/SAWScript/Interpreter.hs

+    "HeapsterEnv -> String -> TopLevel ()"
+    (bicVal heapster_translate_rust_type)
+    Experimental
+    [ "Parse and print back a set of Heapster permissions for a function"


I feel like this description is slightly imprecise in a way that might confuse the user, because it sounds like the function is parsing Heapster permissions and printing them. The point of this function is to convert a Rust type to a Heapster type and print out the result. So maybe say something like that.

eddywestbrook · 2023-08-14T16:48:48Z

src/SAWScript/Interpreter.hs

  , 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. "


Ohh, it looks like the doc string for heapster_parse_test got switched with that for heapster_trans_rust_type. Slight tweak, though: technically, this isn't parsing the signature for a function, because there need not be any function associated with the type. Instead, it is just parsing a Rust function type.

…mRust

eddywestbrook · 2023-08-14T19:50:29Z

src/SAWScript/Interpreter.hs

+    "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. "


Please wrap this line to 80 columns like the rest of the file

eddywestbrook · 2023-08-15T14:31:17Z

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

 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 ->
+  (return emptyPPInfo) >>= \ppInfo ->


How about let ppInfo = emptyPPInfo in instead of binding a return, which looks kind of weird to a Hasekll-er

eddywestbrook

Please address the one remaining small change I suggested. Otherwise, this looks good!

scuellar added 4 commits July 18, 2023 15:56

Add translate_rust_type so we can call the function from the command …

951fb17

…line

Last details to get rust translation working at the toplevel

3b67591

add example file

82d34dd

Better descriptions

c9c88b4

scuellar added the subsystem: heapster Issues specifically related to memory verification using Heapster label Aug 11, 2023

scuellar requested a review from eddywestbrook August 11, 2023 18:17

eddywestbrook reviewed Aug 14, 2023

View reviewed changes

scuellar added 5 commits August 14, 2023 13:23

Remove comments

c7fe919

Improve description for heapster_parse_test

fb24c94

Description was on the wrong function

2a79212

Deduplicating functions parseFunPermFromRust and parseSome3FunPermFro…

72dbd3e

…mRust

Fix the arguments

d204452

eddywestbrook reviewed Aug 14, 2023

View reviewed changes

scuellar added 2 commits August 14, 2023 16:36

Generalize un3SomeFunPerm

8326fc7

wrap line to 80 columns

453b05e

eddywestbrook reviewed Aug 15, 2023

View reviewed changes

eddywestbrook approved these changes Aug 15, 2023

View reviewed changes

Simplify expression (and add alignment)

56bfeac

scuellar added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Aug 15, 2023

eddywestbrook merged commit d4b61c3 into master Aug 16, 2023
34 of 36 checks passed

mergify bot deleted the toplevel-rust-translation branch August 16, 2023 21:57

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Toplevel rust translation #1905

Toplevel rust translation #1905

scuellar commented Aug 11, 2023 •

edited

Loading

eddywestbrook left a comment

eddywestbrook Aug 14, 2023

eddywestbrook Aug 14, 2023

scuellar Aug 14, 2023

eddywestbrook Aug 14, 2023

eddywestbrook Aug 14, 2023

eddywestbrook Aug 14, 2023

eddywestbrook Aug 14, 2023

eddywestbrook Aug 14, 2023

eddywestbrook Aug 14, 2023

eddywestbrook Aug 14, 2023

eddywestbrook Aug 15, 2023

eddywestbrook left a comment

Toplevel rust translation #1905

Toplevel rust translation #1905

Conversation

scuellar commented Aug 11, 2023 • edited Loading

eddywestbrook left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eddywestbrook left a comment

Choose a reason for hiding this comment

scuellar commented Aug 11, 2023 •

edited

Loading