Skip to content

Commit 1151f10

Browse files
vzalivavzaliva
committed
alignment value check in allocate_object and proof sketch
1 parent f33b9b3 commit 1151f10

File tree

2 files changed

+132
-58
lines changed

2 files changed

+132
-58
lines changed

‎coq/CheriMemory/CheriMorelloMemory.v

+59-56
Original file line numberDiff line numberDiff line change
@@ -873,14 +873,17 @@ Module Type CheriMemoryImpl
873873
: memM pointer_value
874874
:=
875875
let align_n := num_of_int int_val in
876-
size_n <- serr2InternalErr (sizeof DEFAULT_FUEL None ty) ;;
877-
let size_z := Z.of_nat size_n in
878-
let mask := C.representable_alignment_mask size_z in
879-
let size_z' := C.representable_length size_z in
880-
let size_n' := Z.to_nat size_z' in
881-
let align_n' := Z.max align_n (1 + (AddressValue.to_Z (AddressValue.bitwise_complement (AddressValue.of_Z mask)))) in
882-
883-
(*
876+
if align_n <=? 0
877+
then raise (InternalErr "non-positive aligment passed to allocate_object")
878+
else
879+
size_n <- serr2InternalErr (sizeof DEFAULT_FUEL None ty) ;;
880+
let size_z := Z.of_nat size_n in
881+
let mask := C.representable_alignment_mask size_z in
882+
let size_z' := C.representable_length size_z in
883+
let size_n' := Z.to_nat size_z' in
884+
let align_n' := Z.max align_n (1 + (AddressValue.to_Z (AddressValue.bitwise_complement (AddressValue.of_Z mask)))) in
885+
886+
(*
884887
(if (negb ((size_n =? size_n') && (align_n =? align_n')))
885888
then
886889
mprint_msg
@@ -891,60 +894,60 @@ Module Type CheriMemoryImpl
891894
", size= " ++ String.dec_str size_n' ++
892895
", align= " ++ String.dec_str align_n')
893896
else ret tt) ;;
894-
*)
897+
*)
895898

