Fix Rust to Heapster type translation for functions with no return value (#1445)

* fixed the IRT description generation to match the recent change that made the translation of bitvector permissions to just be bitvectors

* updated xor_swap_rust example to use the Rust type in the SAW script

* added a case to the Rust to Heapster translator to handle function types with no return value

* whoops, forgot to update the bitcode file for xor_swap_rust

* bugfix in the Rust to Heapster translator: empty return types need to be converted to unit, not to the empty struct

* tweaked the error message for when Rust types do not translate correctly to the expected LLVM type

Author: Eddy Westbrook

heapster-saw/examples/xor_swap_rust.bc

@@ -1,10 +1,11 @@
 // This script expects to be run from the saw-script root directory
 enable_experimental;
-
 env <- heapster_init_env "xor_swap_rust" "xor_swap_rust.bc";
 
-xor_swap_sym <- heapster_find_symbol env "13xor_swap_rust13xor_swap_rust";
+heapster_define_llvmshape env "i64" 64 "" "fieldsh(exists x:bv 64.eq(llvmword(x)))";
 
-heapster_typecheck_fun_rename env xor_swap_sym "xor_swap_rust" "(x:bv 64, y:bv 64). arg0: ptr((W,0) |-> eq(llvmword(x))), arg1: ptr((W,0) |-> eq(llvmword(y))) -o arg0: ptr((W,0) |-> exists z:bv 64.eq(llvmword(z))), arg1: ptr((W,0) |-> exists z:bv 64.eq(llvmword(z))), ret:true";
+xor_swap_sym <- heapster_find_symbol env "13xor_swap_rust13xor_swap_rust";
+heapster_typecheck_fun_rename env xor_swap_sym "xor_swap_rust" "<'a,'b> fn (x:&'a mut i64, y:&'b mut i64)";
+//heapster_typecheck_fun_rename env xor_swap_sym "xor_swap_rust" "(x:bv 64, y:bv 64). arg0: ptr((W,0) |-> eq(llvmword(x))), arg1: ptr((W,0) |-> eq(llvmword(y))) -o arg0: ptr((W,0) |-> exists z:bv 64.eq(llvmword(z))), arg1: ptr((W,0) |-> exists z:bv 64.eq(llvmword(z))), ret:true";
 
 heapster_export_coq env "xor_swap_rust_gen.v";

heapster-saw/examples/xor_swap_rust.saw

@@ -673,12 +673,12 @@ un3SomeFunPerm args ret (Some3FunPerm fun_perm)
     return $ SomeFunPerm fun_perm
 un3SomeFunPerm args ret (Some3FunPerm fun_perm) =
   fail $ renderDoc $ vsep
-  [ pretty "Incorrect LLVM type for function permission:"
+  [ pretty "Unexpected LLVM type for function permission:"
   , permPretty emptyPPInfo fun_perm
-  , pretty "Expected type:"
+  , pretty "Actual LLVM type of function:"
     <+> PP.group (permPretty emptyPPInfo args) <+> pretty "=>"
     <+> PP.group (permPretty emptyPPInfo ret)
-  , pretty "Actual type:"
+  , pretty "Expected LLVM type of function:"
     <+> PP.group (permPretty emptyPPInfo (funPermArgs fun_perm))
     <+> pretty "=>"
     <+> PP.group (permPretty emptyPPInfo (funPermRet fun_perm)) ]
@@ -931,14 +931,24 @@ layoutFun abi arg_shs ret_sh =
        foldr appendArgLayout argLayout0 <$> mapM (layoutArgShape abi) arg_shs
      ret_layout_eith <- layoutArgShapeOrBlock abi ret_sh
      case ret_layout_eith of
+
+       -- Special case: if the return type is empty, use the unit type as the
+       -- return type
+       Right (ArgLayout Ctx.Empty _) ->
+         funPerm3FromArgLayoutNoArgs args_layout UnitRepr ValPerm_True
+
+       -- Special case: if the return type is a single field, remove the struct
+       -- type and just use the type of that single field
        Right (ArgLayout (Ctx.Empty Ctx.:> ret_tp)
               (argLayoutPerm1ToPerm -> ret_p)) ->
-         -- Special case: if the return type is a single field, remove the
-         -- struct type and just use the type of that single field
          funPerm3FromArgLayoutNoArgs args_layout ret_tp ret_p
+
+       -- If the return type can be laid out as a struct type, then do so
        Right (ArgLayout ret_ctx ret_p) ->
          funPerm3FromArgLayoutNoArgs args_layout (StructRepr ret_ctx)
          (argLayoutPermToPerm ret_p)
+
+       -- Otherwise add an extra pointer argument used as an out variable
        Left bp ->
            funPerm3FromArgLayout args_layout
            (extend Ctx.empty knownRepr)
@@ -1088,13 +1098,13 @@ rsConvertMonoFun w span abi ls fn_tp =
 rsConvertFun :: (1 <= w, KnownNat w) => prx w ->
                 Abi -> Generics Span -> FnDecl Span -> RustConvM Some3FunPerm
 rsConvertFun w abi (Generics ldefs _tparams@[]
-                    (WhereClause [] _) _) (FnDecl args (Just ret_tp) False _) =
+                    (WhereClause [] _) _) (FnDecl args maybe_ret_tp False _) =
   fmap (\ret ->
          tracePretty (pretty "rsConvertFun returning:" <+>
                       permPretty emptyPPInfo ret) ret) $
   withLifetimes ldefs $
   do arg_shapes <- mapM (rsConvert w) args
-     ret_shape <- rsConvert w ret_tp
+     ret_shape <- maybe (return PExpr_EmptyShape) (rsConvert w) maybe_ret_tp
      layoutFun abi arg_shapes ret_shape
 rsConvertFun _ _ _ _ = fail "rsConvertFun: unsupported Rust function type"