Skip to content

Commit

Permalink
more syntax cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@vzaliva
vzaliva committed Aug 2, 2023
1 parent f82f1c7 commit ca875af
Showing 1 changed file with 90 additions and 117 deletions.
207 changes: 90 additions & 117 deletions coq/CheriMemory/CheriMemory.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -323,30 +323,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])
Expand Down Expand Up @@ -943,24 +919,24 @@ Module CheriMemory
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
let prov := if CoqSwitches.is_PNVI (SW.get_switches tt)
then Prov_some alloc_id
else Prov_disabled
in
ret (PV prov (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)
Expand All @@ -977,40 +953,40 @@ 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_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);
last_used := st.(last_used);
|})
;;
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)
)).
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);
last_used := st.(last_used);
|})
;;
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.
Expand All @@ -1022,8 +998,7 @@ Module CheriMemory
(ZMap.fold (fun alloc_id alloc acc =>
match acc with
| None =>
if andb (negb alloc.(is_dead))
(AddressValue.eqb alloc.(base) addr)
if AddressValue.eqb alloc.(base) addr && negb alloc.(is_dead)
then Some (alloc_id,alloc)
else None
| Some _ => acc
Expand Down Expand Up @@ -1071,15 +1046,14 @@ Module CheriMemory

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).
Expand Down Expand Up @@ -1126,7 +1100,8 @@ Module CheriMemory

(* 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 supposrted").
Definition zap_pointers {A:Type} (_:storage_instance_id) : memM A
:= raise (InternalErr "zap_pointers is not supported").

Definition is_pointer_algined (a : Z) : bool :=
let v := IMP.get.(alignof_pointer) in
Expand Down Expand Up @@ -1278,7 +1253,7 @@ 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.

Expand Down Expand Up @@ -1559,7 +1534,7 @@ Module CheriMemory
memM (bool* CapGhostState)
:=
(* mprint_msg ("maybe_revoke_pointer " ++ String.hex_str addr) ;; *)
if (negb (fst meta))
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
Expand All @@ -1571,7 +1546,7 @@ Module CheriMemory
| MVEpointer _ (PV _ (PVconcrete c)) =>
let '(t, gs) := meta in
let ptr_base := fst (Bounds.to_Zs (C.cap_get_bounds c)) in
if andb (Z.leb alloc_base ptr_base) (Z.ltb ptr_base alloc_limit)
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.")
Expand Down Expand Up @@ -1662,10 +1637,8 @@ Module CheriMemory
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
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 : storage_instance_id) :=
is_dead_allocation z >>=
Expand Down Expand Up @@ -1697,8 +1670,8 @@ Module CheriMemory
ret tt) ;;
resolve_iota precondition iota >>=
(fun alloc_id =>
(if is_dyn && (CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_revocation INSTANT))
then (get_allocation alloc_id >>= fun alloc => revoke_pointers alloc)
(if is_dyn && CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_revocation INSTANT)
then get_allocation alloc_id >>= fun alloc => revoke_pointers alloc
else ret tt) ;;
update (fun st =>
{|
Expand All @@ -1715,15 +1688,14 @@ Module CheriMemory
last_used := Some alloc_id;
|})
;;
(if CoqSwitches.has_switch (SW.get_switches tt) SW_zap_dead_pointers
then zap_pointers alloc_id
else ret tt)
if CoqSwitches.has_switch (SW.get_switches tt) SW_zap_dead_pointers
then zap_pointers alloc_id
else ret tt
)
| 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
&& CoqSwitches.has_switch (SW.get_switches 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) *)
Expand All @@ -1745,7 +1717,8 @@ Module CheriMemory
raise (InternalErr "Concrete: FREE was called on a dead allocation")
| false =>
get_allocation alloc_id >>= fun alloc =>
if AddressValue.eqb (C.cap_get_value c) alloc.(base) then
if AddressValue.eqb (C.cap_get_value c) alloc.(base)
then
(if is_dyn && (CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_revocation INSTANT))
then revoke_pointers alloc
else ret tt) ;;
Expand All @@ -1764,9 +1737,9 @@ Module CheriMemory
capmeta := st.(capmeta);
last_used := Some alloc_id;
|}) ;;
(if CoqSwitches.has_switch (SW.get_switches tt) SW_zap_dead_pointers
then zap_pointers alloc_id
else ret tt)
if CoqSwitches.has_switch (SW.get_switches tt) SW_zap_dead_pointers
then zap_pointers alloc_id
else ret tt
else
fail loc (MerrUndefinedFree Free_out_of_bound)
end
Expand Down Expand Up @@ -1962,9 +1935,8 @@ Module CheriMemory
;;
mem_value_strip_err loc mval >>=
(fun (mval : mem_value) =>
(if orb
(CoqSwitches.has_switch (SW.get_switches tt) (CoqSwitches.SW_PNVI AE))
(CoqSwitches.has_switch (SW.get_switches 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) =>
Expand Down Expand Up @@ -2457,7 +2429,7 @@ 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_switches tt) CoqSwitches.SW_strict_pointer_relationals then
match
Expand Down Expand Up @@ -2495,7 +2467,7 @@ 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_switches tt) CoqSwitches.SW_strict_pointer_relationals then
match
Expand Down Expand Up @@ -2528,9 +2500,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_switches 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
Expand Down Expand Up @@ -2563,7 +2536,7 @@ 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_switches tt) CoqSwitches.SW_strict_pointer_relationals then
match
Expand Down Expand Up @@ -2659,7 +2632,7 @@ Module CheriMemory
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) =>
Expand Down

0 comments on commit ca875af

Please sign in to comment.