diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 08:17:40 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 08:17:40 +0100 |
commit | 1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68 (patch) | |
tree | 210ffc156c83f04fb0c61a40b4f9037d7ba8a7e1 /common | |
parent | 222c9047d61961db9c6b19fed5ca49829223fd33 (diff) | |
parent | 12be46d59a2483a10d77fa8ee67f7e0ca1bd702f (diff) | |
download | compcert-kvx-1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68.tar.gz compcert-kvx-1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68.zip |
Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
Diffstat (limited to 'common')
-rw-r--r-- | common/AST.v | 29 | ||||
-rw-r--r-- | common/Memory.v | 129 | ||||
-rw-r--r-- | common/PrintAST.ml | 4 | ||||
-rw-r--r-- | common/Switchaux.ml | 3 | ||||
-rw-r--r-- | common/Values.v | 106 |
5 files changed, 269 insertions, 2 deletions
diff --git a/common/AST.v b/common/AST.v index fcbf0b34..eb34d675 100644 --- a/common/AST.v +++ b/common/AST.v @@ -17,7 +17,7 @@ the abstract syntax trees of many of the intermediate languages. *) Require Import String. -Require Import Coqlib Maps Errors Integers Floats. +Require Import Coqlib Maps Errors Integers Floats BinPos. Require Archi. Set Implicit Arguments. @@ -232,6 +232,16 @@ Definition chunk_of_type (ty: typ) := Lemma chunk_of_Tptr: chunk_of_type Tptr = Mptr. Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed. +(** Trapping mode: does undefined behavior result in a trap or an undefined value (e.g. for loads) *) +Inductive trapping_mode : Type := TRAP | NOTRAP. + +Definition trapping_mode_eq : forall x y : trapping_mode, + { x=y } + { x <> y}. +Proof. + decide equality. +Defined. + + (** Initialization data for global variables. *) Inductive init_data: Type := @@ -669,11 +679,28 @@ Inductive builtin_arg (A: Type) : Type := | BA_splitlong (hi lo: builtin_arg A) | BA_addptr (a1 a2: builtin_arg A). +Definition builtin_arg_eq {A: Type}: + (forall x y : A, {x = y} + {x <> y}) -> + forall (ba1 ba2: (builtin_arg A)), {ba1=ba2} + {ba1<>ba2}. +Proof. + intro. generalize Integers.int_eq int64_eq float_eq float32_eq chunk_eq ptrofs_eq ident_eq. + decide equality. +Defined. +Global Opaque builtin_arg_eq. + Inductive builtin_res (A: Type) : Type := | BR (x: A) | BR_none | BR_splitlong (hi lo: builtin_res A). +Definition builtin_res_eq {A: Type}: + (forall x y : A, {x = y} + {x <> y}) -> + forall (a b: builtin_res A), {a=b} + {a<>b}. +Proof. + intro. decide equality. +Defined. +Global Opaque builtin_res_eq. + Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident := match a with | BA_loadglobal chunk id ofs => id :: nil diff --git a/common/Memory.v b/common/Memory.v index 9f9934c2..f21d99af 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -38,6 +38,10 @@ Require Import Floats. Require Import Values. Require Export Memdata. Require Export Memtype. +Require Import Lia. + +Definition default_notrap_load_value (chunk : memory_chunk) := Vundef. + (* To avoid useless definitions of inductors in extracted code. *) Local Unset Elimination Schemes. @@ -538,6 +542,48 @@ Proof. induction vl; simpl; intros. auto. rewrite IHvl. auto. Qed. +Remark set_setN_swap_disjoint: + forall vl: list memval, + forall v: memval, + forall m : ZMap.t memval, + forall p pl: Z, + ~ (Intv.In p (pl, pl + Z.of_nat (length vl))) -> + (setN vl pl (ZMap.set p v m)) = (ZMap.set p v (setN vl pl m)). +Proof. + induction vl; simpl; trivial. + intros. + unfold Intv.In in *; simpl in *. + rewrite ZMap.set_disjoint by lia. + apply IHvl. + lia. +Qed. + +Lemma setN_swap_disjoint: + forall vl1 vl2: list memval, + forall m : ZMap.t memval, + forall p1 p2: Z, + Intv.disjoint (p1, p1 + Z.of_nat (length vl1)) + (p2, p2 + Z.of_nat (length vl2)) -> + (setN vl1 p1 (setN vl2 p2 m)) = (setN vl2 p2 (setN vl1 p1 m)). +Proof. + induction vl1; simpl; trivial. + intros until p2. intro DISJOINT. + rewrite <- set_setN_swap_disjoint. + { rewrite IHvl1. + reflexivity. + unfold Intv.disjoint, Intv.In in *. + simpl in *. + intro. + intro BOUNDS. + apply DISJOINT. + lia. + } + unfold Intv.disjoint, Intv.In in *. + simpl in *. + apply DISJOINT. + lia. +Qed. + (** [store chunk m b ofs v] perform a write in memory state [m]. Value [v] is stored at address [b] and offset [ofs]. Return the updated memory store, or [None] if the accessed bytes @@ -1178,6 +1224,89 @@ Local Hint Resolve store_valid_block_1 store_valid_block_2: mem. Local Hint Resolve store_valid_access_1 store_valid_access_2 store_valid_access_3: mem. +Remark mem_same_proof_irr : + forall m1 m2 : mem, + (mem_contents m1) = (mem_contents m2) -> + (mem_access m1) = (mem_access m2) -> + (nextblock m1) = (nextblock m2) -> + m1 = m2. +Proof. + destruct m1 as [contents1 access1 nextblock1 access_max1 nextblock_noaccess1 default1]. + destruct m2 as [contents2 access2 nextblock2 access_max2 nextblock_noaccess2 default2]. + simpl. + intros. + subst contents2. + subst access2. + subst nextblock2. + f_equal; apply proof_irr. +Qed. + +Theorem store_store_other: + forall chunk b ofs v chunk' b' ofs' v' m0 m1 m1', + b' <> b + \/ ofs' + size_chunk chunk' <= ofs + \/ ofs + size_chunk chunk <= ofs' -> + store chunk m0 b ofs v = Some m1 -> + store chunk' m0 b' ofs' v' = Some m1' -> + store chunk' m1 b' ofs' v' = + store chunk m1' b ofs v. +Proof. + intros until m1'. + intro DISJOINT. + intros W0 W0'. + assert (valid_access m1' chunk b ofs Writable) as WRITEABLE1' by eauto with mem. + (* { + eapply store_valid_access_1. + apply W0'. + eapply store_valid_access_3. + apply W0. + } *) + assert (valid_access m1 chunk' b' ofs' Writable) as WRITABLE1 by eauto with mem. + (* { + eapply store_valid_access_1. + apply W0. + eapply store_valid_access_3. + apply W0'. + } *) + unfold store in *. + destruct (valid_access_dec m0 chunk b ofs Writable). + 2: congruence. + destruct (valid_access_dec m1 chunk' b' ofs' Writable). + 2: contradiction. + destruct (valid_access_dec m0 chunk' b' ofs' Writable). + 2: congruence. + destruct (valid_access_dec m1' chunk b ofs Writable). + 2: contradiction. + f_equal. + inv W0; simpl in *. + inv W0'; simpl in *. + apply mem_same_proof_irr; simpl; trivial. + destruct (eq_block b b'). + { subst b'. + rewrite PMap.gss. + rewrite PMap.gss. + rewrite PMap.set2. + rewrite PMap.set2. + f_equal. + apply setN_swap_disjoint. + unfold Intv.disjoint. + rewrite encode_val_length. + rewrite <- size_chunk_conv. + rewrite encode_val_length. + rewrite <- size_chunk_conv. + unfold Intv.In; simpl. + intros. + destruct DISJOINT. contradiction. + lia. + } + { + rewrite PMap.set_disjoint by congruence. + rewrite PMap.gso by congruence. + rewrite PMap.gso by congruence. + reflexivity. + } +Qed. + Lemma load_store_overlap: forall chunk m1 b ofs v m2 chunk' ofs' v', store chunk m1 b ofs v = Some m2 -> diff --git a/common/PrintAST.ml b/common/PrintAST.ml index cf3a17d5..3f718428 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -98,3 +98,7 @@ let rec print_builtin_res px oc = function fprintf oc "splitlong(%a, %a)" (print_builtin_res px) hi (print_builtin_res px) lo +let print_trapping_mode oc = function + | TRAP -> () + | NOTRAP -> output_string oc " [notrap]" + diff --git a/common/Switchaux.ml b/common/Switchaux.ml index 4035e299..1744a932 100644 --- a/common/Switchaux.ml +++ b/common/Switchaux.ml @@ -80,6 +80,7 @@ let compile_switch_as_jumptable default cases minkey maxkey = CTaction default) let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) = + (* DM Settings this to constant false disables jump tables *) let span = Z.sub maxkey minkey in assert (Z.ge span Z.zero); let tree_size = Z.mul (Z.of_uint 4) (Z.of_uint numcases) @@ -87,7 +88,7 @@ let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) = numcases >= 7 (* small jump tables are always less efficient *) && Z.le table_size tree_size && Z.lt span (Z.of_uint Sys.max_array_length) - + let compile_switch modulus default table = let (tbl, keys) = normalize_table table in if ZSet.is_empty keys then CTaction default else begin diff --git a/common/Values.v b/common/Values.v index 68a2054b..6401ba52 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1470,6 +1470,60 @@ Proof. assert (32 < Int.max_unsigned) by reflexivity. omega. Qed. +Theorem shrx1_shr: + forall x z, + shrx x (Vint (Int.repr 1)) = Some z -> + z = shr (add x (shru x (Vint (Int.repr 31)))) (Vint (Int.repr 1)). +Proof. + intros. destruct x; simpl in H; try discriminate. + change (Int.ltu (Int.repr 1) (Int.repr 31)) with true in H; simpl in H. + inversion_clear H. + simpl. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true; simpl. + change (Int.ltu (Int.repr 1) Int.iwordsize) with true; simpl. + f_equal. + rewrite Int.shrx1_shr by reflexivity. + reflexivity. +Qed. + +Theorem shrx_shr_3: + forall n x z, + shrx x (Vint n) = Some z -> + z = (if Int.eq n Int.zero then x else + if Int.eq n Int.one + then shr (add x (shru x (Vint (Int.repr 31)))) (Vint Int.one) + else shr (add x (shru (shr x (Vint (Int.repr 31))) + (Vint (Int.sub (Int.repr 32) n)))) + (Vint n)). +Proof. + intros. destruct x; simpl in H; try discriminate. + destruct (Int.ltu n (Int.repr 31)) eqn:LT; inv H. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31; intros LT'. + predSpec Int.eq Int.eq_spec n Int.zero. +- subst n. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs. change (Int.signed Int.one) with 1. + rewrite Z.quot_1_r. rewrite Int.repr_signed; auto. +- predSpec Int.eq Int.eq_spec n Int.one. + * subst n. simpl. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. + change (Int.ltu Int.one Int.iwordsize) with true. simpl. + f_equal. + apply Int.shrx1_shr. + reflexivity. + * clear H0. + simpl. change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. + replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl. + replace (Int.ltu n Int.iwordsize) with true. + f_equal; apply Int.shrx_shr_2; assumption. + symmetry; apply zlt_true. change (Int.unsigned n < 32); omega. + symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32. + assert (Int.unsigned n <> 0). + { red; intros; elim H. + rewrite <- (Int.repr_unsigned n), H0. auto. } + rewrite Int.unsigned_repr. + change (Int.unsigned Int.iwordsize) with 32; omega. + assert (32 < Int.max_unsigned) by reflexivity. omega. +Qed. + Theorem or_rolm: forall x n m1 m2, or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2). @@ -1729,6 +1783,58 @@ Proof. assert (64 < Int.max_unsigned) by reflexivity. omega. Qed. +Theorem shrxl1_shrl: + forall x z, + shrxl x (Vint (Int.repr 1)) = Some z -> + z = shrl (addl x (shrlu x (Vint (Int.repr 63)))) (Vint (Int.repr 1)). +Proof. + intros. destruct x; simpl in H; try discriminate. + change (Int.ltu (Int.repr 1) (Int.repr 63)) with true in H; simpl in H. + inversion_clear H. + simpl. + change (Int.ltu (Int.repr 63) Int64.iwordsize') with true; simpl. + change (Int.ltu (Int.repr 1) Int64.iwordsize') with true; simpl. + f_equal. + rewrite Int64.shrx'1_shr' by reflexivity. + reflexivity. +Qed. + +Theorem shrxl_shrl_3: + forall n x z, + shrxl x (Vint n) = Some z -> + z = (if Int.eq n Int.zero then x else + if Int.eq n Int.one + then shrl (addl x (shrlu x (Vint (Int.repr 63)))) (Vint Int.one) + else shrl (addl x (shrlu (shrl x (Vint (Int.repr 63))) + (Vint (Int.sub (Int.repr 64) n)))) + (Vint n)). +Proof. + intros. destruct x; simpl in H; try discriminate. + destruct (Int.ltu n (Int.repr 63)) eqn:LT; inv H. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 63)) with 63; intros LT'. + predSpec Int.eq Int.eq_spec n Int.zero. +- subst n. unfold Int64.shrx'. rewrite Int64.shl'_zero. unfold Int64.divs. change (Int64.signed Int64.one) with 1. + rewrite Z.quot_1_r. rewrite Int64.repr_signed; auto. +- predSpec Int.eq Int.eq_spec n Int.one. + * subst n. simpl. + change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl. + change (Int.ltu Int.one Int64.iwordsize') with true. simpl. + f_equal. + apply Int64.shrx'1_shr'. + reflexivity. + * clear H0. +simpl. change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl. + replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl. + replace (Int.ltu n Int64.iwordsize') with true. + f_equal; apply Int64.shrx'_shr_2; assumption. + symmetry; apply zlt_true. change (Int.unsigned n < 64); omega. + symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64. + assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } + rewrite Int.unsigned_repr. + change (Int.unsigned Int64.iwordsize') with 64; omega. + assert (64 < Int.max_unsigned) by reflexivity. omega. +Qed. + Theorem negate_cmp_bool: forall c x y, cmp_bool (negate_comparison c) x y = option_map negb (cmp_bool c x y). Proof. |