896-
(match init_opt with
897-
| None =>
898-
'(alloc_id, addr) <- allocator size_n' align_n' false pref (Some ty) IsWritable ;;
899-
ret (alloc_id, addr, false)
900-
| Some mval => (* here we allocate an object with initiliazer *)
901-
let (ro,readonly_status) :=
902-
match pref with
903-
| CoqSymbol.PrefStringLiteral _ _ => (true, IsReadOnly ReadonlyStringLiteral)
904-
| CoqSymbol.PrefTemporaryLifetime _ _ =>
905-
(true, IsReadOnly ReadonlyTemporaryLifetime)
906-
| _ =>
907-
(true, IsReadOnly ReadonlyConstQualified)
908-
(* | _ => (false,IsWritable) *)
909-
end
910-
in
911-
'(alloc_id, addr) <- allocator size_n' align_n' false pref (Some ty) readonly_status ;;
912-
(* We should be careful not to introduce a state change here
899+
(match init_opt with
900+
| None =>
901+
'(alloc_id, addr) <- allocator size_n' align_n' false pref (Some ty) IsWritable ;;
902+
ret (alloc_id, addr, false)
903+
| Some mval => (* here we allocate an object with initiliazer *)
904+
let (ro,readonly_status) :=
905+
match pref with
906+
| CoqSymbol.PrefStringLiteral _ _ => (true, IsReadOnly ReadonlyStringLiteral)
907+
| CoqSymbol.PrefTemporaryLifetime _ _ =>
908+
(true, IsReadOnly ReadonlyTemporaryLifetime)
909+
| _ =>
910+
(true, IsReadOnly ReadonlyConstQualified)
911+
(* | _ => (false,IsWritable) *)
912+
end
913+
in
914+
'(alloc_id, addr) <- allocator size_n' align_n' false pref (Some ty) readonly_status ;;
915+
(* We should be careful not to introduce a state change here
913916
in case of error which happens after the [allocator]
914917
invocation, as [allocator] modifies state. In the current
915918
implementation, this is not happening, as errors are handled
916919
as [InternalErr] which supposedly should terminate program
917920
evaluation. *)
918-
st <- get ;;
919-
'(funptrmap, capmeta, pre_bs) <- serr2InternalErr (repr DEFAULT_FUEL st.(funptrmap) st.(capmeta) addr mval) ;;
920-
let bs := mapi (fun i b => (AddressValue.with_offset addr (Z.of_nat i), b)) pre_bs in
921-
let bytemap := List.fold_left (fun acc '(addr, b) => AMap.M.add addr b acc) bs st.(bytemap) in
922-
put {|
923-
next_alloc_id := st.(next_alloc_id);
924-
last_address := st.(last_address) ;
925-
allocations := st.(allocations);
926-
funptrmap := funptrmap;
927-
varargs := st.(varargs);
928-
next_varargs_id := st.(next_varargs_id);
929-
bytemap := bytemap;
930-
capmeta := capmeta;
931-
|}
932-
;;
933-
ret (alloc_id, addr, ro)
934-
end)
935-
>>=
936-
fun '(alloc_id, addr, ro) =>
937-
let c := C.alloc_cap addr (AddressValue.of_Z size_z') in
938-
let c :=
939-
if ro then
940-
let p := C.cap_get_perms c in
941-
let p := Permissions.perm_clear_store p in
942-
let p := Permissions.perm_clear_store_cap p in
943-
let p := Permissions.perm_clear_store_local_cap p in
944-
C.cap_narrow_perms c p
945-
else c
946-
in
947-
ret (PVconcrete c).
921+
st <- get ;;
922+
'(funptrmap, capmeta, pre_bs) <- serr2InternalErr (repr DEFAULT_FUEL st.(funptrmap) st.(capmeta) addr mval) ;;
923+
let bs := mapi (fun i b => (AddressValue.with_offset addr (Z.of_nat i), b)) pre_bs in
924+
let bytemap := List.fold_left (fun acc '(addr, b) => AMap.M.add addr b acc) bs st.(bytemap) in
925+
put {|
926+
next_alloc_id := st.(next_alloc_id);
927+
last_address := st.(last_address) ;
928+
allocations := st.(allocations);
929+
funptrmap := funptrmap;
930+
varargs := st.(varargs);
931+
next_varargs_id := st.(next_varargs_id);
932+
bytemap := bytemap;
933+
capmeta := capmeta;
934+
|}
935+
;;
936+
ret (alloc_id, addr, ro)
937+
end)
938+
>>=
939+
fun '(alloc_id, addr, ro) =>
940+
let c := C.alloc_cap addr (AddressValue.of_Z size_z') in
941+
let c :=
942+
if ro then
943+
let p := C.cap_get_perms c in
944+
let p := Permissions.perm_clear_store p in
945+
let p := Permissions.perm_clear_store_cap p in
946+
let p := Permissions.perm_clear_store_local_cap p in
947+
C.cap_narrow_perms c p
948+
else c
949+
in
950+
ret (PVconcrete c).
948951

949952

950953
Definition cap_is_null (c : C.t) : bool :=

‎coq/Proofs/Revocation.v

+73-2
Original file line numberDiff line numberDiff line change
@@ -4105,7 +4105,7 @@ Module CheriMemoryImplWithProofs
41054105
same_state_steps.
41064106
Qed.
41074107

4108-
Instance allocate_object_PreservesInvariant
4108+
Instance allocate_object_PreservesInvariantg
41094109
(tid:MemCommonExe.thread_id)
41104110
(pref:CoqSymbol.prefix)
41114111
(int_val:integer_value)
@@ -4116,7 +4116,78 @@ Module CheriMemoryImplWithProofs
41164116
Proof.
41174117
intros s.
41184118
unfold allocate_object.
4119-
(* TODO: postponed until I figure out readonly logic and re-prove `allocator` *)
4119+
break_if;[preserves_step|].
4120+
preserves_step.
4121+
preserves_step.
4122+
preserves_step.
4123+
-
4124+
break_match_goal; repeat break_let.
4125+
+
4126+
apply bind_PreservesInvariant_value.
4127+
intros H s'0 x0 H0.
4128+
4129+
4130+
assert(mem_invariant s'0) as S0.
4131+
{
4132+
pose proof (allocator_PreservesInvariant (Z.to_nat (Capability_GS.representable_length (Z.of_nat x)))
4133+
(Z.max (num_of_int int_val)
4134+
(1 +
4135+
AddressValue.to_Z
4136+
(AddressValue.bitwise_complement
4137+
(AddressValue.of_Z
4138+
(Capability_GS.representable_alignment_mask (Z.of_nat x))))))
4139+
false pref (Some ty) r
4140+
) as A.
4141+
autospecialize A.
4142+
lia.
4143+
specialize (A s' H).
4144+
unfold post_exec_invariant, lift_sum_p in A.
4145+
clear Heqp.
4146+
break_match_hyp.
4147+
--
4148+
unfold execErrS in Heqs0.
4149+
break_let.
4150+
tuple_inversion.
4151+
invc Heqs0.
4152+
--
4153+
unfold execErrS in Heqs0.
4154+
break_let.
4155+
tuple_inversion.
4156+
apply ret_inr in Heqs0.
4157+
invc Heqs0.
4158+
assumption.
4159+
}
4160+
4161+
split.
4162+
*
4163+
apply S0.
4164+
*
4165+
repeat break_let.
4166+
preserves_step.
4167+
preserves_step.
4168+
preserves_step.
4169+
repeat break_let.
4170+
preserves_step;[|preserves_step].
4171+
preserves_step.
4172+
4173+
bool_to_prop_hyp.
4174+
destruct x1, p0.
4175+
tuple_inversion.
4176+
4177+
(* TODO: need `allocator_capmeta_spec`
4178+
similar to `init_ghost_tags_spec`
4179+
*)
4180+
4181+
admit.
4182+
+
4183+
preserves_step.
4184+
apply allocator_PreservesInvariant.
4185+
lia.
4186+
break_let.
4187+
preserves_step.
4188+
-
4189+
repeat break_let.
4190+
preserves_step.
41204191
Admitted.
41214192

41224193
Instance allocate_region_PreservesInvariant

0 commit comments

Comments
 (0)