Skip to content

Commit 9a91f41

Browse files
andrew-appelandrew-appel
committed
Fix issue #561 (missing check for long-long signed overflow)
and also, fix a bug with extendM that was inadvertently introduced in P.R. #555.
1 parent d3afd1e commit 9a91f41

File tree

5 files changed

+157
-60
lines changed

5 files changed

+157
-60
lines changed

‎msl/predicates_sl.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,7 @@ Qed.
9898

9999
(*Definition compareM : modality
100100
:= exist _ compareR valid_rel_compare.*)
101-
Definition extendM {A}{JA: Join A}{PA: Perm_alg A}{SA : Sep_alg A}{AG: ageable A}{XA: Age_alg A} : modality
101+
Definition extendM (*{A}{JA: Join A}{PA: Perm_alg A}{SA : Sep_alg A}{AG: ageable A}{XA: Age_alg A}*) : modality
102102
:= exist _ extendR valid_rel_extend.
103103

104104
(* Definitions of the BI connectives. *)

‎veric/expr.v

Lines changed: 17 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -286,15 +286,17 @@ Definition tc_nodivover {CS: compspecs} (e1 e2: expr) : tc_assert :=
286286
| _ , _ => tc_nodivover' e1 e2
287287
end.
288288

289-
Definition if_expr_signed (e: expr) (tc: tc_assert) : tc_assert :=
290-
match typeof e with
291-
| Tint _ Signed _ => tc
292-
| Tlong Signed _ => tc
293-
| _ => tc_TT
289+
Definition if_expr_signed (e1 e2 : expr) (tc: tc_assert) : tc_assert :=
290+
match typeof e1, typeof e2 with
291+
| Tint _ Signed _, Tint _ Signed _ => tc
292+
| Tlong Signed _, Tlong Signed _ => tc
293+
| Tint _ _ _, Tlong Signed _ => tc
294+
| Tlong Signed _, Tint _ _ _ => tc
295+
| _, _ => tc_TT
294296
end.
295297

296298
Definition tc_nobinover (op: Z->Z->Z) {CS: compspecs} (e1 e2: expr) : tc_assert :=
297-
if_expr_signed e1
299+
if_expr_signed e1 e2
298300
match eval_expr e1 any_environ, eval_expr e2 any_environ with
299301
| Vint n1, Vint n2 =>
300302
if range_s32 (op (Int.signed n1) (Int.signed n2))
@@ -303,8 +305,15 @@ Definition tc_nobinover (op: Z->Z->Z) {CS: compspecs} (e1 e2: expr) : tc_assert
303305
if range_s64 (op (Int64.signed n1) (Int64.signed n2))
304306
then tc_TT else tc_nosignedover op e1 e2
305307
| Vint n1, Vlong n2 =>
306-
if range_s64 (op (Int.signed n1) (Int64.signed n2))
307-
then tc_TT else tc_nosignedover op e1 e2
308+
match typeof e1 with
309+
| Tint _ Signed _ =>
310+
if range_s64 (op (Int.signed n1) (Int64.signed n2))
311+
then tc_TT
312+
else tc_nosignedover op e1 e2
313+
| _ =>
314+
if range_s64 (op (Int.unsigned n1) (Int64.signed n2))
315+
then tc_TT else tc_nosignedover op e1 e2
316+
end
308317
| Vlong n1, Vint n2 =>
309318
match typeof e2 with
310319
| Tint _ Signed _ =>

‎veric/extend_tc.v

Lines changed: 137 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,7 @@ Proof.
5858
intros.
5959
rewrite denote_tc_assert_andp.
6060
apply boxy_andp; auto.
61+
apply extendM_refl.
6162
Qed.
6263

6364
Lemma extend_tc_bool:
@@ -87,7 +88,6 @@ repeat match goal with |- boxy _ (match ?A with _ => _ end) => destruct A end;
8788
try apply extend_prop.
8889
Qed.
8990

