fixing the return type of CHERI_intrinsic

rems-project · Aug 27, 2023 · 0ed72b0 · 0ed72b0
1 parent 9ee1f53
commit 0ed72b0
Show file tree

Hide file tree

Showing 3 changed files with 25 additions and 5 deletions.
diff --git a/frontend/model/core_typing.lem b/frontend/model/core_typing.lem
@@ -1534,7 +1534,7 @@ let memop_signature = function
       let oTys_opt = Utils.maybe_mapM Core_aux.core_object_type_of_ctype tys in
       match (core_object_type_of_ctype ret_ty, oTys_opt ) with
         | (Just ret_oTy, Just oTys) ->
-            (BTy_object ret_oTy, List.map BTy_object oTys)
+            (BTy_loaded ret_oTy, List.map BTy_object oTys)
         | _ ->
             error "when typechecking CHERI intrinsics failed to get the params object types"
       end

diff --git a/frontend/model/driver.lem b/frontend/model/driver.lem
@@ -866,7 +866,7 @@ let perform_memop_request2 loc memop cvals tid mk_th_st =
         liftMem (Mem.call_intrinsic loc str mvals) >>= fun res_opt ->
         match res_opt with
           | Just res ->
-              ND.return (mk_th_st (Core.Vobject (snd (Caux.objectValueFromMemValue res))))
+              ND.return (mk_th_st (Core.Vloaded (snd (Caux.loadedValueFromMemValue res))))
           | Nothing ->
             ND.return (mk_th_st Core.Vunit)
         end

diff --git a/frontend/model/translation.lem b/frontend/model/translation.lem
@@ -2313,7 +2313,28 @@ end
             C.Expr [] (C.Ememop (Mem_common.CHERI_intrinsic str (result_ty, [])) [])
           end
 
-      | A.AilEcall (A.AnnotatedExpression _ _ _ (A.AilEbuiltin (A.AilBCHERI str))) (_::_ as es) ->
+      | A.AilEcall (A.AnnotatedExpression _ _ _ (A.AilEbuiltin (A.AilBCHERI str))) [e] ->
+          self e >>= fun core_e ->
+          let bTy_ret = maybe C.BTy_unit C.BTy_loaded (Caux.core_object_type_of_ctype result_ty) in
+          let ty_e = ctype_of e in
+          let oTy = force_core_object_type_of_ctype ty_e in
+          let arg_bTy = C.BTy_loaded oTy in
+          E.wrapped_fresh_symbol bTy_ret            >>= fun memop_wrp ->
+          E.wrapped_fresh_symbol arg_bTy            >>= fun arg_wrp   ->
+          E.wrapped_fresh_symbol (C.BTy_object oTy) >>= fun obj_wrp   ->
+          let memop = Mem_common.CHERI_intrinsic str (result_ty, [ty_e]) in
+          E.return begin
+            Caux.mk_sseq_e arg_wrp.E.sym_pat core_e
+            begin
+              Caux.mk_case_e arg_wrp.E.sym_pe
+                [ ( Caux.mk_specified_pat obj_wrp.E.sym_pat
+                  , (C.Expr [] (C.Ememop memop [obj_wrp.E.sym_pe])) )
+                ; ( Caux.mk_empty_pat arg_bTy
+                  , Caux.mk_pure_e (Caux.mk_undef_pe loc (Undefined.DUMMY "Elab, CHERI intrinsics (unspec)")) ) ]
+            end
+          end
+
+      | A.AilEcall (A.AnnotatedExpression _ _ _ (A.AilEbuiltin (A.AilBCHERI str))) (_::_::_ as es) ->
           E.mapM self es >>= fun core_es ->
           let bTy_ret = maybe C.BTy_unit C.BTy_loaded (Caux.core_object_type_of_ctype result_ty) in
           let oTys = List.map (fun e -> force_core_object_type_of_ctype (ctype_of e)) es in
@@ -2340,8 +2361,7 @@ end
             begin
               Caux.mk_case_e args_wrp.E.sym_pe
                 [ ( Caux.mk_tuple_pat (List.map Caux.mk_specified_pat (List.reverse rev_obj_sym_pats))
-                  , Caux.mk_wseq_e memop_wrp.E.sym_pat (C.Expr [] (C.Ememop memop (List.reverse rev_obj_sym_pes)))
-                      (Caux.mk_pure_e (Caux.mk_specified_pe memop_wrp.E.sym_pe)) )
+                  , (C.Expr [] (C.Ememop memop (List.reverse rev_obj_sym_pes))) )
                 ; ( Caux.mk_empty_pat args_bTy
                   , Caux.mk_pure_e (Caux.mk_undef_pe loc (Undefined.DUMMY "Elab, CHERI intrinsics (unspec)")) ) ]
             end