Skip to content

Commit

Permalink
Prov_default handling
Browse files Browse the repository at this point in the history
  • Loading branch information
@vzaliva
vzaliva committed Jul 27, 2023
1 parent 40cd34e commit 0f66dd7
Show file tree
Hide file tree
Showing 2 changed files with 71 additions and 41 deletions.
66 changes: 49 additions & 17 deletions coq/CheriMemory/CheriMemory.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -740,16 +740,21 @@ Module CheriMemory
match fuel with
| O => raise "out of fuel in repr"
| S fuel =>
let default_prov :=
if CoqSwitches.is_PNVI (SW.get_switches tt)
then Prov_none
else Prov_disabled
in
match mval with
| 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 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 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) ;;
Expand All @@ -760,11 +765,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 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 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_) =>
Expand Down Expand Up @@ -803,7 +808,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 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
Expand Down Expand Up @@ -833,7 +838,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 None None))))
end
end.

Expand Down Expand Up @@ -870,7 +875,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
Expand Down Expand Up @@ -1140,6 +1145,11 @@ Module CheriMemory
match bs with
| [] => raise "CHERI.AbsByte.split_bytes: called on an empty list"
| bs =>
let default_prov :=
if CoqSwitches.is_PNVI (SW.get_switches tt)
then Prov_none
else Prov_disabled
in
'(_prov, rev_values, offset_status) <-
monadic_fold_left
(fun '(prov_acc, val_acc, offset_acc) b_value =>
Expand Down Expand Up @@ -1170,6 +1180,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
Expand All @@ -1188,10 +1202,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), nil, (PtrBytes 0)) ;;

let pvalid := match _prov with
| INVALID => Prov_none
| INVALID => Prov_disabled
| VALID z_value => z_value
end in

Expand All @@ -1209,11 +1223,12 @@ Module CheriMemory
(fun (acc : list storage_instance_id) =>
fun (b_value : AbsByte) =>
match b_value.(prov) with
| Prov_disabled => acc
| 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
Expand Down Expand Up @@ -1418,11 +1433,16 @@ Module CheriMemory
(base_addr : Z)
(n_bytes : Z) : list AbsByte
:=
let default_prov :=
if CoqSwitches.is_PNVI (SW.get_switches tt)
then Prov_none
else Prov_disabled
in
List.map
(fun (addr : Z.t) =>
match ZMap.find addr bytemap with
| Some b_value => b_value
| None => absbyte_v Prov_none None None
| None => absbyte_v default_prov None None
end)
(list_init (Z.to_nat n_bytes)
(fun (i : nat) =>
Expand Down Expand Up @@ -2290,11 +2310,21 @@ Module CheriMemory

Definition null_ptrval (_:CoqCtype.ctype) : pointer_value
:=
PV Prov_none (PVconcrete (C.cap_c0 tt)).
let default_prov :=
if CoqSwitches.is_PNVI (SW.get_switches tt)
then Prov_none
else Prov_disabled
in
PV default_prov (PVconcrete (C.cap_c0 tt)).

Definition fun_ptrval (sym : CoqSymbol.sym)
: serr pointer_value :=
ret (PV Prov_none (PVfunction (FP_valid sym))).
let default_prov :=
if CoqSwitches.is_PNVI (SW.get_switches tt)
then Prov_none
else Prov_disabled
in
ret (PV default_prov (PVfunction (FP_valid sym))).

Definition concrete_ptrval : Z -> AddressValue.t -> serr pointer_value :=
fun _ _ =>
Expand Down Expand Up @@ -3881,7 +3911,9 @@ Module CheriMemory
end.

Definition cornucopiaRevoke (_:unit) : memM unit
:= ret tt. (* TODO *)
:=
mprint_msg "cornucopiaRevoke" ;;
ret tt. (* TODO *)

Definition call_intrinsic
(loc : location_ocaml) (name : string) (args : list mem_value)
Expand Down
46 changes: 22 additions & 24 deletions memory/cheri-coq/impl_mem.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1087,7 +1087,8 @@ module CHERIMorello : Memory = struct
if MM.cap_is_null c
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
Expand Down Expand Up @@ -1183,29 +1184,26 @@ module CHERIMorello : Memory = struct
| _ ->
return None
end)
| Prov_none ->
if Switches.is_PNVI ()
then return None
else
begin match pv with
| PVconcrete c ->
let addr = C.cap_get_value c in
bind (lift_coq_memM ~quiet:true "find_overlapping" (MM.find_overlaping 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 ~quiet:true "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
| Prov_disabled ->
begin match pv with
| PVconcrete c ->
let addr = C.cap_get_value c in
bind (lift_coq_memM ~quiet:true "find_overlapping" (MM.find_overlaping 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 ~quiet:true "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

Expand Down

0 comments on commit 0f66dd7

Please sign in to comment.