90-
9191
Lemma extend_tc_Zle:
9292
forall {CS: compspecs} v i rho,
9393
boxy extendM (denote_tc_assert (tc_Zle v i) rho).
@@ -131,16 +131,22 @@ rewrite H1 in H.
131131
inv H; auto.
132132
Qed.
133133

134-
Lemma extend_andp: forall P Q,
135-
boxy extendM P -> boxy extendM Q -> boxy extendM (andp P Q).
134+
Lemma extend_andp:
135+
forall {A: Type} {JA : Join A} {PA: Perm_alg A} {SA : Sep_alg A} {AG: ageable A}
136+
{XA: Age_alg A} {EO: Ext_ord A} {EA: Ext_alg A}
137+
(P Q: pred A),
138+
boxy extendM P -> boxy extendM Q -> boxy extendM (andp P Q).
136139
Proof.
137140
intros.
138141
apply boxy_i; intros.
139142
apply extendM_refl.
140143
destruct H2; split; eapply boxy_e; eauto.
141144
Qed.
142145

143-
Lemma extend_orp: forall P Q,
146+
Lemma extend_orp:
147+
forall {A: Type} {JA : Join A} {PA: Perm_alg A} {SA : Sep_alg A} {AG: ageable A}
148+
{XA: Age_alg A} {EO: Ext_ord A} {EA: Ext_alg A}
149+
(P Q: pred A),
144150
boxy extendM P -> boxy extendM Q -> boxy extendM (orp P Q).
145151
Proof.
146152
intros.
@@ -281,27 +287,14 @@ Proof.
281287
intros.
282288
unfold tc_nobinover.
283289
unfold if_expr_signed.
284-
destruct (typeof e1); try apply extend_prop.
285-
destruct s; try apply extend_prop.
290+
destruct (typeof e1) as [ | _ [ | ] _ | [ | ] _ | | | | | | ],
291+
(typeof e2) as [ | _ [ | ] _ | [ | ] _ | | | | | | ];
292+
try apply extend_prop;
286293
destruct (eval_expr e1 any_environ); try apply extend_prop;
287294
destruct (eval_expr e2 any_environ); try apply extend_prop;
288-
try apply extend_tc_nosignedover;
289-
simple_if_tac; try apply extend_prop; try apply extend_tc_nosignedover.
290-
destruct (typeof e2) as [ | _ [ | ] _ | | | | | | | ];
291-
try apply extend_prop.
292-
simple_if_tac; try apply extend_prop; try apply extend_tc_nosignedover.
293-
destruct (typeof e2) as [ | _ [ | ] _ | | | | | | | ];
294295
try apply extend_tc_nosignedover.
296+
all:
295297
simple_if_tac; try apply extend_prop; try apply extend_tc_nosignedover.
296-
try destruct s; try apply extend_prop; try apply extend_tc_nosignedover.
297-
destruct (eval_expr e1 any_environ); try apply extend_prop;
298-
destruct (eval_expr e2 any_environ); try apply extend_prop;
299-
try apply extend_tc_nosignedover.
300-
all: simple_if_tac; try apply extend_prop; try apply extend_tc_nosignedover;
301-
destruct (typeof e2) as [ | _ [ | ] _ | | | | | | | ];
302-
try apply extend_prop;
303-
try apply extend_tc_nosignedover.
304-
all: simple_if_tac; try apply extend_prop; try apply extend_tc_nosignedover.
305298
Qed.
306299

