diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-12 19:31:42 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-12 19:31:42 +0100 |
commit | 7ead22b0a04fbea3fb0ef99ba3528460f0d6bd67 (patch) | |
tree | 6700f03c7ff29d2ff7afedb7f42828b07ac98ba2 /backend | |
parent | 560c9837eee2145e3a9763aa2e37a6eb34c7e9ac (diff) | |
download | compcert-kvx-7ead22b0a04fbea3fb0ef99ba3528460f0d6bd67.tar.gz compcert-kvx-7ead22b0a04fbea3fb0ef99ba3528460f0d6bd67.zip |
CSE3 analysis
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CSE3.v | 2 | ||||
-rw-r--r-- | backend/CSE3analysis.v | 10 | ||||
-rw-r--r-- | backend/CSE3analysisproof.v | 75 |
3 files changed, 81 insertions, 6 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v index d54b9ffa..f8a25515 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -69,7 +69,7 @@ Definition transf_function (f: function) : res function := do tenv <- type_function f; let (invariants, hints) := preanalysis tenv f in let ctx := context_from_hints hints in - if check_inductiveness (ctx:=ctx) tenv invariants f + if check_inductiveness (ctx:=ctx) f tenv invariants then OK {| fn_sig := f.(fn_sig); fn_params := f.(fn_params); diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 43c44ccd..76723f40 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -331,16 +331,16 @@ Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : RB.t Definition invariants := PMap.t RB.t. -Definition rel_le (x y : RELATION.t) : bool := (PSet.is_subset y x). +Definition rel_leb (x y : RELATION.t) : bool := (PSet.is_subset y x). -Definition relb_le (x y : RB.t) : bool := +Definition relb_leb (x y : RB.t) : bool := match x, y with | None, _ => true | (Some _), None => false - | (Some x), (Some y) => rel_le x y + | (Some x), (Some y) => rel_leb x y end. -Definition check_inductiveness (tenv: typing_env) (inv: invariants) (fn : RTL.function) := +Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: invariants) := (RB.beq (Some RELATION.top) (PMap.get (fn_entrypoint fn) inv)) && PTree_Properties.for_all (fn_code fn) (fun pc instr => @@ -349,7 +349,7 @@ Definition check_inductiveness (tenv: typing_env) (inv: invariants) (fn : RTL.fu | Some rel => let rel' := apply_instr pc tenv instr rel in List.forallb - (fun pc' => relb_le rel' (PMap.get pc' inv)) + (fun pc' => relb_leb rel' (PMap.get pc' inv)) (RTL.successors_instr instr) end). diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 05c7a8f3..5514c532 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -10,6 +10,26 @@ Require Import CSE3analysis CSE2deps CSE2depsproof HashedSet. Require Import RTLtyping. Require Import Lia. +Lemma rel_leb_correct: + forall x x', + rel_leb x x' = true <-> RELATION.ge x' x. +Proof. + unfold rel_leb, RELATION.ge. + split; auto. +Qed. + +Hint Resolve rel_leb_correct : cse3. + +Lemma relb_leb_correct: + forall x x', + relb_leb x x' = true <-> RB.ge x' x. +Proof. + unfold relb_leb, RB.ge. + destruct x; destruct x'; split; trivial; try contradiction; discriminate. +Qed. + +Hint Resolve relb_leb_correct : cse3. + Theorem loadv_storev_really_same: forall chunk: memory_chunk, forall m1: mem, @@ -708,4 +728,59 @@ Section SOUNDNESS. rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. assumption. Qed. + + Hint Resolve store_sound : cse3. + + Section INDUCTIVENESS. + Variable fn : RTL.function. + Variable tenv : typing_env. + Variable inv: invariants. + + Definition is_inductive_step (pc pc' : node) := + forall instr, + PTree.get pc (fn_code fn) = Some instr -> + In pc' (successors_instr instr) -> + RB.ge (PMap.get pc' inv) + (apply_instr' (ctx:=ctx) tenv (fn_code fn) pc (PMap.get pc inv)). + + Definition is_inductive_allstep := + forall pc pc', is_inductive_step pc pc'. + + Lemma checked_is_inductive_allstep: + (check_inductiveness (ctx:=ctx) fn tenv inv) = true -> + is_inductive_allstep. + Proof. + unfold check_inductiveness, is_inductive_allstep, is_inductive_step. + rewrite andb_true_iff. + rewrite PTree_Properties.for_all_correct. + intros (ENTRYPOINT & ALL). + intros until instr. + intros INSTR IN_SUCC. + specialize ALL with (x := pc) (a := instr). + pose proof (ALL INSTR) as AT_PC. + destruct (inv # pc). + 2: apply RB.ge_bot. + rewrite List.forallb_forall in AT_PC. + unfold apply_instr'. + rewrite INSTR. + apply relb_leb_correct. + auto. + Qed. + + Lemma checked_is_inductive_entry: + (check_inductiveness (ctx:=ctx) fn tenv inv) = true -> + inv # (fn_entrypoint fn) = Some RELATION.top. + Proof. + unfold check_inductiveness, is_inductive_allstep, is_inductive_step. + rewrite andb_true_iff. + intros (ENTRYPOINT & ALL). + apply RB.beq_correct in ENTRYPOINT. + unfold RB.eq, RELATION.eq in ENTRYPOINT. + destruct (inv # (fn_entrypoint fn)) as [rel | ]. + 2: contradiction. + f_equal. + symmetry. + assumption. + Qed. + End INDUCTIVENESS. End SOUNDNESS. |