diff --git a/Makefile b/Makefile index b7a8c5496..fff0b61de 100644 --- a/Makefile +++ b/Makefile @@ -17,14 +17,10 @@ endif # To enable the printing of commands, use [make Q= ...], Q = @ -# parse the -j flag if present, set jobs to "auto" oterwise -JFLAGVALUE=$(patsubst -j%,%,$(filter -j%,$(MFLAGS))) -JOBS=$(if $(JFLAGVALUE),$(JFLAGVALUE),"auto") - ifdef PROFILING - DUNEFLAGS=--workspace=dune-workspace.profiling -j $(JOBS) + DUNEFLAGS=--workspace=dune-workspace.profiling else - DUNEFLAGS=-j $(JOBS) + DUNEFLAGS= endif .PHONY: normal @@ -85,7 +81,7 @@ cn: prelude-src cheri: prelude-src @echo "[DUNE] cerberus-cheri" - $(Q)./tools/cheribuild_hack.sh "dune build $(DUNEFLAGS) cerberus-cheri.install" + $(Q)dune build $(DUNEFLAGS) cerberus-cheri.install # .PHONY: cerberus-ocaml ocaml @@ -293,7 +289,7 @@ install: cerberus .PHONY: install-cheri install-cheri: @echo "[DUNE] install cerberus-cheri" - $(Q)./tools/cheribuild_hack.sh "dune build -p cerberus-cheri --profile=release -j $(JOBS) @install" + $(Q)dune install cerberus-cheri .PHONY: install_cn install_cn: cn diff --git a/backend/common/pipeline.ml b/backend/common/pipeline.ml index ed91048ef..c8b4d4355 100644 --- a/backend/common/pipeline.ml +++ b/backend/common/pipeline.ml @@ -520,8 +520,10 @@ let print_core (conf, io) ~filename core_file = let core_passes (conf, io) ~filename core_file = (* If using the switch making load() returning unspecified value undefined, then we remove from the Core the code dealing with them. *) + (* This is disabled for CHERI because some of the CHERI_intrinsics can + return an unspecified value *) let core_file = - if Switches.(has_switch SW_strict_reads) then + if Switches.(has_switch SW_strict_reads && not (is_CHERI ())) then Remove_unspecs.rewrite_file core_file else core_file in diff --git a/cerberus-cheri.opam b/cerberus-cheri.opam index 4ea786240..22ffac789 100644 --- a/cerberus-cheri.opam +++ b/cerberus-cheri.opam @@ -46,6 +46,16 @@ depends: [ build: [ ["dune" "subst"] {pinned} - [ make "-j" jobs "install-cheri" ] + ["dune" + "build" + "-p" + name + "--profile=release" + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] ] dev-repo: "git+https://github.com/rems-project/cerberus.git" diff --git a/coq/CheriMemory/CerbSwitches.v b/coq/CheriMemory/CerbSwitches.v index 7beacaf11..a7b3efe58 100644 --- a/coq/CheriMemory/CerbSwitches.v +++ b/coq/CheriMemory/CerbSwitches.v @@ -3,6 +3,6 @@ Require Import CoqSwitches. Module Type CerbSwitchesDefs. - Parameter get_swtiches: unit -> cerb_switches_t. + Parameter get_switches: unit -> cerb_switches_t. End CerbSwitchesDefs. diff --git a/coq/CheriMemory/CheriMemory.v b/coq/CheriMemory/CheriMemory.v index 14dc9bc53..6ca3ebd36 100644 --- a/coq/CheriMemory/CheriMemory.v +++ b/coq/CheriMemory/CheriMemory.v @@ -3,22 +3,18 @@ Require Import Coq.Numbers.BinNums. Require Import Coq.ZArith.Zcompare. Require Import Coq.Floats.PrimFloat. From Coq.Strings Require Import String Ascii HexString. -Require Import Coq.FSets.FMapAVL. -Require Import Coq.Structures.OrderedTypeEx. -Require Coq.Program.Wf. -Require Recdef. Require Import Lia. From ExtLib.Data Require Import List. From ExtLib.Structures Require Import Monad Monads MonadExc MonadState Traversable. From ExtLib.Data.Monads Require Import EitherMonad OptionMonad. -From Coq.Lists Require Import List ListSet. (* after exltlib *) +From Coq.Lists Require Import List. (* after exltlib *) From CheriCaps.Morello Require Import Capabilities. From CheriCaps.Common Require Import Capabilities. -From Common Require Import SimpleError Utils. +From Common Require Import SimpleError Utils ZMap. From Morello Require Import CapabilitiesGS MorelloCapsGS. Require Import Memory_model CoqMem_common ErrorWithState CoqUndefined ErrorWithState CoqLocation CoqSymbol CoqImplementation CoqTags CoqSwitches CerbSwitches CoqAilTypesAux. @@ -33,10 +29,6 @@ Require Import AltBinNotations. Import ListNotations. Import MonadNotation. -Definition debugging : bool := false. - -Module ZMap := FMapAVL.Make(Z_as_OT). - Module CheriMemory (C:CAPABILITY_GS (AddressValue) @@ -60,6 +52,7 @@ Module CheriMemory Definition storage_instance_id : Set := Z. Inductive provenance : Set := + | Prov_disabled : provenance | Prov_none : provenance | Prov_some : storage_instance_id -> provenance | Prov_symbolic : symbolic_storage_instance_id -> provenance @@ -172,6 +165,8 @@ Module CheriMemory size : Z; ty : option CoqCtype.ctype; is_readonly : readonly_status; + is_dynamic : bool ; + is_dead : bool ; taint : allocation_taint }. @@ -190,7 +185,10 @@ Module CheriMemory *) Definition allocation_with_prefix prefix (r : allocation) := - Build_allocation prefix r.(base) r.(size) r.(ty) r.(is_readonly) r.(taint). + Build_allocation prefix r.(base) r.(size) r.(ty) r.(is_readonly) r.(is_dynamic) r.(is_dead) r.(taint). + + Definition allocation_with_dead (r : allocation) := + Build_allocation r.(prefix) r.(base) r.(size) r.(ty) r.(is_readonly) r.(is_dynamic) true r.(taint). Record AbsByte := { @@ -220,9 +218,6 @@ Module CheriMemory next_varargs_id : Z; bytemap : ZMap.t AbsByte; capmeta : ZMap.t (bool* CapGhostState); - dead_allocations : list storage_instance_id; - dynamic_addrs : list C.t; - last_used : option storage_instance_id }. (* @@ -239,37 +234,31 @@ Module CheriMemory next_varargs_id := st.(next_varargs_id); bytemap := st.(bytemap); capmeta := st.(capmeta); - dead_allocations := st.(dead_allocations); - dynamic_addrs := st.(dynamic_addrs); - last_used := st.(last_used); |} *) Definition mem_state := mem_state_r. Definition mem_state_with_bytemap bytemap (r : mem_state) := - Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) r.(allocations) r.(iota_map) r.(funptrmap) r.(varargs) r.(next_varargs_id) bytemap r.(capmeta) r.(dead_allocations) r.(dynamic_addrs) r.(last_used). + Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) r.(allocations) r.(iota_map) r.(funptrmap) r.(varargs) r.(next_varargs_id) bytemap r.(capmeta). Definition mem_state_with_allocations allocations (r : mem_state) := - Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) allocations r.(iota_map) r.(funptrmap) r.(varargs) r.(next_varargs_id) r.(bytemap) r.(capmeta) r.(dead_allocations) r.(dynamic_addrs) r.(last_used). - - Definition mem_state_with_last_used last_used (r : mem_state) := - Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) r.(allocations) r.(iota_map) r.(funptrmap) r.(varargs) r.(next_varargs_id) r.(bytemap) r.(capmeta) r.(dead_allocations) r.(dynamic_addrs) last_used. + Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) allocations r.(iota_map) r.(funptrmap) r.(varargs) r.(next_varargs_id) r.(bytemap) r.(capmeta). Definition mem_state_with_iota_map iota_map (r : mem_state) := - Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) r.(allocations) iota_map r.(funptrmap) r.(varargs) r.(next_varargs_id) r.(bytemap) r.(capmeta) r.(dead_allocations) r.(dynamic_addrs) r.(last_used). + Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) r.(allocations) iota_map r.(funptrmap) r.(varargs) r.(next_varargs_id) r.(bytemap) r.(capmeta). Definition mem_state_with_next_iota next_iota (r : mem_state) := - Build_mem_state_r r.(next_alloc_id) next_iota r.(last_address) r.(allocations) r.(iota_map) r.(funptrmap) r.(varargs) r.(next_varargs_id) r.(bytemap) r.(capmeta) r.(dead_allocations) r.(dynamic_addrs) r.(last_used). + Build_mem_state_r r.(next_alloc_id) next_iota r.(last_address) r.(allocations) r.(iota_map) r.(funptrmap) r.(varargs) r.(next_varargs_id) r.(bytemap) r.(capmeta). Definition mem_state_with_capmeta capmeta (r : mem_state) := - Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) r.(allocations) r.(iota_map) r.(funptrmap) r.(varargs) r.(next_varargs_id) r.(bytemap) capmeta r.(dead_allocations) r.(dynamic_addrs) r.(last_used). + Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) r.(allocations) r.(iota_map) r.(funptrmap) r.(varargs) r.(next_varargs_id) r.(bytemap) capmeta. Definition mem_state_with_funptrmap funptrmap (r : mem_state) := - Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) r.(allocations) r.(iota_map) funptrmap r.(varargs) r.(next_varargs_id) r.(bytemap) r.(capmeta) r.(dead_allocations) r.(dynamic_addrs) r.(last_used). + Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) r.(allocations) r.(iota_map) funptrmap r.(varargs) r.(next_varargs_id) r.(bytemap) r.(capmeta). Definition mem_state_with_varargs_next_varargs_id varargs next_varargs_id (r : mem_state) := - Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) r.(allocations) r.(iota_map) r.(funptrmap) varargs next_varargs_id r.(bytemap) r.(capmeta) r.(dead_allocations) r.(dynamic_addrs) r.(last_used). + Build_mem_state_r r.(next_alloc_id) r.(next_iota) r.(last_address) r.(allocations) r.(iota_map) r.(funptrmap) varargs next_varargs_id r.(bytemap) r.(capmeta). Definition initial_address := AddressValue.of_Z (HexString.to_Z "0xFFFFFFFF"). @@ -289,9 +278,6 @@ Module CheriMemory next_varargs_id := Z0; bytemap := ZMap.empty AbsByte; capmeta := ZMap.empty _; - dead_allocations := nil; - dynamic_addrs := nil; - last_used := None |}. (* Unfortunate names of two consturctors are mirroring ones from @@ -309,10 +295,7 @@ Module CheriMemory Qed. Definition mprint_msg (msg : string) : memM unit := - if debugging then - ret (print_msg msg) - else - ret tt. + ret (print_msg msg). Definition serr2memM {A: Type} (e:serr A): (memM A) := match e with @@ -327,30 +310,6 @@ Module CheriMemory end. Definition fail {A:Type} loc err : memM A := - (* let loc := - match err with - | MerrAccess loc _ _ - | MerrWriteOnReadOnly _ loc - | MerrReadUninit loc - | MerrUndefinedFree loc _ - | MerrUndefinedRealloc loc _ - | MerrFreeNullPtr loc - | MerrArrayShift loc - | MerrIntFromPtr loc => - loc - | MerrOutsideLifetime _ - | MerrInternal _ - | MerrOther _ - | MerrPtrdiff - | MerrPtrFromInt - | MerrPtrComparison - | MerrWIP _ - | MerrVIP _ => - Loc_other "cherimem" - | MerrCHERI loc _ => - loc - end - in *) match undefinedFromMem_error err with | Some ub => raise (Undef0 loc [ub]) @@ -380,6 +339,8 @@ Module CheriMemory Definition footprint := footprint_ind. + Definition cap_to_Z c := AddressValue.to_Z (C.cap_get_value c). + Definition overlapping a b := match a,b with | FP k1 b1 sz1, FP k2 b2 sz2 => @@ -402,7 +363,7 @@ Module CheriMemory let ptraddr_bits := (Z.of_nat C.sizeof_ptraddr) * 8 in let min_v := Z.opp (Z.pow 2 (ptraddr_bits - 1)) in let max_v := Z.sub (Z.pow 2 (ptraddr_bits - 1)) 1 in - if andb (Z.leb n min_v) (Z.leb n max_v) + if Z.leb n min_v && Z.leb n max_v then n else wrapI min_v max_v n. @@ -410,19 +371,10 @@ Module CheriMemory match x with | IV n => n | IC is_signed c => - let n := AddressValue.to_Z (C.cap_get_value c) in + let n := (cap_to_Z c) in if is_signed then unwrap_cap_value n else n end. - Fixpoint zmap_range_init {T} (a0:Z) (n:nat) (step:Z) (v:T) (m:ZMap.t T) : ZMap.t T - := - match n with - | O => m - | S n => - let m := ZMap.add (Z.add a0 (Z.mul (Z.of_nat n) step)) v m in - zmap_range_init a0 n step v m - end. - (* Creare new cap meta for region where all tags are unspecified *) Program Definition init_ghost_tags (addr: AddressValue.t) @@ -460,7 +412,7 @@ Module CheriMemory let a1 := lower_a (Z.pred (Z.add (AddressValue.to_Z addr) size)) in ZMap.mapi (fun (a:Z) '(t, gs) => - if ((negb gs.(tag_unspecified)) && t && Z.geb a a0 && Z.leb a a1)%bool + if negb gs.(tag_unspecified) && t && Z.geb a a0 && Z.leb a a1 then (true, {| tag_unspecified := true; bounds_unspecified := gs.(bounds_unspecified) |}) else (t, gs) @@ -492,9 +444,6 @@ Module CheriMemory bytemap := st.(bytemap); (* tags in newly allocated region are unspecified *) capmeta := init_ghost_tags (AddressValue.of_Z addr) size st.(capmeta); - dead_allocations := st.(dead_allocations); - dynamic_addrs := st.(dynamic_addrs); - last_used := Some alloc_id; |} ;; ret (alloc_id, (AddressValue.of_Z addr)). @@ -690,6 +639,11 @@ Module CheriMemory | FP_invalid c => (funptrmap, c) end. + Definition default_prov (_:unit) := + if CoqSwitches.is_PNVI (SW.get_switches tt) + then Prov_none + else Prov_disabled. + Fixpoint repr (fuel: nat) (funptrmap: ZMap.t (digest * string * C.t)) @@ -707,12 +661,12 @@ Module CheriMemory | MVunspecified ty => sz <- sizeof DEFAULT_FUEL None ty ;; ret (funptrmap, (ghost_tags (AddressValue.of_Z addr) sz capmeta), - (list_init (Z.to_nat sz) (fun _ => absbyte_v Prov_none None None))) + (list_init (Z.to_nat sz) (fun _ => absbyte_v (default_prov tt) None None))) | MVinteger ity (IV n_value) => iss <- option2serr "Could not get int signedness of a type in repr" (is_signed_ity DEFAULT_FUEL ity) ;; sz <- sizeof DEFAULT_FUEL None (CoqCtype.Ctype nil (CoqCtype.Basic (CoqCtype.Integer ity))) ;; bs' <- bytes_of_Z iss (Z.to_nat sz) n_value ;; - let bs := List.map (fun (x : ascii) => absbyte_v Prov_none None (Some x)) bs' in + let bs := List.map (fun (x : ascii) => absbyte_v (default_prov tt) None (Some x)) bs' in ret (funptrmap, (ghost_tags (AddressValue.of_Z addr) (Z.of_nat (List.length bs)) capmeta), bs) | MVinteger ity (IC _ c_value) => '(cb, ct) <- option2serr "int encoding error" (C.encode true c_value) ;; @@ -723,11 +677,11 @@ Module CheriMemory ret (funptrmap, capmeta, (mapi (fun (i_value : nat) (b_value : ascii) => - absbyte_v Prov_none None (Some b_value)) cb)) + absbyte_v (default_prov tt) None (Some b_value)) cb)) | MVfloating fty fval => sz <- sizeof DEFAULT_FUEL None (CoqCtype.Ctype nil (CoqCtype.Basic (CoqCtype.Floating fty))) ;; bs' <- bytes_of_Z true (Z.to_nat sz) (bits_of_float fval) ;; - let bs := List.map (fun (x : ascii) => absbyte_v Prov_none None (Some x)) bs' + let bs := List.map (fun (x : ascii) => absbyte_v (default_prov tt) None (Some x)) bs' in ret (funptrmap, (ghost_tags (AddressValue.of_Z addr) (Z.of_nat (List.length bs)) capmeta), bs) | MVpointer ref_ty (PV prov ptrval_) => @@ -766,7 +720,7 @@ Module CheriMemory mvals (funptrmap, capmeta, addr, nil) ;; ret (funptrmap, capmeta, (List.concat (List.rev bs_s))) | MVstruct tag_sym xs => - let padding_byte _ : AbsByte := absbyte_v Prov_none None None in + let padding_byte _ : AbsByte := absbyte_v (default_prov tt) None None in '(offs, last_off) <- offsetsof DEFAULT_FUEL (TD.tagDefs tt) tag_sym ;; sz <- sizeof DEFAULT_FUEL None (CoqCtype.Ctype nil (CoqCtype.Struct tag_sym)) ;; let final_pad := Z.sub sz last_off in @@ -796,7 +750,7 @@ Module CheriMemory ret (funptrmap', capmeta', (List.app bs (list_init (Nat.sub (Z.to_nat size) (List.length bs)) - (fun _ => absbyte_v Prov_none None None)))) + (fun _ => absbyte_v (default_prov tt) None None)))) end end. @@ -833,7 +787,7 @@ Module CheriMemory (fun '(alloc_id, addr) => (* mprint_msg - ("allocate_object addr=" ++ String.hex_str addr ++ + ("allocate_object addr=" ++ String.hex_str (AddressValue.to_Z addr) ++ ", size=" ++ String.dec_str size_n' ++ ", align=" ++ String.dec_str align_n' ++ ", alloc_id=" ++ String.dec_str alloc_id @@ -841,7 +795,7 @@ Module CheriMemory *) (match init_opt with | None => - let alloc := {| prefix := pref; base:= addr; size:= size_n'; ty:= Some ty; is_readonly:= IsWritable; taint:= Unexposed|} in + let alloc := {| prefix := pref; base:= addr; size:= size_n'; ty:= Some ty; is_dynamic := false; is_dead := false; is_readonly:= IsWritable; taint:= Unexposed|} in update (fun st => {| next_alloc_id := st.(next_alloc_id); @@ -854,9 +808,6 @@ Module CheriMemory next_varargs_id := st.(next_varargs_id); bytemap := st.(bytemap); capmeta := st.(capmeta); - dead_allocations := st.(dead_allocations); - dynamic_addrs := st.(dynamic_addrs); - last_used := st.(last_used); |}) ;; ret false | Some mval => (* here we allocate an object with initiliazer *) let (ro,readonly_status) := @@ -865,7 +816,7 @@ Module CheriMemory | _ => (false,IsWritable) end in - let alloc := {| prefix:= pref; base:= addr; size:= size_n'; ty:= Some ty; is_readonly:= readonly_status; taint:= Unexposed |} in + let alloc := {| prefix:= pref; base:= addr; size:= size_n'; ty:= Some ty; is_dynamic := false; is_dead := false; is_readonly:= readonly_status; taint:= Unexposed |} in st <- get ;; '(funptrmap, capmeta, pre_bs) <- serr2memM (repr DEFAULT_FUEL st.(funptrmap) st.(capmeta) (AddressValue.to_Z addr) mval) ;; @@ -883,28 +834,29 @@ Module CheriMemory ZMap.add addr b acc ) bs st.(bytemap); capmeta := capmeta; - dead_allocations := st.(dead_allocations); - dynamic_addrs := st.(dynamic_addrs); - last_used := st.(last_used); |} ;; ret ro end) >>= - (fun ro => - let c := C.alloc_cap addr (AddressValue.of_Z size_n') in - (* Check here *) - let c := - if ro then - let p := C.cap_get_perms c in - let p := Permissions.perm_clear_store p in - let p := Permissions.perm_clear_store_cap p in - let p := Permissions.perm_clear_store_local_cap p in - C.cap_narrow_perms c p - else c - in - ret (PV (Prov_some alloc_id) (PVconcrete c)) - )). + fun ro => + let c := C.alloc_cap addr (AddressValue.of_Z size_n') in + (* Check here *) + let c := + if ro then + let p := C.cap_get_perms c in + let p := Permissions.perm_clear_store p in + let p := Permissions.perm_clear_store_cap p in + let p := Permissions.perm_clear_store_local_cap p in + C.cap_narrow_perms c p + else c + in + let prov := if CoqSwitches.is_PNVI (SW.get_switches tt) + then Prov_some alloc_id + else Prov_disabled + in + ret (PV prov (PVconcrete c)) + ). Definition allocate_region (tid : thread_id) @@ -921,60 +873,116 @@ Module CheriMemory Z.max align_n (Z.succ (AddressValue.to_Z (AddressValue.bitwise_complement (AddressValue.of_Z mask)))) in allocator size_n' align_n' >>= - (fun '(alloc_id, addr) => - let alloc := - {| prefix := CoqSymbol.PrefMalloc; - base := addr; - size := size_n'; - ty := None; - is_readonly := IsWritable; - taint := Unexposed |} - in - let c_value := C.alloc_cap addr (AddressValue.of_Z size_n') in - update - (fun (st : mem_state) => + fun '(alloc_id, addr) => + let alloc := + {| prefix := CoqSymbol.PrefMalloc; + base := addr; + size := size_n'; + ty := None; + is_dynamic := true ; + is_dead := false ; + is_readonly := IsWritable; + taint := Unexposed |} + in + let c_value := C.alloc_cap addr (AddressValue.of_Z size_n') in + update + (fun (st : mem_state) => + {| + next_alloc_id := st.(next_alloc_id); + next_iota := st.(next_iota); + last_address := st.(last_address) ; + allocations := (ZMap.add alloc_id alloc st.(allocations)); + iota_map := st.(iota_map); + funptrmap := st.(funptrmap); + varargs := st.(varargs); + next_varargs_id := st.(next_varargs_id); + bytemap := st.(bytemap); + capmeta := st.(capmeta); + |}) + ;; + let prov := if CoqSwitches.is_PNVI (SW.get_switches tt) + then Prov_some alloc_id + else Prov_disabled + in + ret (PV prov (PVconcrete c_value) + ). + + Definition cap_is_null (c : C.t) : bool := + Z.eqb (cap_to_Z c) 0. + + (* find first live allocation with given starting addrress *) + Definition find_live_allocation (addr:AddressValue.t) : memM (option (Z*allocation)) := + get >>= fun st => + ret + (ZMap.fold (fun alloc_id alloc acc => + match acc with + | None => + if AddressValue.eqb alloc.(base) addr && negb alloc.(is_dead) + then Some (alloc_id,alloc) + else None + | Some _ => acc + end + ) st.(allocations) None). + + (* private *) + Definition is_dynamic_addr (addr:AddressValue.t) : memM bool := + find_live_allocation addr >>= fun x => + match x with + | None => ret false + | Some (_,alloc) => + ret alloc.(is_dynamic) + end. + + (* + Check if given cap is matches exactly a cap retruned by one of + previous dynamic allocations. + + 0. The allocation must be live (ensured by [find_live_allocation] + 1. The allocation must be dynamic + 2. Bounds must exactly span allocation + 3. Address must be equal to the beginning of allocation + 4. Permissions must be the same as returned by allocator + + TODO: check ghost state? + TODO: assumes that [C.cap_get_value c = fst (C.cap_get_bounds c) ] + *) + Definition cap_match_dyn_allocation c alloc : bool := + let zbounds := Bounds.to_Zs (C.cap_get_bounds c) in + let csize := (snd zbounds) - (fst zbounds) in + + Permissions.eqb (C.cap_get_perms c) Permissions.perm_alloc + && alloc.(is_dynamic) + && AddressValue.eqb alloc.(base) (C.cap_get_value c) + && Z.eqb alloc.(size) csize. + + Definition remove_allocation (alloc_id : Z) : memM unit := + update (fun st => {| next_alloc_id := st.(next_alloc_id); next_iota := st.(next_iota); last_address := st.(last_address) ; - allocations := (ZMap.add alloc_id alloc st.(allocations)); + allocations := ZMap.remove alloc_id st.(allocations); iota_map := st.(iota_map); funptrmap := st.(funptrmap); varargs := st.(varargs); next_varargs_id := st.(next_varargs_id); bytemap := st.(bytemap); capmeta := st.(capmeta); - dead_allocations := st.(dead_allocations); - dynamic_addrs := c_value::st.(dynamic_addrs); - last_used := st.(last_used); - |}) - ;; - ret (PV (Prov_some alloc_id) (PVconcrete c_value) - )). - - Definition cap_is_null (c : C.t) : bool := - Z.eqb (AddressValue.to_Z (C.cap_get_value c)) 0. - - - Definition is_dynamic c : memM bool := - get >>= fun st => - ret (List.existsb (C.eqb c) st.(dynamic_addrs)). - - Definition is_dead (alloc_id : storage_instance_id) : memM bool := - get >>= fun st => - ret (set_mem Z_as_OT.eq_dec alloc_id st.(dead_allocations)). + |}). Definition get_allocation (alloc_id : Z) : memM allocation := get >>= - (fun st => - match ZMap.find alloc_id st.(allocations) with - | Some v => ret v - | None => - fail_noloc (MerrOutsideLifetime - (String.append "CHERI.get_allocation, alloc_id=" - (of_Z alloc_id))) - end - ). + fun st => + match ZMap.find alloc_id st.(allocations) with + | Some v => ret v + | None => + fail_noloc (MerrOutsideLifetime + (String.append "CHERI.get_allocation, alloc_id=" + (of_Z alloc_id))) + end. + + Definition is_dead_allocation (alloc_id : storage_instance_id) : memM bool := + get_allocation alloc_id >>= fun alloc => ret alloc.(is_dead). (* PNVI-ae-udi *) Definition lookup_iota iota := @@ -1013,138 +1021,8 @@ Module CheriMemory next_varargs_id := st.(next_varargs_id); bytemap := st.(bytemap); capmeta := st.(capmeta); - dead_allocations := st.(dead_allocations); - dynamic_addrs := st.(dynamic_addrs); - last_used := st.(last_used); |}) ;; ret alloc_id. - (* zap (make unspecified) any pointer in the memory with provenance matching a - given allocation id *) - Definition zap_pointers {A:Type} (_:storage_instance_id) : memM A := raise (InternalErr "zap_pointers is not supported"). - - Definition kill - (loc : location_ocaml) - (is_dyn : bool) - (ptr : pointer_value) - : memM unit - := - match ptr with - | PV _ (PVfunction _) => - fail loc (MerrOther "attempted to kill with a function pointer") - | PV Prov_none (PVconcrete _) => - fail loc (MerrOther "attempted to kill with a pointer lacking a provenance") - | PV Prov_device (PVconcrete _) => ret tt - | PV (Prov_symbolic iota) (PVconcrete addr) => - if andb - (cap_is_null addr) - (CoqSwitches.has_switch (SW.get_swtiches tt) CoqSwitches.SW_forbid_nullptr_free) - then - fail loc MerrFreeNullPtr - else - let precondition (z : storage_instance_id) := - is_dead z >>= - (fun x => match x with - | true => - ret - (FAIL loc (MerrUndefinedFree Free_dead_allocation)) - | false => - get_allocation z >>= - (fun alloc => - if - AddressValue.eqb - (C.cap_get_value addr) - alloc.(base) - then - ret OK - else - ret - (FAIL loc (MerrUndefinedFree Free_out_of_bound))) - end) - in - (if is_dyn then - (is_dynamic addr) >>= - (fun (b : bool) => - if b then ret tt - else fail loc (MerrUndefinedFree Free_non_matching)) - else - ret tt) ;; - resolve_iota precondition iota >>= - (fun alloc_id => - update (fun st => - {| - next_alloc_id := st.(next_alloc_id); - next_iota := st.(next_iota); - last_address := st.(last_address) ; - allocations := ZMap.remove alloc_id st.(allocations); - iota_map := st.(iota_map); - funptrmap := st.(funptrmap); - varargs := st.(varargs); - next_varargs_id := st.(next_varargs_id); - bytemap := st.(bytemap); - capmeta := st.(capmeta); - dead_allocations := alloc_id :: st.(dead_allocations); - dynamic_addrs := st.(dynamic_addrs); - last_used := Some alloc_id; - |}) - ;; - if CoqSwitches.has_switch (SW.get_swtiches tt) SW_zap_dead_pointers then - zap_pointers alloc_id - else - ret tt) - | PV (Prov_some alloc_id) (PVconcrete addr) => - (if andb - (cap_is_null addr) - (CoqSwitches.has_switch (SW.get_swtiches tt) CoqSwitches.SW_forbid_nullptr_free) - then - fail loc MerrFreeNullPtr - else - if is_dyn then - (* this kill is dynamic one (i.e. free() or friends) *) - is_dynamic addr >>= - fun x => match x with - | false => - fail loc (MerrUndefinedFree Free_non_matching) - | true => ret tt - end - else - ret tt) - ;; - is_dead alloc_id >>= - fun x => match x with - | true => - if is_dyn then - fail loc (MerrUndefinedFree Free_dead_allocation) - else - raise (InternalErr "Concrete: FREE was called on a dead allocation") - | false => - get_allocation alloc_id >>= fun alloc => - if AddressValue.eqb (C.cap_get_value addr) alloc.(base) then - update - (fun st => - {| - next_alloc_id := st.(next_alloc_id); - next_iota := st.(next_iota); - last_address := st.(last_address) ; - allocations := ZMap.remove alloc_id st.(allocations); - iota_map := st.(iota_map); - funptrmap := st.(funptrmap); - varargs := st.(varargs); - next_varargs_id := st.(next_varargs_id); - bytemap := st.(bytemap); - capmeta := st.(capmeta); - dead_allocations := alloc_id :: st.(dead_allocations); - dynamic_addrs := st.(dynamic_addrs); - last_used := Some alloc_id; - |}) ;; - if CoqSwitches.has_switch (SW.get_swtiches tt) SW_zap_dead_pointers then - zap_pointers alloc_id - else - ret tt - else - fail loc (MerrUndefinedFree Free_out_of_bound) - end - end. - Definition is_pointer_algined (a : Z) : bool := let v := IMP.get.(alignof_pointer) in let (_,m) := quomod a v in @@ -1156,12 +1034,6 @@ Module CheriMemory | PV prov ptrval => (prov,ptrval) end. - (** Helper function to split a list at given position. - List.split_at in Lem. - *) - Definition split_at {A:Type} (n:nat) (l:list A) - := (List.firstn n l, List.skipn n l). - Inductive overlap_ind := | NoAlloc: overlap_ind | SingleAlloc: storage_instance_id -> overlap_ind @@ -1227,6 +1099,10 @@ Module CheriMemory raise "TODO(iota) split_bytes 2" | (VALID Prov_none, (Prov_some _) as new_prov), _, _ => ret (VALID new_prov) + | (VALID Prov_disabled, Prov_some _), _, _ => + ret INVALID + | (VALID Prov_disabled, Prov_symbolic _), _, _ => + ret INVALID | (VALID Prov_none, (Prov_symbolic _) as new_prov), _, _ => ret (VALID new_prov) | (prev_acc, _), _, _ => ret prev_acc @@ -1245,10 +1121,10 @@ Module CheriMemory end in ret (prov_acc', (cons b_value.(value) val_acc), offset_acc')) - (List.rev bs) ((VALID Prov_none), nil, (PtrBytes 0)) ;; + (List.rev bs) ((VALID (default_prov tt)), nil, (PtrBytes 0)) ;; let pvalid := match _prov with - | INVALID => Prov_none + | INVALID => Prov_disabled | VALID z_value => z_value end in @@ -1266,10 +1142,12 @@ Module CheriMemory (fun (acc : list storage_instance_id) => fun (b_value : AbsByte) => match b_value.(prov) with - | Prov_none => acc + | Prov_disabled + | Prov_none + | Prov_symbolic _ + | Prov_device + => acc | Prov_some alloc_id => cons alloc_id acc - | Prov_symbolic iota => acc - | Prov_device => acc end) bs nil in match xs with | [] => NoTaint @@ -1289,13 +1167,13 @@ Module CheriMemory (** Convert an arbitrary integer value to unsinged cap value *) Definition wrap_cap_value (n_value : Z) : Z := - if andb (Z.leb n_value (AddressValue.to_Z C.min_ptraddr)) (Z.leb n_value (AddressValue.to_Z C.max_ptraddr)) + if Z.leb n_value (AddressValue.to_Z C.min_ptraddr) && Z.leb n_value (AddressValue.to_Z C.max_ptraddr) then n_value else wrapI (AddressValue.to_Z C.min_ptraddr) (AddressValue.to_Z C.max_ptraddr) n_value. Fixpoint abst (fuel: nat) - (find_overlaping : Z -> overlap_ind) + (find_overlapping : Z -> overlap_ind) (funptrmap : ZMap.t (digest * string * C.t)) (tag_query_f : Z -> (bool* CapGhostState)) (addr : Z) @@ -1307,7 +1185,7 @@ Module CheriMemory | O => raise "abst out of fuel" | S fuel => let '(CoqCtype.Ctype _ ty) := cty in - let self f := abst f find_overlaping funptrmap tag_query_f in + let self f := abst f find_overlapping funptrmap tag_query_f in sz <- sizeof DEFAULT_FUEL None cty ;; sassert (negb (Nat.ltb (List.length bs) (Z.to_nat sz))) "abst, |bs| < sizeof(ty)" ;; let merge_taint (x_value : taint_ind) (y_value : taint_ind) : taint_ind := @@ -1402,7 +1280,7 @@ Module CheriMemory let c_value := C.set_ghost_state c_value gs in match ref_ty with | CoqCtype.Ctype _ (CoqCtype.Function _ _ _) => - let n_value := Z.sub (AddressValue.to_Z (C.cap_get_value c_value)) (AddressValue.to_Z initial_address) in + let n_value := Z.sub (cap_to_Z c_value) (AddressValue.to_Z initial_address) in match ZMap.find n_value funptrmap with | Some (file_dig, name, c') => if C.eqb c_value c' then @@ -1425,9 +1303,9 @@ Module CheriMemory match prov_status with | NotValidPtrProv => match - find_overlaping - (AddressValue.to_Z (C.cap_get_value c_value)) with - | NoAlloc => Prov_none + find_overlapping + (cap_to_Z c_value) with + | NoAlloc => (default_prov tt) | SingleAlloc alloc_id => Prov_some alloc_id | DoubleAlloc alloc_id1 alloc_id2 => Prov_some alloc_id1 @@ -1469,49 +1347,21 @@ Module CheriMemory end end. - (** Checks if memory region starting from [addr] and - of size [sz] fits withing interval \[b1,b2) *) - Definition cap_bounds_check (bounds : Bounds.t) - : Z -> Z -> bool + Definition fetch_bytes + (bytemap : ZMap.t AbsByte) + (base_addr : Z) + (n_bytes : Z) : list AbsByte := - let '(base, limit) := Bounds.to_Zs bounds in - fun (addr : Z) (sz : Z) => - andb (Z.leb base addr) (Z.leb (Z.add addr sz) limit). - - Definition cap_check - (loc : location_ocaml) - (c : C.t) - (offset : Z) - (intent : access_intention) - (sz : Z) - : memM unit := - if (C.get_ghost_state c).(tag_unspecified) then - fail loc (MerrCHERI CheriUndefinedTag) - else - if C.cap_is_valid c then - let addr := - Z.add (AddressValue.to_Z (C.cap_get_value c)) offset in - let pcheck := - match intent with - | ReadIntent => - Permissions.has_load_perm - | WriteIntent => - Permissions.has_store_perm - | CallIntent => - Permissions.has_execute_perm - end in - if pcheck (C.cap_get_perms c) then - let limit := Z.add addr sz in - if C.cap_bounds_check c (Bounds.of_Zs (addr, sz)) - then ret tt - else - fail loc - (MerrCHERI (CheriBoundsErr (C.cap_get_bounds c, AddressValue.of_Z addr, (Z.to_nat sz)))) - else - fail loc (MerrCHERI CheriMerrInsufficientPermissions) - else - fail loc - (MerrCHERI CheriMerrInvalidCap). + List.map + (fun (addr : Z.t) => + match ZMap.find addr bytemap with + | Some b_value => b_value + | None => absbyte_v (default_prov tt) None None + end) + (list_init (Z.to_nat n_bytes) + (fun (i : nat) => + let offset := Z.of_nat i in + Z.add base_addr offset)). Fixpoint mem_value_strip_err (loc : location_ocaml) @@ -1540,26 +1390,12 @@ Module CheriMemory | MVErr err => fail loc err end. - Definition fetch_bytes - (bytemap : ZMap.t AbsByte) - (base_addr : Z) - (n_bytes : Z) : list AbsByte - := - List.map - (fun (addr : Z.t) => - match ZMap.find addr bytemap with - | Some b_value => b_value - | None => absbyte_v Prov_none None None - end) - (list_init (Z.to_nat n_bytes) - (fun (i : nat) => - let offset := Z.of_nat i in - Z.add base_addr offset)). - - Definition find_overlaping st addr : overlap_ind + Definition find_overlapping_st st addr : overlap_ind := let (require_exposed, allow_one_past) := - match CoqSwitches.has_switch_pred (SW.get_swtiches tt) (fun x => match x with SW_PNVI _ => true | _ => false end) with + match CoqSwitches.has_switch_pred (SW.get_switches tt) + (fun x => match x with SW_PNVI _ => true | _ => false end) + with | Some (CoqSwitches.SW_PNVI variant) => match variant with | PLAIN => (false, false) @@ -1572,19 +1408,21 @@ Module CheriMemory in ZMap.fold (fun alloc_id alloc acc => let new_opt := - if negb (mem alloc_id st.(dead_allocations)) - && Z.leb (AddressValue.to_Z alloc.(base)) addr && Z.ltb addr (Z.add (AddressValue.to_Z alloc.(base)) alloc.(size)) then - (* PNVI-ae, PNVI-ae-udi *) - if require_exposed && (negb (allocation_taint_eqb alloc.(taint) Exposed)) - then None - else Some alloc_id - else if allow_one_past then - (* PNVI-ae-udi *) - if Z.eqb addr (Z.add (AddressValue.to_Z alloc.(base)) alloc.(size)) - && negb (require_exposed && (negb (allocation_taint_eqb alloc.(taint) Exposed))) - then Some alloc_id - else None - else None + if alloc.(is_dead) + then None + else if Z.leb (AddressValue.to_Z alloc.(base)) addr && Z.ltb addr (Z.add (AddressValue.to_Z alloc.(base)) alloc.(size)) + then + (* PNVI-ae, PNVI-ae-udi *) + if require_exposed && (negb (allocation_taint_eqb alloc.(taint) Exposed)) + then None + else Some alloc_id + else if allow_one_past then + (* PNVI-ae-udi *) + if Z.eqb addr (Z.add (AddressValue.to_Z alloc.(base)) alloc.(size)) + && negb (require_exposed && (negb (allocation_taint_eqb alloc.(taint) Exposed))) + then Some alloc_id + else None + else None in match acc, new_opt with | _, None => acc @@ -1594,28 +1432,235 @@ Module CheriMemory end ) st.(allocations) NoAlloc. + Definition find_overlapping addr : memM overlap_ind + := get >>= fun st => ret (find_overlapping_st st addr). - (* TODO: see if could be generalized and moved to Utils.v. *) - (** [update key f m] returns a map containing the same bindings as - [m], except for the binding of [key]. Depending on the value of [y] - where [y] is [f (find_opt key m)], the binding of [key] is added, - removed or updated. If [y] is [None], the binding is removed if it - exists; otherwise, if [y] is [Some z] then key is associated to [z] - in the resulting map. *) - Definition zmap_update - {A:Type} - (key: Z) - (f: option A -> option A) - (m: ZMap.t A) - : (ZMap.t A) + (* If pointer stored at [addr] with meta information [meta] has it's + base within given [base] and [limit] region, revoke it by returning + new meta. + *) + Definition maybe_revoke_pointer + (alloc_base alloc_limit: Z) + (st: mem_state) + (addr: Z) + (meta: (bool*CapGhostState)) + : + memM (bool* CapGhostState) + := + (* mprint_msg ("maybe_revoke_pointer " ++ String.hex_str addr) ;; *) + if negb (fst meta) + then ret meta (* the pointer is already untagged *) + else + let bs := fetch_bytes st.(bytemap) addr IMP.get.(sizeof_pointer) in + '(_, mval, _) <- + serr2memM (abst DEFAULT_FUEL (fun _ => NoAlloc) st.(funptrmap) (fun _ => meta) addr + (CoqCtype.mk_ctype_pointer CoqCtype.no_qualifiers CoqCtype.void) bs) + ;; + match mval with + | MVEpointer _ (PV _ (PVconcrete c)) => + let '(t, gs) := meta in + let ptr_base := fst (Bounds.to_Zs (C.cap_get_bounds c)) in + if Z.leb alloc_base ptr_base && Z.ltb ptr_base alloc_limit + then ret (false, {| tag_unspecified := false; bounds_unspecified := gs.(bounds_unspecified) |}) + else ret meta (* outside allocation. leave unchanged *) + | MVEunspecified _ => raise (InternalErr "unexpected unspec.") + | _ => raise (InternalErr "unexpected abst return value. Expecting concrete pointer.") + end. + + (* revoke (clear tag) any pointer in the memory pointing within the + bounds of given dynamic allocation. + *) + Definition revoke_pointers alloc : memM unit + := + if alloc.(is_dynamic) + then + let base := AddressValue.to_Z alloc.(base) in + let limit := base + alloc.(size) in + (* mprint_msg ("revoke_pointers " ++ (String.hex_str base) ++ " - " ++ (String.hex_str limit)) ;; *) + get >>= + (fun st => + zmap_mmapi + (maybe_revoke_pointer base limit st) + st.(capmeta) + ) + >>= + (fun newmeta => update (fun st => mem_state_with_capmeta newmeta st)) + ;; ret tt + else + ret tt. (* allocation is not dynamic *) + + Definition kill + (loc : location_ocaml) + (is_dyn : bool) + (ptr : pointer_value) + : memM unit := - let y := f (ZMap.find key m) in - let m' := ZMap.remove key m in (* could be optimized, as removal may be unecessary in some cases *) - match y with - | None => m' - | Some z => ZMap.add key z m' + + let precond c alloc alloc_id := + if is_dyn && negb (cap_match_dyn_allocation c alloc) + then fail loc (MerrUndefinedFree Free_non_matching) + else + if is_dyn && CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_revocation INSTANT) + then revoke_pointers alloc ;; remove_allocation alloc_id + else ret tt + in + + let update_allocations alloc alloc_id all_allocs := + if is_dyn && CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_revocation CORNUCOPIA) + then zmap_update_element alloc_id (allocation_with_dead alloc) all_allocs + else ZMap.remove alloc_id all_allocs + in + + match ptr with + | PV _ (PVfunction _) => + fail loc (MerrOther "attempted to kill with a function pointer") + | PV Prov_none (PVconcrete c) => + fail loc (MerrOther "attempted to kill with a pointer lacking a provenance") + | PV Prov_disabled (PVconcrete c) => + if cap_is_null c + && CoqSwitches.has_switch (SW.get_switches tt) CoqSwitches.SW_forbid_nullptr_free + then fail loc MerrFreeNullPtr + else + find_live_allocation (C.cap_get_value c) >>= + fun x => + match x with + | None => fail loc + (if is_dyn + then (MerrUndefinedFree Free_non_matching) + else (MerrOther "attempted to kill with a pointer not matching any live allocation")) + | Some (alloc_id,alloc) => + precond c alloc alloc_id ;; + update + (fun st => + {| + next_alloc_id := st.(next_alloc_id); + next_iota := st.(next_iota); + last_address := st.(last_address) ; + allocations := update_allocations alloc + alloc_id + st.(allocations); + iota_map := st.(iota_map); + funptrmap := st.(funptrmap); + varargs := st.(varargs); + next_varargs_id := st.(next_varargs_id); + bytemap := st.(bytemap); + capmeta := st.(capmeta); + |}) + end + | PV Prov_device (PVconcrete _) => ret tt + | PV (Prov_symbolic iota) (PVconcrete c) => + if cap_is_null c && CoqSwitches.has_switch (SW.get_switches tt) CoqSwitches.SW_forbid_nullptr_free + then fail loc MerrFreeNullPtr + else + let precondition z := + get_allocation z >>= + fun alloc => + ret + (if alloc.(is_dead) + then (FAIL loc (MerrUndefinedFree Free_dead_allocation)) + else if AddressValue.eqb (C.cap_get_value c) alloc.(base) + then OK + else FAIL loc (MerrUndefinedFree Free_out_of_bound)) + in + resolve_iota precondition iota >>= + (fun alloc_id => + get_allocation alloc_id >>= + (fun alloc => + precond c alloc alloc_id ;; + update (fun st => + {| + next_alloc_id := st.(next_alloc_id); + next_iota := st.(next_iota); + last_address := st.(last_address) ; + allocations := update_allocations alloc + alloc_id + st.(allocations) ; + iota_map := st.(iota_map); + funptrmap := st.(funptrmap); + varargs := st.(varargs); + next_varargs_id := st.(next_varargs_id); + bytemap := st.(bytemap); + capmeta := st.(capmeta); + |}) + )) + | PV (Prov_some alloc_id) (PVconcrete c) => + if cap_is_null c + && CoqSwitches.has_switch (SW.get_switches tt) CoqSwitches.SW_forbid_nullptr_free + then fail loc MerrFreeNullPtr + else + get_allocation alloc_id >>= fun alloc => + if alloc.(is_dead) then + if is_dyn + then fail loc (MerrUndefinedFree Free_dead_allocation) + else raise (InternalErr "Concrete: FREE was called on a dead allocation") + else + if is_dyn && negb (cap_match_dyn_allocation c alloc) + then fail loc (MerrUndefinedFree Free_non_matching) + else + precond c alloc alloc_id ;; + update + (fun st => + {| + next_alloc_id := st.(next_alloc_id); + next_iota := st.(next_iota); + last_address := st.(last_address) ; + allocations := update_allocations alloc + alloc_id + st.(allocations); + iota_map := st.(iota_map); + funptrmap := st.(funptrmap); + varargs := st.(varargs); + next_varargs_id := st.(next_varargs_id); + bytemap := st.(bytemap); + capmeta := st.(capmeta); + |}) end. + + (** Checks if memory region starting from [addr] and + of size [sz] fits withing interval \[b1,b2) *) + Definition cap_bounds_check (bounds : Bounds.t) + : Z -> Z -> bool + := + let '(base, limit) := Bounds.to_Zs bounds in + fun (addr : Z) (sz : Z) => + Z.leb base addr && Z.leb (Z.add addr sz) limit. + + Definition cap_check + (loc : location_ocaml) + (c : C.t) + (offset : Z) + (intent : access_intention) + (sz : Z) + : memM unit := + if (C.get_ghost_state c).(tag_unspecified) then + fail loc (MerrCHERI CheriUndefinedTag) + else + if C.cap_is_valid c then + let addr := + Z.add (cap_to_Z c) offset in + let pcheck := + match intent with + | ReadIntent => + Permissions.has_load_perm + | WriteIntent => + Permissions.has_store_perm + | CallIntent => + Permissions.has_execute_perm + end in + if pcheck (C.cap_get_perms c) then + let limit := Z.add addr sz in + if C.cap_bounds_check c (Bounds.of_Zs (addr, sz)) + then ret tt + else + fail loc + (MerrCHERI (CheriBoundsErr (C.cap_get_bounds c, AddressValue.of_Z addr, (Z.to_nat sz)))) + else + fail loc (MerrCHERI CheriMerrInsufficientPermissions) + else + fail loc + (MerrCHERI CheriMerrInvalidCap). + Definition expose_allocation (alloc_id : Z) : memM unit := update (fun (st: mem_state) => @@ -1629,6 +1674,8 @@ Module CheriMemory base := alloc.(base); size := alloc.(size); ty := alloc.(ty); + is_dynamic := alloc.(is_dynamic); + is_dead := alloc.(is_dead); is_readonly := alloc.(is_readonly); taint := Exposed |} @@ -1653,6 +1700,8 @@ Module CheriMemory base := alloc.(base); size := alloc.(size); ty := alloc.(ty); + is_dynamic := alloc.(is_dynamic); + is_dead := alloc.(is_dead); is_readonly := alloc.(is_readonly); taint := Exposed |} @@ -1671,11 +1720,10 @@ Module CheriMemory get_allocation alloc_id >>= (fun (alloc : allocation) => ret - (andb - (Z.leb (AddressValue.to_Z alloc.(base)) addr) - (Z.leb + (Z.leb (AddressValue.to_Z alloc.(base)) addr + && Z.leb (Z.add addr sz) - (Z.add (AddressValue.to_Z alloc.(base)) alloc.(size))))). + (Z.add (AddressValue.to_Z alloc.(base)) alloc.(size)))). Definition device_ranges : list (AddressValue.t * AddressValue.t) := [ (AddressValue.of_Z 0x40000000, AddressValue.of_Z 0x40000004) @@ -1687,12 +1735,10 @@ Module CheriMemory ret (List.existsb (fun '(min, max) => - andb - (Z.leb (AddressValue.to_Z min) addr) - (Z.leb (Z.add addr sz) (AddressValue.to_Z max))) + Z.leb (AddressValue.to_Z min) addr + && Z.leb (Z.add addr sz) (AddressValue.to_Z max)) device_ranges). - Definition is_atomic_member_access (alloc_id : Z.t) (lvalue_ty : CoqCtype.ctype) @@ -1756,23 +1802,19 @@ Module CheriMemory bounds_unspecified := false |}) in '(taint, mval, bs') <- - serr2memM (abst DEFAULT_FUEL (find_overlaping st) st.(funptrmap) tag_query addr ty bs) + serr2memM (abst DEFAULT_FUEL (find_overlapping_st st) st.(funptrmap) tag_query addr ty bs) ;; mem_value_strip_err loc mval >>= (fun (mval : mem_value) => - (if orb - (CoqSwitches.has_switch (SW.get_swtiches tt) (CoqSwitches.SW_PNVI AE)) - (CoqSwitches.has_switch (SW.get_swtiches tt) (CoqSwitches.SW_PNVI AE_UDI)) + (if CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_PNVI AE) + || CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_PNVI AE_UDI) then expose_allocations taint else ret tt) ;; - (update (fun (st : mem_state) => - mem_state_with_last_used alloc_id_opt st)) - ;; sz <- serr2memM (sizeof DEFAULT_FUEL None ty) ;; let fp := FP Read (AddressValue.of_Z addr) sz in match bs' with | [] => - if CoqSwitches.has_switch (SW.get_swtiches tt) CoqSwitches.SW_strict_reads + if CoqSwitches.has_switch (SW.get_switches tt) CoqSwitches.SW_strict_reads then match mval with | MVunspecified _ => @@ -1792,19 +1834,56 @@ Module CheriMemory : memM (footprint * mem_value) := cap_check loc c 0 ReadIntent sz ;; - do_load alloc_id_opt (AddressValue.to_Z (C.cap_get_value c)) sz + do_load alloc_id_opt (cap_to_Z c) sz + in + let load_concrete (alloc_id:storage_instance_id) (c:C.t) : memM (footprint * mem_value) := + if cap_is_null c then + fail loc (MerrAccess LoadAccess NullPtr) + else + (is_dead_allocation alloc_id) >>= + (fun x => + match x with + | true => fail loc (MerrAccess LoadAccess DeadPtr) + | false => ret tt + end) + ;; + is_within_bound alloc_id ty + (cap_to_Z c) >>= + (fun (function_parameter : bool) => + match function_parameter with + | false => + fail loc (MerrAccess LoadAccess OutOfBoundPtr) + | true => + is_atomic_member_access alloc_id ty + (cap_to_Z c) >>= + (fun (function_parameter : bool) => + match function_parameter with + | true => + fail loc (MerrAccess LoadAccess AtomicMemberof) + | false => + sz <- serr2memM (sizeof DEFAULT_FUEL None ty) ;; + do_load_cap (Some alloc_id) c sz + end) + end) in match prov, ptrval_ with | _, PVfunction _ => fail loc (MerrAccess LoadAccess FunctionPtr) - | Prov_none, _ => + | Prov_none, PVconcrete c => fail loc (MerrAccess LoadAccess OutOfBoundPtr) + | Prov_disabled, PVconcrete c => + find_overlapping (cap_to_Z c) >>= fun x => + match x with + | NoAlloc => fail loc (MerrAccess LoadAccess OutOfBoundPtr) + | DoubleAlloc _ _ => fail loc (MerrInternal "DoubleAlloc without PNVI") + | SingleAlloc alloc_id => load_concrete alloc_id c + end | Prov_device, PVconcrete c => if cap_is_null c then fail loc (MerrAccess LoadAccess NullPtr) else sz <- serr2memM (sizeof DEFAULT_FUEL None ty) ;; - is_within_device ty (AddressValue.to_Z (C.cap_get_value c)) >>= + is_within_device ty (cap_to_Z c) >>= (fun (function_parameter : bool) => match function_parameter with | false => @@ -1821,19 +1900,19 @@ Module CheriMemory else let precondition (z_value : storage_instance_id) : memM merr := - is_dead z_value >>= + is_dead_allocation z_value >>= (fun (function_parameter : bool) => if function_parameter then ret (FAIL loc (MerrAccess LoadAccess DeadPtr)) else - is_within_bound z_value ty (AddressValue.to_Z (C.cap_get_value addr)) >>= + is_within_bound z_value ty (cap_to_Z addr) >>= (fun (function_parameter : bool) => match function_parameter with | false => ret (FAIL loc (MerrAccess LoadAccess OutOfBoundPtr)) | true => is_atomic_member_access z_value ty - (AddressValue.to_Z (C.cap_get_value addr)) >>= + (cap_to_Z addr) >>= (fun (function_parameter : bool) => match function_parameter with | true => @@ -1846,36 +1925,8 @@ Module CheriMemory resolve_iota precondition iota >>= (fun (alloc_id : storage_instance_id) => do_load_cap (Some alloc_id) addr sz) - | Prov_some alloc_id, PVconcrete addr => - if cap_is_null addr then - fail loc (MerrAccess LoadAccess NullPtr) - else - (is_dead alloc_id) >>= - (fun (function_parameter : bool) => - match function_parameter with - | true => - fail loc (MerrAccess LoadAccess DeadPtr) - | false => ret tt - end) - ;; - is_within_bound alloc_id ty - (AddressValue.to_Z (C.cap_get_value addr)) >>= - (fun (function_parameter : bool) => - match function_parameter with - | false => - fail loc (MerrAccess LoadAccess OutOfBoundPtr) - | true => - is_atomic_member_access alloc_id ty - (AddressValue.to_Z (C.cap_get_value addr)) >>= - (fun (function_parameter : bool) => - match function_parameter with - | true => - fail loc (MerrAccess LoadAccess AtomicMemberof) - | false => - sz <- serr2memM (sizeof DEFAULT_FUEL None ty) ;; - do_load_cap (Some alloc_id) addr sz - end) - end) + | Prov_some alloc_id, PVconcrete c => + load_concrete alloc_id c end. Fixpoint typeof (mval : mem_value) @@ -1908,7 +1959,6 @@ Module CheriMemory : memM footprint := let '(prov,ptrval_) := break_PV ptr in - cond <- serr2memM ( mt <- typeof mval ;; CoqCtype.ctypeEqual DEFAULT_FUEL (CoqCtype.unatomic cty) @@ -1924,7 +1974,7 @@ Module CheriMemory := nsz <- serr2memM (sizeof DEFAULT_FUEL None cty) ;; cap_check loc c_value 0 WriteIntent nsz ;; - let addr := AddressValue.to_Z (C.cap_get_value c_value) in + let addr := (cap_to_Z c_value) in st <- get ;; '(funptrmap, capmeta, pre_bs) <- @@ -1952,38 +2002,98 @@ Module CheriMemory next_varargs_id := st.(next_varargs_id); bytemap := bytemap; capmeta := capmeta; - dead_allocations := st.(dead_allocations); - dynamic_addrs := st.(dynamic_addrs); - last_used := alloc_id_opt; |} ;; ret (FP Write (AddressValue.of_Z addr) nsz) in + let store_concrete alloc_id c := + if cap_is_null c then + fail loc (MerrAccess StoreAccess NullPtr) + else + is_within_bound alloc_id cty (cap_to_Z c) + >>= + (fun (x : bool) => + match x with + | false => + fail loc (MerrAccess StoreAccess OutOfBoundPtr) + | true + => + get_allocation alloc_id >>= + (fun (alloc : allocation) => + match alloc.(is_readonly) with + | IsReadOnly ro_kind => + fail loc (MerrWriteOnReadOnly ro_kind) + | IsWritable => + is_atomic_member_access alloc_id cty + (cap_to_Z c) >>= + (fun (x : bool) => + match x with + | true => + fail loc + (MerrAccess LoadAccess AtomicMemberof) + | false => + do_store_cap (Some alloc_id) c >>= + (fun (fp : footprint) => + if is_locking then + update + (fun (st : mem_state) => + mem_state_with_allocations + (zmap_update + alloc_id + (fun (x:option allocation) => + match x with + | Some a => + Some {| + prefix := a.(prefix) ; + base := a.(base) ; + size := a.(size) ; + ty := a.(ty) ; + is_dynamic := a.(is_dynamic) ; + is_dead := a.(is_dead) ; + is_readonly := IsReadOnly ReadonlyConstQualified; + taint := a.(taint) ; + |} + | None => None + end) st.(allocations)) + st) + ;; + ret fp + else + ret fp) + end) + end) + end) + in + match prov, ptrval_ with | _, PVfunction _ => fail loc (MerrAccess StoreAccess FunctionPtr) - | Prov_none, _ => - fail loc - (MerrAccess - StoreAccess - OutOfBoundPtr) - | Prov_device, PVconcrete addr => - if cap_is_null addr then + | Prov_none, PVconcrete c => + fail loc (MerrAccess StoreAccess OutOfBoundPtr) + | Prov_disabled, PVconcrete c => + find_overlapping (cap_to_Z c) >>= fun x => + match x with + | NoAlloc => fail loc (MerrAccess StoreAccess OutOfBoundPtr) + | DoubleAlloc _ _ => fail loc (MerrInternal "DoubleAlloc without PNVI") + | SingleAlloc alloc_id => store_concrete alloc_id c + end + | Prov_device, PVconcrete c => + if cap_is_null c then fail loc (MerrAccess StoreAccess NullPtr) else - is_within_device cty (AddressValue.to_Z (C.cap_get_value addr)) >>= + is_within_device cty (cap_to_Z c) >>= (fun (x : bool) => if x - then do_store_cap None addr + then do_store_cap None c else fail loc (MerrAccess StoreAccess OutOfBoundPtr)) - | Prov_symbolic iota, PVconcrete addr => - if cap_is_null addr then + | Prov_symbolic iota, PVconcrete c => + if cap_is_null c then fail loc (MerrAccess StoreAccess @@ -1991,7 +2101,7 @@ Module CheriMemory else let precondition (z_value : Z) : memM merr := - is_within_bound z_value cty (AddressValue.to_Z (C.cap_get_value addr)) >>= + is_within_bound z_value cty (cap_to_Z c) >>= (fun (x : bool) => match x with | false => @@ -2007,7 +2117,7 @@ Module CheriMemory ro_kind)) | IsWritable => is_atomic_member_access z_value cty - (AddressValue.to_Z (C.cap_get_value addr)) + (cap_to_Z c) >>= (fun (x : bool) => if x @@ -2021,7 +2131,7 @@ Module CheriMemory in resolve_iota precondition iota >>= (fun (alloc_id : storage_instance_id) => - do_store_cap (Some alloc_id) addr >>= + do_store_cap (Some alloc_id) c >>= (fun (fp : footprint) => (if is_locking then update @@ -2033,12 +2143,14 @@ Module CheriMemory | Some a => Some {| - prefix := a.(prefix) ; - base := a.(base) ; - size := a.(size) ; - ty := a.(ty) ; + prefix := a.(prefix) ; + base := a.(base) ; + size := a.(size) ; + ty := a.(ty) ; + is_dynamic := a.(is_dynamic) ; + is_dead := a.(is_dead) ; is_readonly := IsReadOnly ReadonlyConstQualified; - taint := a.(taint) ; + taint := a.(taint) ; |} | None => None end) st.(allocations)) @@ -2047,6 +2159,9 @@ Module CheriMemory ret tt) ;; ret fp)) + | Prov_some alloc_id, PVconcrete c + => store_concrete alloc_id c +(* | Prov_some alloc_id, PVconcrete addr => if cap_is_null addr then @@ -2103,15 +2218,16 @@ Module CheriMemory end) end) end) +*) end. Definition null_ptrval (_:CoqCtype.ctype) : pointer_value := - PV Prov_none (PVconcrete (C.cap_c0 tt)). + PV (default_prov tt) (PVconcrete (C.cap_c0 tt)). Definition fun_ptrval (sym : CoqSymbol.sym) : serr pointer_value := - ret (PV Prov_none (PVfunction (FP_valid sym))). + ret (PV (default_prov tt) (PVfunction (FP_valid sym))). Definition concrete_ptrval : Z -> AddressValue.t -> serr pointer_value := fun _ _ => @@ -2175,7 +2291,7 @@ Module CheriMemory | PVfunction (FP_valid sym) => Some sym | PVfunction (FP_invalid c) | PVconcrete c => - let n := (Z.sub (AddressValue.to_Z (C.cap_get_value c)) (AddressValue.to_Z initial_address)) in + let n := (Z.sub (cap_to_Z c) (AddressValue.to_Z initial_address)) in match ZMap.find n st.(funptrmap) with | Some (file_dig, name, _) => Some (CoqSymbol.Symbol file_dig n (SD_Id name)) @@ -2200,7 +2316,7 @@ Module CheriMemory get >>= (fun (st : mem_state) => let n_value := - Z.sub (AddressValue.to_Z (C.cap_get_value c_value)) (AddressValue.to_Z initial_address) + Z.sub (cap_to_Z c_value) (AddressValue.to_Z initial_address) in match ZMap.find n_value st.(funptrmap) with | Some (file_dig, name, _) => @@ -2231,9 +2347,9 @@ Module CheriMemory let '(prov2, ptrval_2) := break_PV ptr2 in match ptrval_1, ptrval_2 with | PVconcrete addr1, PVconcrete addr2 => - if orb (cap_is_null addr1) (cap_is_null addr2) then + if cap_is_null addr1 || cap_is_null addr2 then fail loc (MerrWIP "lt_ptrval ==> one null pointer") - else if CoqSwitches.has_switch (SW.get_swtiches tt) CoqSwitches.SW_strict_pointer_relationals then + else if CoqSwitches.has_switch (SW.get_switches tt) CoqSwitches.SW_strict_pointer_relationals then match prov1, prov2, (match prov1, prov2 with @@ -2256,6 +2372,11 @@ Module CheriMemory | _, _ => fail loc (MerrWIP "lt_ptrval") end. + + Definition is_strict_pointer_arith (_:unit) := + CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_pointer_arith STRICT) + || negb (CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_pointer_arith PERMISSIVE)). + Definition gt_ptrval (loc : location_ocaml) (ptr1 ptr2 : pointer_value) : memM bool @@ -2264,9 +2385,9 @@ Module CheriMemory let '(prov2, ptrval_2) := break_PV ptr2 in match ptrval_1, ptrval_2 with | PVconcrete addr1, PVconcrete addr2 => - if orb (cap_is_null addr1) (cap_is_null addr2) then + if cap_is_null addr1 || cap_is_null addr2 then fail loc (MerrWIP "gt_ptrval ==> one null pointer") - else if CoqSwitches.has_switch (SW.get_swtiches tt) CoqSwitches.SW_strict_pointer_relationals then + else if CoqSwitches.has_switch (SW.get_switches tt) CoqSwitches.SW_strict_pointer_relationals then match prov1, prov2, (match prov1, prov2 with @@ -2297,9 +2418,10 @@ Module CheriMemory let '(prov2, ptrval_2) := break_PV ptr2 in match ptrval_1, ptrval_2 with | PVconcrete addr1, PVconcrete addr2 => - if orb (cap_is_null addr1) (cap_is_null addr2) then - fail loc (MerrWIP "le_ptrval ==> one null pointer") - else if CoqSwitches.has_switch (SW.get_swtiches tt) CoqSwitches.SW_strict_pointer_relationals then + if cap_is_null addr1 || cap_is_null addr2 + then fail loc (MerrWIP "le_ptrval ==> one null pointer") + else + if CoqSwitches.has_switch (SW.get_switches tt) CoqSwitches.SW_strict_pointer_relationals then match prov1, prov2, (match prov1, prov2 with @@ -2332,9 +2454,9 @@ Module CheriMemory let '(prov2, ptrval_2) := break_PV ptr2 in match ptrval_1, ptrval_2 with | PVconcrete addr1, PVconcrete addr2 => - if orb (cap_is_null addr1) (cap_is_null addr2) then + if cap_is_null addr1 || cap_is_null addr2 then fail loc (MerrWIP "ge_ptrval ==> one null pointer") - else if CoqSwitches.has_switch (SW.get_swtiches tt) CoqSwitches.SW_strict_pointer_relationals then + else if CoqSwitches.has_switch (SW.get_switches tt) CoqSwitches.SW_strict_pointer_relationals then match prov1, prov2, (match prov1, prov2 with @@ -2383,11 +2505,11 @@ Module CheriMemory let error_postcond := fail loc MerrPtrdiff in - if CoqSwitches.has_switch (SW.get_swtiches tt) (CoqSwitches.SW_pointer_arith PERMISSIVE) + if CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_pointer_arith PERMISSIVE) then match ptrval1, ptrval2 with | PV _ (PVconcrete addr1), PV _ (PVconcrete addr2) => - valid_postcond (AddressValue.to_Z (C.cap_get_value addr1)) (AddressValue.to_Z (C.cap_get_value addr2)) + valid_postcond (cap_to_Z addr1) (cap_to_Z addr2) | _, _=> error_postcond end else @@ -2397,9 +2519,9 @@ Module CheriMemory if Z.eqb alloc_id1 alloc_id2 then get_allocation alloc_id1 >>= (fun (alloc : allocation) => - if precond alloc (AddressValue.to_Z (C.cap_get_value addr1)) (AddressValue.to_Z (C.cap_get_value addr2)) + if precond alloc (cap_to_Z addr1) (cap_to_Z addr2) then - valid_postcond (AddressValue.to_Z (C.cap_get_value addr1)) (AddressValue.to_Z (C.cap_get_value addr2)) + valid_postcond (cap_to_Z addr1) (cap_to_Z addr2) else error_postcond) else @@ -2417,24 +2539,24 @@ Module CheriMemory (fun (alloc : allocation) => if precond alloc - (AddressValue.to_Z (C.cap_get_value addr1)) - (AddressValue.to_Z (C.cap_get_value addr2)) + (cap_to_Z addr1) + (cap_to_Z addr2) then valid_postcond - (AddressValue.to_Z (C.cap_get_value addr1)) - (AddressValue.to_Z (C.cap_get_value addr2)) + (cap_to_Z addr1) + (cap_to_Z addr2) else error_postcond) else error_postcond | inr (alloc_id1, alloc_id2) => - if orb (Z.eqb alloc_id1 alloc_id') (Z.eqb alloc_id2 alloc_id') + if Z.eqb alloc_id1 alloc_id' || Z.eqb alloc_id2 alloc_id' then get_allocation alloc_id' >>= (fun (alloc : allocation) => if precond alloc - (AddressValue.to_Z (C.cap_get_value addr1)) - (AddressValue.to_Z (C.cap_get_value addr2)) + (cap_to_Z addr1) + (cap_to_Z addr2) then (update (fun (st : mem_state) => @@ -2443,8 +2565,8 @@ Module CheriMemory st.(iota_map)) st)) ;; (valid_postcond - (AddressValue.to_Z (C.cap_get_value addr1)) - (AddressValue.to_Z (C.cap_get_value addr2))) + (cap_to_Z addr1) + (cap_to_Z addr2)) else error_postcond) else @@ -2488,14 +2610,14 @@ Module CheriMemory st.(iota_map))) st) ;; valid_postcond - (AddressValue.to_Z (C.cap_get_value addr1)) - (AddressValue.to_Z (C.cap_get_value addr2)) + (cap_to_Z addr1) + (cap_to_Z addr2) | DoubleAlloc alloc_id1 alloc_id2 => match C.value_compare addr1 addr2 with | Eq => valid_postcond - (AddressValue.to_Z (C.cap_get_value addr1)) - (AddressValue.to_Z (C.cap_get_value addr2)) + (cap_to_Z addr1) + (cap_to_Z addr2) | _ => fail loc (MerrOther @@ -2603,17 +2725,21 @@ Module CheriMemory "called isWellAligned_ptrval on function pointer") | PV _ (PVconcrete addr) => sz <- serr2memM (alignof DEFAULT_FUEL None ref_ty) ;; - ret (Z.eqb (Z.modulo (AddressValue.to_Z (C.cap_get_value addr)) sz) 0) + ret (Z.eqb (Z.modulo (cap_to_Z addr) sz) 0) end end. + (* References: + §6.5.3.3, footnote 102 in C11 + §6.5.3.2, footnote 106 in C17 + *) Definition validForDeref_ptrval (ref_ty: CoqCtype.ctype) (ptrval: pointer_value) : memM bool := let do_test (alloc_id : storage_instance_id): memM bool := - is_dead alloc_id >>= + is_dead_allocation alloc_id >>= (fun (x : bool) => match x with | true => ret false @@ -2623,13 +2749,12 @@ Module CheriMemory match ptrval with | PV _ (PVfunction _) => ret false | (PV Prov_device (PVconcrete c_value)) as ptrval => - if cap_is_null c_value then - ret false - else - isWellAligned_ptrval ref_ty ptrval + if cap_is_null c_value + then ret false + else isWellAligned_ptrval ref_ty ptrval | PV (Prov_symbolic iota) (PVconcrete c_value) => - if cap_is_null c_value then - ret false + if cap_is_null c_value + then ret false else lookup_iota iota >>= (fun x => @@ -2646,7 +2771,18 @@ Module CheriMemory if cap_is_null c_value then ret false else do_test alloc_id - | PV Prov_none _ => ret false + | PV Prov_none (PVconcrete c_value) => + ret false + | PV Prov_disabled (PVconcrete c_value) => + if cap_is_null c_value + then ret false + else + find_overlapping (cap_to_Z c_value) >>= fun x => + match x with + | NoAlloc => fail Loc_unknown (MerrAccess LoadAccess OutOfBoundPtr) + | DoubleAlloc _ _ => fail Loc_unknown (MerrInternal "DoubleAlloc without PNVI") + | SingleAlloc alloc_id => isWellAligned_ptrval ref_ty ptrval + end end. Definition add_iota @@ -2674,11 +2810,11 @@ Module CheriMemory | CoqCtype.Unsigned CoqCtype.Intptr_t, IC _ c_value | CoqCtype.Signed CoqCtype.Intptr_t, IC _ c_value => - let addr := AddressValue.to_Z (C.cap_get_value c_value) in - get >>= - (fun (st : mem_state) => - match find_overlaping st addr with - | NoAlloc => ret Prov_none + let addr := (cap_to_Z c_value) in + find_overlapping addr >>= + (fun x => + match x with + | NoAlloc => ret (default_prov tt) | SingleAlloc alloc_id => ret (Prov_some alloc_id) | DoubleAlloc alloc_id1 alloc_id2 => add_iota (alloc_id1,alloc_id2) >>= @@ -2691,7 +2827,7 @@ Module CheriMemory raise (InternalErr "ptrfromint: invalid encoding for [u]intptr_t") | _, IV n_value => if Z.eqb n_value 0 - then ret (PV Prov_none (PVconcrete (C.cap_c0 tt))) + then ret (PV (default_prov tt) (PVconcrete (C.cap_c0 tt))) else let addr := let dlt := Z.succ (Z.sub (AddressValue.to_Z C.max_ptraddr) (AddressValue.to_Z C.min_ptraddr)) in @@ -2700,10 +2836,10 @@ Module CheriMemory then r_value else Z.sub r_value dlt in - get >>= - (fun (st : mem_state) => - match find_overlaping st addr with - | NoAlloc => ret Prov_none + find_overlapping addr >>= + (fun x => + match x with + | NoAlloc => ret (default_prov tt) | SingleAlloc alloc_id => ret (Prov_some alloc_id) | DoubleAlloc alloc_id1 alloc_id2 => add_iota (alloc_id1, alloc_id2) >>= @@ -2744,13 +2880,9 @@ Module CheriMemory else 1 | _ => - if - andb (Z.leb n_value min_ity2) - (Z.leb n_value max_ity2) - then - n_value - else - wrapI min_ity2 max_ity2 n_value + if Z.leb n_value min_ity2 && Z.leb n_value max_ity2 + then n_value + else wrapI min_ity2 max_ity2 n_value end in match ival, ity2 with | IC false _, CoqCtype.Unsigned CoqCtype.Intptr_t @@ -2760,10 +2892,10 @@ Module CheriMemory | IC (true as is_signed) cap, CoqCtype.Unsigned CoqCtype.Intptr_t => ret (inr (IC (negb is_signed) cap)) | IC false cap, _ => - let n_value := AddressValue.to_Z (C.cap_get_value cap) in + let n_value := (cap_to_Z cap) in ret (inr (IV (conv_int_to_ity2 n_value))) | IC true cap, _ => - let n_value := AddressValue.to_Z (C.cap_get_value cap) in + let n_value := (cap_to_Z cap) in ret (inr (IV (conv_int_to_ity2 (unwrap_cap_value n_value)))) | IV n_value, CoqCtype.Unsigned CoqCtype.Intptr_t | IV n_value, CoqCtype.Signed CoqCtype.Intptr_t => @@ -2878,8 +3010,8 @@ Module CheriMemory | _ => ret (IV 0) end else - (if CoqSwitches.has_switch (SW.get_swtiches tt) (CoqSwitches.SW_PNVI AE) || - CoqSwitches.has_switch (SW.get_swtiches tt) (CoqSwitches.SW_PNVI AE_UDI) + (if CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_PNVI AE) || + CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_PNVI AE_UDI) then match prov with | Prov_some alloc_id => expose_allocation alloc_id @@ -2898,7 +3030,7 @@ Module CheriMemory minival <- serr2memM (min_ival ity) ;; let ity_max := num_of_int maxival in let ity_min := num_of_int minival in - let addr := AddressValue.to_Z (C.cap_get_value c_value) in + let addr := (cap_to_Z c_value) in if Z.ltb addr ity_min || Z.ltb ity_max addr then fail loc MerrIntFromPtr else ret (IV addr) @@ -2993,6 +3125,19 @@ Module CheriMemory sz <- serr2memM (sizeof DEFAULT_FUEL None ty) ;; let offset := Z.mul sz ival in + let shift_concrete c_value shifted_addr alloc_id := + get_allocation alloc_id >>= + (fun (alloc : allocation) => + if Z.leb (AddressValue.to_Z alloc.(base)) shifted_addr + && Z.leb (Z.add shifted_addr sz) + (Z.add (Z.add (AddressValue.to_Z alloc.(base)) alloc.(size)) sz) + then + let c_value := C.cap_set_value c_value (AddressValue.of_Z shifted_addr) in + ret (PV (Prov_some alloc_id) (PVconcrete c_value)) + else + fail loc MerrArrayShift + ) + in match ptrval with | PV _ (PVfunction _) => raise (InternalErr "CHERI.eff_array_shift_ptrval, PVfunction") @@ -3002,11 +3147,10 @@ Module CheriMemory "TODO(shift a null pointer should be undefined behaviour)") else let shifted_addr := - Z.add (AddressValue.to_Z (C.cap_get_value c_value)) + Z.add (cap_to_Z c_value) offset in let precond (z_value : Z.t) : memM bool := - if CoqSwitches.has_switch (SW.get_swtiches tt) (CoqSwitches.SW_pointer_arith STRICT) - || negb (CoqSwitches.has_switch (SW.get_swtiches tt) (CoqSwitches.SW_pointer_arith PERMISSIVE)) + if is_strict_pointer_arith tt then get_allocation z_value >>= (fun (alloc : allocation) => @@ -3030,7 +3174,7 @@ Module CheriMemory (fun (x : bool) => match x with | true => - if CoqSwitches.has_switch (SW.get_swtiches tt) (SW_pointer_arith PERMISSIVE) + if CoqSwitches.has_switch (SW.get_switches tt) (SW_pointer_arith PERMISSIVE) then ret NoCollapse else fail loc @@ -3086,35 +3230,35 @@ Module CheriMemory end) end) | PV (Prov_some alloc_id) (PVconcrete c_value) => - let shifted_addr := Z.add (AddressValue.to_Z (C.cap_get_value c_value)) offset in - if CoqSwitches.has_switch (SW.get_swtiches tt) (CoqSwitches.SW_pointer_arith STRICT) - || negb (CoqSwitches.has_switch (SW.get_swtiches tt) (SW_pointer_arith PERMISSIVE)) + let shifted_addr := Z.add (cap_to_Z c_value) offset in + if is_strict_pointer_arith tt then - get_allocation alloc_id >>= - (fun (alloc : allocation) => - if Z.leb (AddressValue.to_Z alloc.(base)) shifted_addr - && Z.leb (Z.add shifted_addr sz) - (Z.add (Z.add (AddressValue.to_Z alloc.(base)) alloc.(size)) sz) - then - let c_value := C.cap_set_value c_value (AddressValue.of_Z shifted_addr) in - ret (PV (Prov_some alloc_id) (PVconcrete c_value)) - else - fail loc MerrArrayShift - ) + shift_concrete c_value shifted_addr alloc_id else let c_value := C.cap_set_value c_value (AddressValue.of_Z shifted_addr) in ret (PV (Prov_some alloc_id) (PVconcrete c_value)) | PV Prov_none (PVconcrete c_value) => let shifted_addr := Z.add (AddressValue.to_Z (C.cap_get_value c_value)) offset in - if CoqSwitches.has_switch (SW.get_swtiches tt) (CoqSwitches.SW_pointer_arith STRICT) - || negb (CoqSwitches.has_switch (SW.get_swtiches tt) (CoqSwitches.SW_pointer_arith PERMISSIVE)) - then - fail loc (MerrOther "out-of-bound pointer arithmetic (Prov_none)") + if is_strict_pointer_arith tt + then fail loc (MerrOther "out-of-bound pointer arithmetic (Prov_none)") else let c_value := C.cap_set_value c_value (AddressValue.of_Z shifted_addr) in ret (PV Prov_none (PVconcrete c_value)) + | PV Prov_disabled (PVconcrete c_value) => + let shifted_addr := Z.add (cap_to_Z c_value) offset in + if is_strict_pointer_arith tt + then + find_overlapping (cap_to_Z c_value) >>= fun x => + match x with + | NoAlloc => fail loc (MerrAccess LoadAccess OutOfBoundPtr) + | DoubleAlloc _ _ => fail loc (MerrInternal "DoubleAlloc without PNVI") + | SingleAlloc alloc_id => shift_concrete c_value shifted_addr alloc_id + end + else + let c_value := C.cap_set_value c_value (AddressValue.of_Z shifted_addr) in + ret (PV Prov_disabled (PVconcrete c_value)) | PV Prov_device (PVconcrete c_value) => - let shifted_addr := Z.add (AddressValue.to_Z (C.cap_get_value c_value)) offset in + let shifted_addr := Z.add (cap_to_Z c_value) offset in let c_value := C.cap_set_value c_value (AddressValue.of_Z shifted_addr) in ret (PV Prov_device (PVconcrete c_value)) end. @@ -3158,7 +3302,7 @@ Module CheriMemory then ret (PV prov (PVconcrete (C.cap_c0 tt))) else raise (InternalErr "CHERI.member_shift_ptrval, shifting NULL") else - let addr := AddressValue.to_Z (C.cap_get_value c_value) in + let addr := (cap_to_Z c_value) in let c_value := C.cap_set_value c_value (AddressValue.of_Z (Z.add addr offset)) in ret (PV prov (PVconcrete c_value)) end. @@ -3172,7 +3316,7 @@ Module CheriMemory match ptr with | PV _ (PVconcrete c_value) | PV _ (PVfunction (FP_invalid c_value)) => - ret (AddressValue.to_Z (C.cap_get_value c_value)) + ret (cap_to_Z c_value) | _ => raise "memcpy: invalid pointer value" end in let size_n := num_of_int size_int in @@ -3265,45 +3409,78 @@ Module CheriMemory acc) (List.combine bytes1 bytes2) 0)))). + Definition cornucopiaRevoke (_:unit) : memM unit + := + st <- get ;; + monadic_fold_left + (fun _ '(allloc_id, alloc) => + if alloc.(is_dead) && alloc.(is_dynamic) + then + (revoke_pointers alloc ;; + remove_allocation allloc_id) + else ret tt + ) + (ZMap.elements st.(allocations)) tt. + Definition realloc (loc : location_ocaml) (tid : thread_id) (align : integer_value) (ptr : pointer_value) (size : integer_value) : memM pointer_value := + (if CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_revocation CORNUCOPIA) + then cornucopiaRevoke tt + else ret tt) ;; match ptr with - | PV Prov_none (PVconcrete c_value) => - if cap_is_null c_value then + | PV Prov_none (PVconcrete c) => + if cap_is_null c then allocate_region tid (CoqSymbol.PrefOther "realloc") align size else fail loc (MerrWIP "realloc no provenance") - | PV (Prov_some alloc_id) (PVconcrete c_value) => - let addr := (C.cap_get_value c_value) in - is_dynamic c_value >>= - (fun (x : bool) => - match x with - | false => fail loc (MerrUndefinedRealloc Free_non_matching) - | true => - is_dead alloc_id >>= - (fun x => match x with - | true => - fail loc (MerrUndefinedRealloc Free_dead_allocation) - | false => - get_allocation alloc_id >>= - (fun (alloc : allocation) => - if AddressValue.eqb alloc.(base) addr then - allocate_region tid (CoqSymbol.PrefOther "realloc") align size >>= - (fun (new_ptr : pointer_value) => - let size_to_copy := - let size_n := num_of_int size in - IV (Z.min (CheriMemory.size alloc) size_n) in - memcpy new_ptr ptr size_to_copy ;; - kill (Loc_other "realloc") true ptr ;; - ret new_ptr) - else - fail loc - (MerrUndefinedRealloc Free_out_of_bound)) - end) - end) + | PV Prov_disabled (PVconcrete c) => + if cap_is_null c then + allocate_region tid (CoqSymbol.PrefOther "realloc") align size + else + find_live_allocation (C.cap_get_value c) >>= + fun x => + match x with + | None => fail loc (MerrUndefinedFree Free_non_matching) + | Some (alloc_id,alloc) => + if negb (cap_match_dyn_allocation c alloc) + then fail loc (MerrUndefinedFree Free_non_matching) + else + allocate_region tid (CoqSymbol.PrefOther "realloc") align size >>= + (fun (new_ptr : pointer_value) => + let size_to_copy := + let size_n := num_of_int size in + IV (Z.min (CheriMemory.size alloc) size_n) in + memcpy new_ptr ptr size_to_copy ;; + kill (Loc_other "realloc") true ptr ;; + ret new_ptr) + end + | PV (Prov_some alloc_id) (PVconcrete c) => + if cap_is_null c then + allocate_region tid (CoqSymbol.PrefOther "realloc") align size + else + get_allocation alloc_id >>= + fun (alloc : allocation) => + if negb (cap_match_dyn_allocation c alloc) + then fail loc (MerrUndefinedRealloc Free_non_matching) + else + if alloc.(is_dead) + then fail loc (MerrUndefinedRealloc Free_dead_allocation) + else + if AddressValue.eqb alloc.(base) (C.cap_get_value c) + then + allocate_region tid (CoqSymbol.PrefOther "realloc") align size >>= + (fun (new_ptr : pointer_value) => + let size_to_copy := + let size_n := num_of_int size in + IV (Z.min (CheriMemory.size alloc) size_n) in + memcpy new_ptr ptr size_to_copy ;; + kill (Loc_other "realloc") true ptr ;; + ret new_ptr) + else + fail loc (MerrUndefinedRealloc Free_out_of_bound) | PV _ _ => fail loc (MerrWIP "realloc: invalid pointer") end. @@ -3611,7 +3788,7 @@ Module CheriMemory | O => raise (InternalErr "string too long") | S max_len => cap_check loc c_value offset ReadIntent 1 ;; - let addr := Z.add (AddressValue.to_Z (C.cap_get_value c_value)) offset + let addr := Z.add (cap_to_Z c_value) offset in get >>= (fun st => @@ -3640,15 +3817,15 @@ Module CheriMemory let pre_bs := List.map (fun (c_value : ascii) => - {| prov := Prov_none; copy_offset := None; + {| prov := (default_prov tt); copy_offset := None; value := Some c_value |}) cs in let pre_bs := List.app pre_bs [ - {| prov := Prov_none; copy_offset := None; + {| prov := (default_prov tt); copy_offset := None; value := Some "000" % char |} ] in - let addr := AddressValue.to_Z (C.cap_get_value c_value) in + let addr := (cap_to_Z c_value) in let bs := mapi (fun (i_value : nat) (b_value : AbsByte) => @@ -3669,7 +3846,11 @@ Module CheriMemory (loc : location_ocaml) (name : string) (args : list mem_value) : memM (option mem_value) := - if String.eqb name "strfcap" then + if String.eqb name "cheri_revoke" then + if CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_revocation CORNUCOPIA) + then (cornucopiaRevoke tt ;; ret None) + else fail loc (MerrOther "'cheri_revoke' called without 'cornucopia' switch") + else if String.eqb name "strfcap" then buf_val <- option2memM "missing argument" (List.nth_error args 0%nat) ;; maxsize_val <- option2memM "missing argument" (List.nth_error args 1%nat) ;; format_val <- option2memM "missing argument" (List.nth_error args 2%nat) ;; @@ -3744,7 +3925,7 @@ Module CheriMemory ;; match upper_val with | MVinteger CoqCtype.Size_t (IV n_value) => - let x' := AddressValue.to_Z (C.cap_get_value c_value) in + let x' := (cap_to_Z c_value) in let c_value := C.cap_narrow_bounds c_value (Bounds.of_Zs (x', (Z.add x' n_value))) in ret (Some (update_cap_in_mem_value cap_val c_value)) | _ => @@ -3831,7 +4012,7 @@ Module CheriMemory "CHERI.call_intrinsic: non-cap 1st argument in: '" (String.append name "'"))) | Some (_, c_value) => - let v_value := AddressValue.to_Z (C.cap_get_value c_value) in + let v_value := (cap_to_Z c_value) in ret (Some (MVinteger CoqCtype.Ptraddr_t (IV v_value))) end) else @@ -4011,7 +4192,11 @@ Module CheriMemory Definition get_intrinsic_type_spec (name : string) : option intrinsics_signature := - if String.eqb name "strfcap" then + if String.eqb name "cheri_revoke" then + if CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_revocation CORNUCOPIA) + then Some ((ExactRet CoqCtype.void), []) + else None + else if String.eqb name "strfcap" then Some ((ExactRet CoqCtype.signed_long), diff --git a/coq/CheriMemory/CoqCtype.v b/coq/CheriMemory/CoqCtype.v index 6e842b2ae..95aac9242 100644 --- a/coq/CheriMemory/CoqCtype.v +++ b/coq/CheriMemory/CoqCtype.v @@ -442,12 +442,14 @@ Definition no_qualifiers : qualifiers := {|const := false;restrict := fals Definition combine_qualifiers (qs1 : qualifiers ) (qs2 : qualifiers ) : qualifiers := {|const := ((const qs1) ||(const qs2)) ;restrict := ((restrict qs1) ||(restrict qs2));volatile := ((volatile qs1) ||(volatile qs2)) |}. +*) (* Some constructors *) Definition mk_ctype_pointer (qs : qualifiers ) (ty : ctype ) : ctype := - Ctype [] (Pointer qs ty). + Ctype nil (Pointer qs ty). +(* Definition mk_ctype_integer (ity : integerType ) : ctype := Ctype [] (Basic (Integer ity)). diff --git a/coq/CheriMemory/dune b/coq/CheriMemory/dune index 527da414d..8f75bc02e 100644 --- a/coq/CheriMemory/dune +++ b/coq/CheriMemory/dune @@ -1,4 +1,5 @@ (coq.theory + (mode vo) (name CheriMemory) (package cerberus-cheri) (modules CoqLocation CoqAnnot CoqCtype CoqSwitches CoqImplementation CoqAilSyntax CoqAilTypesAux ErrorWithState CoqMem_common Memory_model CoqSymbol CoqUndefined CoqTags CheriMemory CerbSwitches) diff --git a/coq/Common/Utils.v b/coq/Common/Utils.v index 76798a8cb..48c473aea 100644 --- a/coq/Common/Utils.v +++ b/coq/Common/Utils.v @@ -25,7 +25,7 @@ Local Open Scope string_scope. Local Open Scope Z_scope. Local Open Scope bool_scope. -Definition debugging : bool := false. +Definition debugging : bool := true. (* this definition will be remapped on extraction to OCaml's print_endline *) Definition print_msg (msg : string) : unit := tt. @@ -294,3 +294,9 @@ Proof. rewrite H0, H1. apply string_eq_refl. Qed. + +(** Helper function to split a list at given position. + List.split_at in Lem. + *) +Definition split_at {A:Type} (n:nat) (l:list A) + := (List.firstn n l, List.skipn n l). diff --git a/coq/Common/ZMap.v b/coq/Common/ZMap.v new file mode 100644 index 000000000..a4c9d0584 --- /dev/null +++ b/coq/Common/ZMap.v @@ -0,0 +1,81 @@ +Require Import Coq.Numbers.BinNums. +Require Import Coq.ZArith.Zcompare. +Require Import Coq.FSets.FMapAVL. +Require Import Coq.Structures.OrderedTypeEx. + +From ExtLib.Data Require Import List. +From ExtLib.Structures Require Import Monad Monads Traversable. + +From Coq.Lists Require Import List. (* after exltlib *) + +Local Open Scope type_scope. +Local Open Scope list_scope. +Local Open Scope Z_scope. +Local Open Scope monad_scope. + +Import ListNotations. +Import MonadNotation. + +Module ZMap := FMapAVL.Make(Z_as_OT). + +Fixpoint zmap_range_init {T} (a0:Z) (n:nat) (step:Z) (v:T) (m:ZMap.t T) : ZMap.t T + := + match n with + | O => m + | S n => + let m := ZMap.add (Z.add a0 (Z.mul (Z.of_nat n) step)) v m in + zmap_range_init a0 n step v m + end. + +Definition zmap_update_element + {A:Type} + (key: Z) + (v: A) + (m: ZMap.t A) + : (ZMap.t A) + := + ZMap.add key v (ZMap.remove key m). + +(** [update key f m] returns a map containing the same bindings as + [m], except for the binding of [key]. Depending on the value of [y] + where [y] is [f (find_opt key m)], the binding of [key] is added, + removed or updated. If [y] is [None], the binding is removed if it + exists; otherwise, if [y] is [Some z] then key is associated to [z] + in the resulting map. *) +Definition zmap_update + {A:Type} + (key: Z) + (f: option A -> option A) + (m: ZMap.t A) + : (ZMap.t A) + := + let y := f (ZMap.find key m) in + let m' := ZMap.remove key m in (* could be optimized, as removal may be unecessary in some cases *) + match y with + | None => m' + | Some z => ZMap.add key z m' + end. + +Definition zmap_sequence + {A: Type} + {m: Type -> Type} + {M: Monad m} + (mv: ZMap.t (m A)): m (ZMap.t A) + := + let fix loop (ls: list (ZMap.key*(m A))) (acc:ZMap.t A) : m (ZMap.t A) := + match ls with + | [] => ret acc + | (k,mv)::ls => mv >>= (fun v => loop ls (ZMap.add k v acc)) + end + in + loop (ZMap.elements mv) (ZMap.empty A). + +(* Monadic mapi *) +Definition zmap_mmapi + {A B : Type} + {m : Type -> Type} + {M : Monad m} + (f : ZMap.key -> A -> m B) (zm: ZMap.t A) + : m (ZMap.t B) + := + zmap_sequence (ZMap.mapi f zm). diff --git a/coq/Common/dune b/coq/Common/dune index 22456d6aa..4e8265d01 100644 --- a/coq/Common/dune +++ b/coq/Common/dune @@ -1,6 +1,7 @@ (coq.theory + (mode vo) (name Common) (package cerberus-cheri) - (modules SimpleError Utils) + (modules SimpleError Utils ZMap) (theories ExtLib StructTact Sail bbv) ) diff --git a/coq/Morello/dune b/coq/Morello/dune index 9203552ed..6920aeaec 100644 --- a/coq/Morello/dune +++ b/coq/Morello/dune @@ -1,4 +1,5 @@ (coq.theory + (mode vo) (name Morello) (package cerberus-cheri) (modules CapabilitiesGS MorelloCapsGS) diff --git a/coq/dune b/coq/dune index 58d0cb81c..993c28c6e 100644 --- a/coq/dune +++ b/coq/dune @@ -119,6 +119,7 @@ (copy_files extracted/Ring_polynom.{ml,mli}) (copy_files extracted/Ring_theory.{ml,mli}) (copy_files extracted/SimpleError.{ml,mli}) +(copy_files extracted/ZMap.{ml,mli}) (copy_files extracted/Specif.{ml,mli}) (copy_files extracted/String0.{ml,mli}) (copy_files extracted/String1.{ml,mli}) @@ -134,6 +135,7 @@ (copy_files extracted/Utils0.{ml,mli}) (copy_files extracted/Values.{ml,mli}) (copy_files extracted/Vector0.{ml,mli}) +(copy_files extracted/vector1.{ml,mli}) (copy_files extracted/VectorDef.{ml,mli}) (copy_files extracted/Wf.{ml,mli}) (copy_files extracted/Word.{ml,mli}) diff --git a/coq/extracted/Extract.v b/coq/extracted/Extract.v index 8629327a3..578c58c17 100644 --- a/coq/extracted/Extract.v +++ b/coq/extracted/Extract.v @@ -16,11 +16,16 @@ Require Import ExtrOcamlZBigInt. Extraction Language OCaml. Unset Extraction Optimize. (* trying to make print_msg work *) -Extraction Blacklist String List Char Core Monad Bool Vector Format Nat Int Option Base Numbers FMapAVL OrderedType Map. +Require Import Coq.Vectors.Vector. +From stdpp Require Import vector. + +Extraction Blacklist vector Vector String List Char Core Monad Bool Format Nat Int Option Base Numbers FMapAVL OrderedType Map. (* Debugging print *) Extraction NoInline Common.Utils.print_msg. -Extract Constant Common.Utils.print_msg => "print_endline". +Extraction NoInline Common.Utils.sprint_msg. +Extract Constant Common.Utils.print_msg => "Stdlib.prerr_endline". +Extract Constant Sail.Values.prerr_endline => "Stdlib.prerr_endline". Extract Inlined Constant MorelloCapsGS.Capability_GS.strfcap => "strfcap". (* Used by Coq's Real library *) @@ -29,6 +34,6 @@ Extract Constant ClassicalDedekindReals.sig_not_dec => false. (* Ugh *) (* Set Extraction AccessOpaque. *) -Extraction Library Vector. +Extraction Library vector. Recursive Extraction Library MorelloCapsGS. Recursive Extraction Library CheriMemory. diff --git a/coq/extracted/dune b/coq/extracted/dune index f7bdb6747..e67ac3224 100644 --- a/coq/extracted/dune +++ b/coq/extracted/dune @@ -1,5 +1,6 @@ (coq.extraction + (mode vo) (prelude Extract) - (extracted_modules Addr BinaryString Capabilities Capabilities0 CapabilitiesGS CoqAilSyntax CoqAnnot Applicative Ascii BinInt BinList BinNat BinNatDef BinNums BinPos BinPosDef bitvector Compare_dec Qcanon Relation_Definitions Bool0 Byte CapFns CapFnsTypes CarryType CheriMemory ClassicalDedekindReals CMorphisms ConstructiveCauchyAbs ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveEpsilon ConstructiveExtra ConstructiveRcomplete ConstructiveReals CRelationClasses CoqCtype Datatypes DecidableClass Decimal DepEqNat EitherMonad Eqdep_dec Equalities EquivDec ErrorWithState Fin FloatClass FMapAVL0 FMapList Functor Hexadecimal HexString CoqImplementation Init Injection Instr_kinds Int0 List0 List1 ListSet CoqLocation Logic Monad0 MonadExc MonadFix MonadPlus MonadReader MonadState MonadTrans MonadWriter MonadZero Monoid MorelloCapsGS Nat0 NatLib Number Operators_mwords OrderedType0 OrderedTypeEx Orders OrdersTac PeanoNat PrimFloat PrimInt63 Prompt Prompt_monad Qabs QArith_base QExtra Qreduction Qround Rdefinitions RelDec Ring_polynom Ring_theory SimpleError Specif String0 String1 Sumbool CoqSwitches CoqSymbol CoqTags CerbSwitches Traversable CoqUndefined Undefined Utils Utils0 TypeCasts MachineWord Values Vector0 VectorDef Wf Word ZArith_dec Zbool Bvector Zdigits Zeven base0 Basics countable decidable fin0 list2 numbers0 option0 finite list_numbers) + (extracted_modules Addr BinaryString Capabilities Capabilities0 CapabilitiesGS CoqAilSyntax CoqAnnot Applicative Ascii BinInt BinList BinNat BinNatDef BinNums BinPos BinPosDef bitvector Compare_dec Qcanon Relation_Definitions Bool0 Byte CapFns CapFnsTypes CarryType CheriMemory ClassicalDedekindReals CMorphisms ConstructiveCauchyAbs ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveEpsilon ConstructiveExtra ConstructiveRcomplete ConstructiveReals CRelationClasses CoqCtype Datatypes DecidableClass Decimal DepEqNat EitherMonad Eqdep_dec Equalities EquivDec ErrorWithState Fin FloatClass FMapAVL0 FMapList Functor Hexadecimal HexString CoqImplementation Init Injection Instr_kinds Int0 List0 List1 ListSet CoqLocation Logic Monad0 MonadExc MonadFix MonadPlus MonadReader MonadState MonadTrans MonadWriter MonadZero Monoid MorelloCapsGS Nat0 NatLib Number Operators_mwords OrderedType0 OrderedTypeEx Orders OrdersTac PeanoNat PrimFloat PrimInt63 Prompt Prompt_monad Qabs QArith_base QExtra Qreduction Qround Rdefinitions RelDec Ring_polynom Ring_theory SimpleError ZMap Specif String0 String1 Sumbool CoqSwitches CoqSymbol CoqTags CerbSwitches Traversable CoqUndefined Undefined Utils Utils0 TypeCasts MachineWord Values Vector0 vector1 VectorDef Wf Word ZArith_dec Zbool Bvector Zdigits Zeven base0 Basics countable decidable fin0 list2 numbers0 option0 finite list_numbers) (theories CheriMemory Common Morello ExtLib stdpp Sail bbv StructTact CheriCaps) ) diff --git a/dune b/dune index c69a2ebb7..25692ef32 100644 --- a/dune +++ b/dune @@ -3,6 +3,6 @@ (dev (flags :standard -bin-annot -I +unix -I +str)) (release (flags :standard -bin-annot -I +unix -I +str))) -(dirs util sibylfs ocaml_frontend memory parsers backend tools runtime) +(dirs util sibylfs ocaml_frontend memory parsers backend tools runtime coq) diff --git a/frontend/model/builtins.lem b/frontend/model/builtins.lem index b240ccad9..73414d375 100644 --- a/frontend/model/builtins.lem +++ b/frontend/model/builtins.lem @@ -495,6 +495,8 @@ let translate_builtin_varnames (Symbol.Identifier _ str) = Just (AilEbuiltin (AilBCHERI "cheri_representable_length")) | "__cerbvar_cheri_representable_alignment_mask" -> Just (AilEbuiltin (AilBCHERI "cheri_representable_alignment_mask")) + | "__cerbvar_cheri_revoke" -> + Just (AilEbuiltin (AilBCHERI "cheri_revoke")) | _ -> Nothing end diff --git a/frontend/model/core_typing.lem b/frontend/model/core_typing.lem index df35be81c..7c5dea8cd 100644 --- 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 index 7b7a53ffe..24cf04567 100644 --- 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 index fc99c592a..b25bc142e 100644 --- a/frontend/model/translation.lem +++ b/frontend/model/translation.lem @@ -2310,11 +2310,37 @@ end end end - | A.AilEcall (A.AnnotatedExpression _ _ _ (A.AilEbuiltin (A.AilBCHERI str))) es -> + | A.AilEcall (A.AnnotatedExpression _ _ _ (A.AilEbuiltin (A.AilBCHERI str))) [] -> + E.return begin + C.Expr [] (C.Ememop (Mem_common.CHERI_intrinsic str (result_ty, [])) []) + end + + | 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 oTy_ret = force_core_object_type_of_ctype result_ty in + 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 - E.wrapped_fresh_symbol (C.BTy_object oTy_ret) >>= fun memop_wrp -> + E.wrapped_fresh_symbol bTy_ret >>= fun memop_wrp -> (* E.foldlM (fun (sym_pat_acc, sym_pe_acc, obj_pat_acc, obj_pe_acc) oTy -> E.wrapped_fresh_symbol (C.BTy_loaded oTy) >>= fun (_, sym_pat, sym_pe) -> E.wrapped_fresh_symbol (C.BTy_object oTy) >>= fun (_, obj_pat, obj_pe) -> @@ -2337,8 +2363,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 diff --git a/memory/cheri-coq/impl_mem.ml b/memory/cheri-coq/impl_mem.ml index a5c0fd25b..1ad3beaaa 100644 --- a/memory/cheri-coq/impl_mem.ml +++ b/memory/cheri-coq/impl_mem.ml @@ -9,6 +9,7 @@ open CoqImplementation open Strfcap open CoqSwitches open Switches +open ZMap module CerbSwitchesProxy = struct @@ -37,7 +38,7 @@ module CerbSwitchesProxy = struct List.fold_left (fun s x -> set_add (=) (toCoq_switch x) s) empty_set cs - let get_swtiches _ = toCoq_switches (Switches.get_switches ()) + let get_switches _ = toCoq_switches (Switches.get_switches ()) end module CerbTagDefs = struct @@ -316,6 +317,15 @@ module CHERIMorello : Memory = struct let get = Nondeterminism.nd_get let (>>=) = Nondeterminism.nd_bind + (* TODO: hackish *) + let fail ?(loc=Cerb_location.other "Cheri") err = + let open Nondeterminism in + match undefinedFromMem_error err with + | Some ub -> + kill (Undef0 (loc, [ub])) + | None -> + kill (Other err) + let lift_coq_serr: (string, 'a) Datatypes.sum -> 'a = function | Coq_inl errs -> failwith errs | Coq_inr v -> v @@ -850,9 +860,12 @@ module CHERIMorello : Memory = struct | InternalErr msg -> failwith msg - (* --- debugging --- *) + open PPrint + open Cerb_pp_prelude let string_of_provenance = function + | MM.Prov_disabled -> + "@disabled" | MM.Prov_none -> "@empty" | Prov_some alloc_id -> @@ -862,11 +875,71 @@ module CHERIMorello : Memory = struct | Prov_device -> "@device" + let pp_pointer_value ?(is_verbose=false) (MM.PV (prov, ptrval_)) = + match ptrval_ with + | MM.PVfunction (FP_valid sym) -> + !^ "Cfunction" ^^ P.parens (!^ (Pp_symbol.to_string_pretty + (fromCoq_Symbol_sym sym))) + | PVfunction (FP_invalid c) -> + !^ "Cfunction" ^^ P.parens (!^ "invalid" ^^ P.colon ^^^ !^ (C.to_string c)) + (* !^ ("") *) + | PVconcrete c -> + if C.eqb c (C.cap_c0 ()) then + !^ "NULL" + else + (* TODO: remove this idiotic hack when Lem's nat_big_num library expose "format" *) + P.parens (!^ (string_of_provenance prov) ^^ P.comma ^^^ !^ (C.to_string c)) + + let pp_integer_value = function + | (MM.IV n) -> + !^ (Z.to_string n) + | (IC (is_signed, c)) -> + let cs = (C.to_string c) + ^ (if is_signed then " (signed)" else " (unsigned)") + in + !^ cs + + let pp_integer_value_for_core = pp_integer_value + + let pp_pretty_pointer_value = pp_pointer_value ~is_verbose:false + let pp_pretty_integer_value _ = pp_integer_value + + let rec pp_mem_value = function + | MM.MVunspecified _ -> + PPrint.string "UNSPEC" + | MVinteger (_, ival) -> + pp_integer_value ival + | MVfloating (_, fval) -> + !^ (Float64.to_string fval) + | MVpointer (_, ptrval) -> + !^ "ptr" ^^ parens (pp_pointer_value ptrval) + | MVarray mvals -> + braces ( + comma_list pp_mem_value mvals + ) + | MVstruct (tag_sym, xs) -> + parens (!^ "struct" ^^^ !^ (Pp_symbol.to_string_pretty (fromCoq_Symbol_sym tag_sym))) ^^ + braces ( + comma_list (fun (ident, _, mval) -> + dot ^^ (Pp_symbol.pp_identifier (fromCoq_Symbol_identifier ident)) ^^ equals ^^^ pp_mem_value mval + ) (List.map (fun ((a,b),c) -> (a,b,c)) xs) + ) + | MVunion (tag_sym, membr_ident, mval) -> + parens (!^ "union" ^^^ !^ (Pp_symbol.to_string_pretty (fromCoq_Symbol_sym tag_sym))) ^^ + braces ( + dot ^^ Pp_symbol.pp_identifier (fromCoq_Symbol_identifier membr_ident) ^^ equals ^^^ + pp_mem_value mval + ) + + let pp_pretty_mem_value _ = pp_mem_value + + (* --- debugging --- *) + let print_allocations str st = Printf.fprintf stderr "BEGIN Allocation ==> %s\n" str; let l = ZMap.elements st.MM.allocations in List.iter (fun (aid,a) -> - Printf.fprintf stderr "@%s: 0x%s,%s (%s)\n" + Printf.fprintf stderr "@%s: 0x%s,%s (%s,%s%s)\n" (Z.format "%d" aid) (Z.format "%x" a.MM.base) (Z.format "%d" a.size) @@ -874,11 +947,10 @@ module CHERIMorello : Memory = struct | MM.Exposed -> "exposed" | MM.Unexposed -> "unexposed" ) + (if a.is_dynamic then "dynamic" else "static") + (if a.is_dead then ", dead" else "") ) l; - prerr_endline "END Allocations"; - Printf.fprintf stderr "Dead Allocations: [%s]\n" - (String.concat "," - (List.map (Z.to_string) st.MM.dead_allocations)) + prerr_endline "END Allocations" let print_bytemap str (st:MM.mem_state) = Printf.fprintf stderr "BEGIN BYTEMAP ==> %s\n" str; @@ -910,15 +982,19 @@ module CHERIMorello : Memory = struct (* lifting memM *) - let lift_coq_memM label (m:'a MM.memM): 'a memM = + let lift_coq_memM ?(print_mem_state=true) label (m:'a MM.memM): 'a memM = ND (fun st -> if !Cerb_debug.debug_level >= 2 then Printf.fprintf stderr "MEMOP %s\n" label; - if !Cerb_debug.debug_level >= 3 then + if print_mem_state then + if !Cerb_debug.debug_level >= 2 then begin print_allocations label st ; - print_bytemap label st ; - print_captags label st + if !Cerb_debug.debug_level >= 3 then + begin + print_bytemap label st ; + print_captags label st + end end ; match m st with | (st', Coq_inl e) -> @@ -941,7 +1017,7 @@ module CHERIMorello : Memory = struct get >>= fun st -> Cerb_debug.print_debug 1 [] (fun () -> "allocate_object. last_address=" ^ - (Z.to_string (MM.last_address st)) + (String_nat_big_num.string_of_hexadecimal (MM.last_address st)) ); lift_coq_memM "allocate_object" (MM.allocate_object (toCoq_thread_id tid) @@ -958,27 +1034,53 @@ module CHERIMorello : Memory = struct (size_int: integer_value): pointer_value memM = get >>= fun st -> - Cerb_debug.print_debug 1 [] - (fun () -> "allocate_region. last_address=" ^ - (Z.to_string (MM.last_address st)) - ); - lift_coq_memM "allocate_region" (MM.allocate_region - (toCoq_thread_id tid) - (toCoq_Symbol_prefix pref) - align_int - size_int) + let label = "allocate_region " ^ + "size=" ^ (Pp_utils.to_plain_string (pp_integer_value size_int)) ^ + ", last_address=" ^ (String_nat_big_num.string_of_hexadecimal (MM.last_address st)) + in + bind + (lift_coq_memM label (MM.allocate_region + (toCoq_thread_id tid) + (toCoq_Symbol_prefix pref) + align_int + size_int)) + (fun newptr -> + Cerb_debug.print_debug 1 [] + (fun () -> "MEMOP_RET allocate_region " ^ + "size=" ^ (Pp_utils.to_plain_string (pp_integer_value size_int)) ^ + " = " ^ + Pp_utils.to_plain_string (pp_pointer_value ~is_verbose:false newptr)); + return newptr) let kill (loc:Cerb_location.t) (is_dyn:bool) (pv:pointer_value) : unit memM = - lift_coq_memM "kill" (MM.kill (toCoq_location loc) is_dyn pv) + let label = "kill " + ^ (string_of_bool is_dyn) ^ ", " + ^ Pp_utils.to_plain_string (pp_pointer_value ~is_verbose:false pv) + in + lift_coq_memM label (MM.kill (toCoq_location loc) is_dyn pv) let load (loc:Cerb_location.t) (ty:Ctype.ctype) (p:pointer_value): (footprint * mem_value) memM = - lift_coq_memM "load" (MM.load (toCoq_location loc) (toCoq_ctype ty) p) + let label = "load " + ^ Pp_utils.to_plain_string (pp_pointer_value ~is_verbose:false p) + in + bind + (lift_coq_memM label (MM.load (toCoq_location loc) (toCoq_ctype ty) p)) + (fun (fp,mval) -> + Cerb_debug.print_debug 4 [] + (fun () -> "MEMOP_RET load =" ^ Pp_utils.to_plain_string (pp_mem_value mval)); + return (fp,mval)) let store (loc:Cerb_location.t) (ty:Ctype.ctype) (is_locking:bool) (p:pointer_value) (mval:mem_value): footprint memM = - lift_coq_memM "store" (MM.store (toCoq_location loc) (toCoq_ctype ty) is_locking p mval) + let label = "store " + ^ Pp_utils.to_plain_string (pp_pointer_value ~is_verbose:false p) + ^ if !Cerb_debug.debug_level >= 4 + then (" value="^ Pp_utils.to_plain_string (pp_mem_value mval)) + else "" + in + lift_coq_memM label (MM.store (toCoq_location loc) (toCoq_ctype ty) is_locking p mval) let null_ptrval (ty:Ctype.ctype) : pointer_value = MM.null_ptrval (toCoq_ctype ty) @@ -999,9 +1101,10 @@ module CHERIMorello : Memory = struct | MM.PV (_, PVfunction (FP_valid sym)) -> ffun (Some (fromCoq_Symbol_sym sym)) | PV (_, PVfunction (FP_invalid c)) -> if MM.cap_is_null c - then fnull Ctype.void + then fnull Ctype.void else ffun None - | PV (Prov_none, PVconcrete c) -> + | PV (Prov_none, PVconcrete c) + | PV (Prov_disabled, PVconcrete c) -> if MM.cap_is_null c then fconc None (C.cap_get_value c) else ffun None @@ -1048,6 +1151,8 @@ module CHERIMorello : Memory = struct it requires some dependencies and fixpoint magic. It OK to have in in OCaml for now *) let prefix_of_pointer (MM.PV (prov, pv)) : string option memM = + if !Cerb_debug.debug_level >= 2 then + Printf.fprintf stderr "MEMOP prefix_of_pointer\n"; let open String_symbol in let rec aux addr (alloc:MM.allocation) = function | None @@ -1085,7 +1190,7 @@ module CHERIMorello : Memory = struct in match prov with | Prov_some alloc_id -> - bind (lift_coq_memM "get_allocation" (MM.get_allocation alloc_id)) (fun alloc -> + bind (lift_coq_memM ~print_mem_state:false "get_allocation" (MM.get_allocation alloc_id)) (fun alloc -> begin match pv with | PVconcrete addr -> if C.cap_get_value addr = alloc.base then @@ -1095,6 +1200,26 @@ module CHERIMorello : Memory = struct | _ -> return None end) + | Prov_disabled -> + begin match pv with + | PVconcrete c -> + let addr = C.cap_get_value c in + bind (lift_coq_memM ~print_mem_state:false "find_overlapping" (MM.find_overlapping addr)) (fun x -> + let loc = Cerb_location.unknown in + match x with + | MM.NoAlloc -> fail ~loc (MerrAccess (LoadAccess, OutOfBoundPtr)) + | MM.DoubleAlloc _ -> fail ~loc (MerrInternal "DoubleAlloc without PNVI") + | MM.SingleAlloc alloc_id -> + bind (lift_coq_memM ~print_mem_state:false "get_allocation" (MM.get_allocation alloc_id)) (fun alloc -> + if addr = alloc.base then + return @@ Some (string_of_prefix (fromCoq_Symbol_prefix alloc.prefix)) + else + return @@ aux addr alloc (Option.map fromCoq_ctype alloc.ty) + ) + ) + | _ -> + return None + end | _ -> return None @@ -1295,81 +1420,19 @@ module CHERIMorello : Memory = struct (toCoq_location loc) name args) + >>= + (fun res -> + Cerb_debug.print_debug 4 [] + (fun () -> + match res with + | Some mval -> "MEMOP_RET call_intrinsic = Just " ^ Pp_utils.to_plain_string (pp_mem_value mval) + | None -> "MEMOP_RET call_intrinsic = None" + ); + return res) let get_intrinsic_type_spec name = Option.map fromCoq_intrinsics_signature (MM.get_intrinsic_type_spec name) - open PPrint - open Cerb_pp_prelude - - let string_of_provenance = function - | MM.Prov_none -> - "@empty" - | Prov_some alloc_id -> - "@" ^ Z.to_string alloc_id - | Prov_symbolic iota -> - "@iota(" ^ Z.to_string iota ^ ")" - | Prov_device -> - "@device" - - let pp_pointer_value ?(is_verbose=false) (MM.PV (prov, ptrval_)) = - match ptrval_ with - | MM.PVfunction (FP_valid sym) -> - !^ "Cfunction" ^^ P.parens (!^ (Pp_symbol.to_string_pretty - (fromCoq_Symbol_sym sym))) - | PVfunction (FP_invalid c) -> - !^ "Cfunction" ^^ P.parens (!^ "invalid" ^^ P.colon ^^^ !^ (C.to_string c)) - (* !^ ("") *) - | PVconcrete c -> - if C.eqb c (C.cap_c0 ()) then - !^ "NULL" - else - (* TODO: remove this idiotic hack when Lem's nat_big_num library expose "format" *) - P.parens (!^ (string_of_provenance prov) ^^ P.comma ^^^ !^ (C.to_string c)) - - let pp_integer_value = function - | (MM.IV n) -> - !^ (Z.to_string n) - | (IC (is_signed, c)) -> - let cs = (C.to_string c) - ^ (if is_signed then " (signed)" else " (unsigned)") - in - !^ cs - - let pp_integer_value_for_core = pp_integer_value - - let pp_pretty_pointer_value = pp_pointer_value ~is_verbose:false - let pp_pretty_integer_value _ = pp_integer_value - - let rec pp_mem_value = function - | MM.MVunspecified _ -> - PPrint.string "UNSPEC" - | MVinteger (_, ival) -> - pp_integer_value ival - | MVfloating (_, fval) -> - !^ (Float64.to_string fval) - | MVpointer (_, ptrval) -> - !^ "ptr" ^^ parens (pp_pointer_value ptrval) - | MVarray mvals -> - braces ( - comma_list pp_mem_value mvals - ) - | MVstruct (tag_sym, xs) -> - parens (!^ "struct" ^^^ !^ (Pp_symbol.to_string_pretty (fromCoq_Symbol_sym tag_sym))) ^^ - braces ( - comma_list (fun (ident, _, mval) -> - dot ^^ (Pp_symbol.pp_identifier (fromCoq_Symbol_identifier ident)) ^^ equals ^^^ pp_mem_value mval - ) (List.map (fun ((a,b),c) -> (a,b,c)) xs) - ) - | MVunion (tag_sym, membr_ident, mval) -> - parens (!^ "union" ^^^ !^ (Pp_symbol.to_string_pretty (fromCoq_Symbol_sym tag_sym))) ^^ - braces ( - dot ^^ Pp_symbol.pp_identifier (fromCoq_Symbol_identifier membr_ident) ^^ equals ^^^ - pp_mem_value mval - ) - - let pp_pretty_mem_value _ = pp_mem_value - (* JSON serialisation *) let serialise_mem_state dig (st: mem_state) : Cerb_json.json = `Assoc [] (* TODO: not implemented *) diff --git a/runtime/libc/include/cheriintrin.h b/runtime/libc/include/cheriintrin.h index 5875980d2..4e35d8b26 100644 --- a/runtime/libc/include/cheriintrin.h +++ b/runtime/libc/include/cheriintrin.h @@ -17,4 +17,8 @@ #define cheri_representable_length __cerbvar_cheri_representable_length #define cheri_representable_alignment_mask __cerbvar_cheri_representable_alignment_mask +#ifdef WITH_CORNUCOPIA +#define cheri_revoke __cerbvar_cheri_revoke +#endif + #endif diff --git a/tools/cheribuild_hack.sh b/tools/cheribuild_hack.sh deleted file mode 100755 index f15618363..000000000 --- a/tools/cheribuild_hack.sh +++ /dev/null @@ -1,38 +0,0 @@ -#!/bin/bash - -trap 'repair_dune' SIGINT - -# GNU vs BSD -# function sedi(){ -# if sed --version 2>/dev/null 1>/dev/null; then -# echo "sed -i -e '$1' $2" -# else -# echo "sed -i '' -e '$1' $2" -# fi -# } - -function repair_dune() { - case "$(uname -s)" in - Darwin) - sed -i '' -e '/(dirs/s/ coq//' dune - ;; - *) - sed -i -e '/(dirs/s/ coq//' dune - ;; - esac -} - -function add_coq() { - case "$(uname -s)" in - Darwin) - sed -i '' -e 's/(dirs \([^)]*\))/(dirs \1 coq)/' dune - ;; - *) - sed -i -e 's/(dirs \([^)]*\))/(dirs \1 coq)/' dune - ;; - esac -} - -add_coq -eval $1 -repair_dune