307300
Lemma boxy_orp {A} `{H : ageable A}:
@@ -325,6 +318,7 @@ Proof.
325318
intros.
326319
rewrite denote_tc_assert_orp.
327320
apply boxy_orp; auto.
321+
apply extendM_refl.
328322
Qed.
329323

330324

@@ -356,6 +350,7 @@ Lemma extend_tc_andp':
356350
Proof.
357351
intros.
358352
apply boxy_andp; auto.
353+
apply extendM_refl.
359354
Qed.
360355

361356
Ltac extend_tc_prover :=
@@ -675,25 +670,25 @@ Ltac tc_expr_cenv_sub_tac2 :=
675670
unfold if_expr_signed.
676671
intros.
677672
destruct (typeof a1) as [ | _ [ | ] | [ | ] | [ | ] | | | | | ];
678-
destruct (typeof a2) as [ | _ [ | ] | | | | | | | ];
673+
destruct (typeof a2) as [ | _ [ | ] | [ | ] | | | | | | ];
679674
tc_expr_cenv_sub_tac; repeat tc_expr_cenv_sub_tac2.
680675
Qed.
681676

682-
Lemma tc_expr_cenv_sub a rho Delta w (T: @tc_expr CS Delta a rho w):
683-
@tc_expr CS' Delta a rho w
684-
with tc_lvalue_cenv_sub a rho Delta w (T: @tc_lvalue CS Delta a rho w):
685-
@tc_lvalue CS' Delta a rho w.
686-
Proof.
687-
- clear tc_expr_cenv_sub.
688-
unfold tc_expr in *.
689-
induction a;
690-
try solve [apply (denote_tc_assert_cenv_sub CSUB); auto];
691-
simpl in T|-*;
692-
tc_expr_cenv_sub_tac.
693-
+ (* Ederef *)
694-
destruct (access_mode t) eqn:?H; auto.
677+
Lemma tc_expr_cenv_sub_unop:
678+
forall
679+
(u : unary_operation)
680+
(a : expr)
681+
(t : type)
682+
(rho : environ)
683+
(Delta : tycontext)
684+
(w : rmap)
685+
(T : (@tc_expr CS Delta (Eunop u a t) rho) w)
686+
(IHa : (@tc_expr CS Delta a rho) w -> (@tc_expr CS' Delta a rho) w),
687+
(@tc_expr CS' Delta (Eunop u a t) rho) w.
688+
Proof.
689+
intros.
690+
unfold tc_expr in *; simpl in T|-*.
695691
tc_expr_cenv_sub_tac.
696-
+ (* Eunop *)
697692
destruct u; simpl in H|-*;
698693
destruct (typeof a) as [ | [ | | | ] [ | ] | [ | ] | [ | ] | | | | | ];
699694
tc_expr_cenv_sub_tac.
@@ -712,8 +707,24 @@ Ltac tc_expr_cenv_sub_tac2 :=
712707
apply (denote_tc_nosignedover_eval_expr_cenv_sub CSUB rho
713708
(Econst_long Int64.zero (Ctypes.Tlong Signed a0)) a w Z.sub Unsigned);
714709
auto.
715-
+ (* Ebinop *)
716-
abstract (
710+
Qed.
711+
712+
Lemma tc_expr_cenv_sub_binop:
713+
forall
714+
(b : binary_operation)
715+
(a1 a2 : expr)
716+
(t : type)
717+
(rho : environ)
718+
(Delta : tycontext)
719+
(w : rmap)
720+
(T : (@tc_expr CS Delta (Ebinop b a1 a2 t) rho) w)
721+
(IHa1 : (@tc_expr CS Delta a1 rho) w -> (@tc_expr CS' Delta a1 rho) w)
722+
(IHa2 : (@tc_expr CS Delta a2 rho) w -> (@tc_expr CS' Delta a2 rho) w),
723+
(@tc_expr CS' Delta (Ebinop b a1 a2 t) rho) w.
724+
Proof.
725+
intros.
726+
unfold tc_expr in *; simpl in T|-*.
727+
tc_expr_cenv_sub_tac.
717728
rewrite den_isBinOpR;
718729
rewrite den_isBinOpR in H;
719730
destruct b; simpl in H|-*;
@@ -722,9 +733,23 @@ Ltac tc_expr_cenv_sub_tac2 :=
722733
destruct A; tc_expr_cenv_sub_tac
723734
end;
724735
tc_expr_cenv_sub_tac;
725-
try solve [simple apply tc_nobinover_cenv_sub; auto]).
726-
+ (* Ecast *)
727-
abstract (
736+
try solve [simple apply tc_nobinover_cenv_sub; auto].
737+
Time Qed. (* This Qed takes a really long time *)
738+
739+
Lemma tc_expr_cenv_sub_cast:
740+
forall
741+
(a : expr)
742+
(t : type)
743+
(rho : environ)
744+
(Delta : tycontext)
745+
(w : rmap)
746+
(T : (@tc_expr CS Delta (Ecast a t) rho) w)
747+
(IHa : (@tc_expr CS Delta a rho) w -> (@tc_expr CS' Delta a rho) w),
748+
(@tc_expr CS' Delta (Ecast a t) rho) w.
749+
Proof.
750+
intros.
751+
unfold tc_expr in *; simpl in T|-*.
752+
tc_expr_cenv_sub_tac.
728753
unfold isCastResultType in *;
729754
repeat match goal with |- app_pred (denote_tc_assert match ?A with _ => _ end _) _ =>
730755
destruct A; tc_expr_cenv_sub_tac
@@ -736,8 +761,28 @@ Ltac tc_expr_cenv_sub_tac2 :=
736761
rewrite ?denote_tc_assert_iszero;
737762
destruct (Val.eq (@eval_expr CS a rho) Vundef) as [e|n];
738763
[rewrite e in *; contradiction |
739-
rewrite <- ?(eval_expr_cenv_sub_eq CSUB _ _ n); auto]]).
740-
+ (* Efield *)
764+
rewrite <- ?(eval_expr_cenv_sub_eq CSUB _ _ n); auto]].
765+
Qed.
766+
767+
Lemma tc_expr_cenv_sub_field:
768+
forall
769+
(a : expr)
770+
(tc_lvalue_cenv_sub : forall (rho : environ)
771+
(Delta : tycontext) (w : rmap),
772+
(@tc_lvalue CS Delta a rho) w ->
773+
(@tc_lvalue CS' Delta a rho) w)
774+
(i : ident)
775+
(t : type)
776+
(rho : environ)
777+
(Delta : tycontext)
778+
(w : rmap)
779+
(T : (@tc_expr CS Delta (Efield a i t) rho) w)
780+
(IHa : (@tc_expr CS Delta a rho) w -> (@tc_expr CS' Delta a rho) w),
781+
(@tc_expr CS' Delta (Efield a i t) rho) w.
782+
Proof.
783+
intros.
784+
unfold tc_expr in *; simpl in T|-*.
785+
tc_expr_cenv_sub_tac.
741786
destruct (access_mode t); tc_expr_cenv_sub_tac.
742787
destruct (typeof a); tc_expr_cenv_sub_tac.
743788
*
@@ -758,12 +803,23 @@ Ltac tc_expr_cenv_sub_tac2 :=
758803
intros. specialize (CSUB id). hnf in CSUB. rewrite H3 in CSUB; auto.
759804
apply co_consistent_complete.
760805
apply (cenv_consistent i0); auto.
761-
- clear tc_lvalue_cenv_sub.
762-
unfold tc_lvalue in *.
763-
induction a;
764-
try solve [apply (denote_tc_assert_cenv_sub CSUB); auto];
765-
simpl in T|-*;
766-
tc_expr_cenv_sub_tac.
806+
Qed.
807+
808+
Lemma tc_lvalue_cenv_sub_field:
809+
forall
810+
(a : expr)
811+
(i : ident)
812+
(t : type)
813+
(rho : environ)
814+
(Delta : tycontext)
815+
(w : rmap)
816+
(T : (@denote_tc_assert CS (@typecheck_lvalue CS Delta (Efield a i t)) rho) w)
817+
(IHa : (@denote_tc_assert CS (@typecheck_lvalue CS Delta a) rho) w ->
818+
(@denote_tc_assert CS' (@typecheck_lvalue CS' Delta a) rho) w),
819+
(@denote_tc_assert CS' (@typecheck_lvalue CS' Delta (Efield a i t)) rho) w.
820+
Proof.
821+
intros.
822+
simpl in T|-*; tc_expr_cenv_sub_tac.
767823
destruct (typeof a); tc_expr_cenv_sub_tac.
768824
*
769825
destruct ((@cenv_cs CS) ! i0) eqn:?; try contradiction.
@@ -785,6 +841,38 @@ Ltac tc_expr_cenv_sub_tac2 :=
785841
apply (cenv_consistent i0); auto.
786842
Qed.
787843

844+
Lemma tc_expr_cenv_sub a rho Delta w (T: @tc_expr CS Delta a rho w):
845+
@tc_expr CS' Delta a rho w
846+
with tc_lvalue_cenv_sub a rho Delta w (T: @tc_lvalue CS Delta a rho w):
847+
@tc_lvalue CS' Delta a rho w.
848+
Proof.
849+
- clear tc_expr_cenv_sub.
850+
induction a;
851+
try solve [apply (denote_tc_assert_cenv_sub CSUB); auto];
852+
try solve [unfold tc_expr in *; simpl in T|-*; tc_expr_cenv_sub_tac].
853+
+ (* Ederef *)
854+
unfold tc_expr in *; simpl in T|-*.
855+
destruct (access_mode t) eqn:?H; auto.
856+
tc_expr_cenv_sub_tac.
857+
+ (* Eunop *)
858+
apply (tc_expr_cenv_sub_unop _ _ _ _ _ _ T IHa).
859+
+ (* Ebinop *)
860+
apply (tc_expr_cenv_sub_binop _ _ _ _ _ _ _ T IHa1 IHa2).
861+
+ (* Ecast *)
862+
apply (tc_expr_cenv_sub_cast _ _ _ _ _ T IHa).
863+
+ (* Efield *)
864+
apply (tc_expr_cenv_sub_field a (tc_lvalue_cenv_sub a) _ _ _ _ _ T IHa).
865+
- clear tc_lvalue_cenv_sub.
866+
unfold tc_lvalue in *.
867+
induction a;
868+
try solve [apply (denote_tc_assert_cenv_sub CSUB); auto].
869+
+ (* Ederef *)
870+
simpl in T|-*;
871+
tc_expr_cenv_sub_tac.
872+
+ (* Efield *)
873+
apply (tc_lvalue_cenv_sub_field _ _ _ _ _ _ T IHa).
874+
Time Qed.
875+
788876
Lemma tc_exprlist_cenv_sub Delta rho w:
789877
forall types bl, (@tc_exprlist CS Delta types bl rho) w ->
790878
(@tc_exprlist CS' Delta types bl rho) w.

‎veric/semax_call.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3764,7 +3764,7 @@ simpl; intros ? ?. unfold cl_after_external. destruct ret0; auto.
37643764
reflexivity.
37653765
intros.
37663766
destruct H8 as [w1 [w2 [H8' [_ ?]]]]. subst m'.
3767-
assert (H8'': @extendM rmap _ _ _ _ _ _ rmap _ _ _ _ _ w2 a'') by (eexists; eauto). clear H8'.
3767+
assert (H8'': extendM w2 a'') by (eexists; eauto). clear H8'.
37683768
remember (construct_rho (filter_genv psi) vx tx) as rho.
37693769
assert (H7': typecheck_environ Delta rho).
37703770
destruct H7; eapply typecheck_environ_sub; eauto.

‎veric/semax_straight.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ Section extensions.
3030

3131
Lemma semax_straight_simple:
3232
forall Delta (B: assert) P c Q,
33-
(forall rho, boxy (@extendM rmap _ _ _ _ _ _ rmap _ _ _ _ _) (B rho)) ->
33+
(forall rho, boxy extendM (B rho)) ->
3434
(forall jm jm1 Delta' ge ve te rho k F f,
3535
tycontext_sub Delta Delta' ->
3636
app_pred (B rho) (m_phi jm) ->

0 commit comments

Comments
 (0)