From 56a0662747876ac2103a6bc4cc973dc8029f4643 Mon Sep 17 00:00:00 2001 From: Kayvan Memarian Date: Sun, 15 Sep 2024 00:32:30 +0100 Subject: [PATCH] CHERI: using capability permissions in the allocation/init of const objects This follows the proposal from issue #229 --- frontend/model/translation.lem | 59 +++++++++++++++------------ frontend/model/translation_aux.lem | 14 +++++++ frontend/model/translation_effect.lem | 21 +++++++++- 3 files changed, 67 insertions(+), 27 deletions(-) diff --git a/frontend/model/translation.lem b/frontend/model/translation.lem index 1d9f5d2a5..3d2ad19e0 100644 --- a/frontend/model/translation.lem +++ b/frontend/model/translation.lem @@ -1806,18 +1806,27 @@ end end))) ) ] end end - | A.AilEident id -> - let id_sym_pe = + | A.AilEident sym -> + E.cheri_const_alias_map >>= fun alias_map -> + let sym_alias_if_CHERI = + if Global.is_CHERI () then + match Map.lookup sym alias_map with + | Just cheri_sym -> cheri_sym + | Nothing -> sym + end + else + sym in + let normalised_sym = match ctx with | ECTX_glob glob_sym sym' -> - if id = glob_sym then - Caux.mk_sym_pe sym' + if sym = glob_sym then + sym' else - Caux.mk_sym_pe id + sym_alias_if_CHERI | _ (* ECTX_other *) -> - Caux.mk_sym_pe id + sym_alias_if_CHERI end in - E.return (Caux.mk_pure_e id_sym_pe) + E.return (Caux.mk_pure_e (Caux.mk_sym_pe normalised_sym)) | A.AilEcast _ cast_ty e -> let e_ty = ctype_of e in @@ -3518,7 +3527,7 @@ let rec translate_stmt stdlib tagDefs f env (A.AnnotatedStatement loc stmt_attrs let decls = List.map (fun (sym, _, (_, qs, ty)) -> (sym, (qs, ty))) decls_with_loc in E.with_block_objects decls begin E.mapM self ss - end >>= fun (compound_lits, core_ss) -> + end >>= fun (const_aliases, compound_lits, core_ss) -> let lit_pats_core_creates : list (C.pattern * C.expr unit) = List.map (fun (loc, prefix, sym, is_const, ty) -> let core_ty = Caux.mk_ail_ctype_pe ty in @@ -3542,6 +3551,13 @@ let rec translate_stmt stdlib tagDefs f env (A.AnnotatedStatement loc stmt_attrs ( Caux.mk_sym_pat sym (C.BTy_object C.OTy_pointer) , Caux.pcreate (Loc.with_cursor_from loc ident_loc) align_ival c_ty (Symbol.PrefSource ident_loc [f; sym]) ) ) decls_with_loc in + let cheri_const_intrinsic = List.map (fun (sym, (qs, ty, sym')) -> + (* TODO: the partial pattern match in the lets is tasteless (even though the memop() + never evaluates to an unspecified value) *) + let ptr_ty = Ctype.mk_ctype_pointer qs ty in + ( Caux.mk_specified_pat (Caux.mk_sym_pat sym' (C.BTy_object C.OTy_pointer)) + , cheri_readonly_perms ptr_ty (Caux.mk_sym_pe sym) ) + ) const_aliases in let pat_core_kills : list (C.expr unit) = List.map (fun (loc, _, sym, _, ty) -> Caux.pkill (Loc.with_cursor_from loc loc) (C.Static ty) (Caux.mk_sym_pe sym) @@ -3556,7 +3572,7 @@ let rec translate_stmt stdlib tagDefs f env (A.AnnotatedStatement loc stmt_attrs ) decls_with_loc in E.return ( (* NOTE: we sequence (left-to-right) the creates and kills of the block-scoped objects *) - Caux.mk_sseqs (lit_pats_core_creates ++ pats_core_creates) begin + Caux.mk_sseqs (lit_pats_core_creates ++ pats_core_creates ++ cheri_const_intrinsic) begin Caux.mk_unit_sseq (core_ss ++ core_kills ++ pat_core_kills) Caux.mk_skip_e end @@ -4044,7 +4060,7 @@ let translate_program stdlib (startup_sym_opt, sigm) = (* NOTE: we use `with_block_objects`, for the compound_literal tracking *) E.with_block_objects [] begin wrapped_translate_expression true (ECTX_glob sym sym_global) ((Nothing: maybe Symbol.sym), (Nothing: maybe Symbol.sym)) stdlib core_tagDefs expr - end >>= fun (compound_lits, core) -> + end >>= fun (_, compound_lits, core) -> let lit_pats_core_creates : list (C.pattern * C.expr unit) = List.map (fun (loc, prefix, sym, is_const, ty) -> let core_ty = Caux.mk_ail_ctype_pe ty in @@ -4160,7 +4176,7 @@ let translate_program stdlib (startup_sym_opt, sigm) = let (mk_body_wrapper, label_visibles) = if is_using_inner_arg_temps then let xs = List.map (fun (sym, (_, ty, _)) -> (sym, ty)) (List.zip param_syms params) in - ( (fun z -> E.with_block_objects (List.map (fun (sym, ty) -> (sym, (Ctype.no_qualifiers, ty))) xs) z >>= fun (_, ret) -> E.return ret) + ( (fun z -> E.with_block_objects (List.map (fun (sym, ty) -> (sym, (Ctype.no_qualifiers, ty))) xs) z >>= fun (_, _, ret) -> E.return ret) , Map.map (fun z -> z ++ xs) visibles.label_visibles_ ) else ((fun z -> z), visibles.label_visibles_) in @@ -4275,20 +4291,13 @@ let translate_program stdlib (startup_sym_opt, sigm) = ; ( Caux.mk_empty_pat C.BTy_unit , Caux.pstore_lock loc ty_pe ptr_wrp.E.sym_pe e_init Cmm.NA ) ] begin - (* TODO: the mask should be ~(BIT(16)|BIT(13)|BIT(12)) but there is - currently a mismatch in the Coq memory model between the mask u64 and - the Permission.t value. -- FIXME when the coq is updated *) - (* let mask_pe = Caux.mk_integer_pe 0xfffffffffffecfff in *) - let mask_pe = Caux.mk_integer_pe 0xffffffffff7fffff in - Caux.mk_sseq_e tmp_wrp.E.sym_pat - (Caux.mk_memop_e (Mem_common.CHERI_intrinsic "cheri_perms_and" (ptr_ty, [ptr_ty; Ctype.size_t])) - [ ptr_wrp.E.sym_pe; mask_pe ]) - (Caux.mk_case_e tmp_wrp.E.sym_pe - [ ( Caux.mk_specified_pat ptr_wrp.E.sym_pat - , Caux.mk_pure_e ptr_wrp.E.sym_pe ) - ; ( Caux.mk_unspecified_pat (Caux.mk_empty_pat C.BTy_ctype) - , Caux.mk_pure_e (Caux.mk_undef_pe loc (Undefined.DUMMY "Unspecified cheri_perms_and()")) ) ] ) - end in + Caux.mk_sseq_e tmp_wrp.E.sym_pat (cheri_readonly_perms ptr_ty ptr_wrp.E.sym_pe) + (Caux.mk_case_e tmp_wrp.E.sym_pe + [ ( Caux.mk_specified_pat ptr_wrp.E.sym_pat + , Caux.mk_pure_e ptr_wrp.E.sym_pe ) + ; ( Caux.mk_unspecified_pat (Caux.mk_empty_pat C.BTy_ctype) + , Caux.mk_pure_e (Caux.mk_undef_pe loc (Undefined.DUMMY "Unspecified cheri_perms_and()")) ) ] ) + end in E.return ((sym, C.GlobalDef (C.BTy_object C.OTy_pointer, ty) expr) :: acc) else fun acc (loc, sym, ty, e_init) -> diff --git a/frontend/model/translation_aux.lem b/frontend/model/translation_aux.lem index b74a70ea5..bc2d6c89c 100644 --- a/frontend/model/translation_aux.lem +++ b/frontend/model/translation_aux.lem @@ -438,3 +438,17 @@ let conv_arith stdlib ty_src ty_dst pe = else (* NOTE: this case will occurs in particular if ty_src is an atomic type *) error "Translation_aux.conv_arith, not (is_arithmetic ty_src)" + + +(* + LET mask = [| ~(CAP_PERM_STORE || CAP_PERM_STORE_CAP || CAP_PERM_STORE_LOCAL_CAP) |] IN + memop(cheri_perms_and, ptr, mask) +*) +let cheri_readonly_perms ptr_ty ptr_pe = + (* TODO: the mask should be ~(BIT(16)|BIT(13)|BIT(12)) but there is + currently a mismatch in the Coq memory model between the mask u64 and + the Permission.t value. -- FIXME when the coq is updated *) + (* let mask_pe = Caux.mk_integer_pe 0xfffffffffffecfff in *) + let mask_pe = Caux.mk_integer_pe 0xffffffffff7fffff in + Caux.mk_memop_e (Mem_common.CHERI_intrinsic "cheri_perms_and" (ptr_ty, [ptr_ty; size_t])) + [ ptr_pe; mask_pe ] diff --git a/frontend/model/translation_effect.lem b/frontend/model/translation_effect.lem index ebb51ae52..f3aa22e86 100644 --- a/frontend/model/translation_effect.lem +++ b/frontend/model/translation_effect.lem @@ -30,6 +30,8 @@ type elab_state = <| temporary_objects: list (wrapped_symbol * Ctype.ctype); visible_objects_types_markers_env: map nat (list (Symbol.sym * Ctype.ctype)); + cheri_const_alias: map Symbol.sym Symbol.sym; + errors: list string; (* readonly *) @@ -46,6 +48,7 @@ let elab_init callconv = <| compound_literals= []; temporary_objects= []; visible_objects_types_markers_env = Map.empty; + cheri_const_alias= Map.empty; errors = []; calling_convention= callconv; |> @@ -91,15 +94,29 @@ let pop_block_objects = fun st -> | _ -> error "[Translation.E.pop_block_objects] found an ill-formed scope stack." end |>) -val with_block_objects: forall 'a. list (Symbol.sym * (Ctype.qualifiers * Ctype.ctype)) -> elabM 'a -> elabM (list compound_literal_info * 'a) +val cheri_const_alias_map: elabM (map Symbol.sym Symbol.sym) +let cheri_const_alias_map = fun st -> + (st.cheri_const_alias, st) + +val with_block_objects: forall 'a. list (Symbol.sym * (Ctype.qualifiers * Ctype.ctype)) -> elabM 'a -> + elabM (list (Symbol.sym * (Ctype.qualifiers * Ctype.ctype * Symbol.sym)) * list compound_literal_info * 'a) let with_block_objects binds ma = fun st -> + let (new_aliases, cheri_const_alias) = List.foldl (fun (xs_acc, map_acc) (sym, (qs, ty)) -> + (* TODO: fail if sym IN acc *) + if qs.Ctype.const then + let sym' = Symbol.fresh () in + ((sym, (qs, ty, sym')) :: xs_acc, Map.insert sym sym' map_acc) + else + (xs_acc, map_acc) + ) ([], st.cheri_const_alias) binds in let st' = <| st with visible_objects_types= List.foldl (fun acc (sym, qs_ty) -> Map.insert sym qs_ty acc) st.visible_objects_types binds; visible_objects= (List.map fst binds) :: st.visible_objects; compound_literals= []; + cheri_const_alias = cheri_const_alias; |> in let (a, st'') = ma st' in - ((st''.compound_literals, a), <| st'' with + ((new_aliases, st''.compound_literals, a), <| st'' with visible_objects= match st''.visible_objects with | _ :: xs -> xs