From d7213cfdef90fc3ebc5f57ae18277d7b4c9dd126 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 8 Dec 2020 20:16:47 +0100 Subject: analysis with Abst_same --- backend/CSE3analysis.v | 35 ++++++++++++++++++++--------------- backend/CSE3analysisproof.v | 14 ++++++++++---- backend/CSE3proof.v | 12 +++++++++--- 3 files changed, 39 insertions(+), 22 deletions(-) diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index bcdebca7..8cfbaaa1 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -127,6 +127,9 @@ End RELATION. Module RB := ADD_BOTTOM(RELATION). Module DS := Dataflow_Solver(RB)(NodeSetForward). +Inductive abst_insn_out := +| Abst_same : RB.t -> abst_insn_out. + Inductive sym_op : Type := | SOp : operation -> sym_op | SLoad : memory_chunk -> addressing -> sym_op. @@ -461,27 +464,27 @@ Section OPERATIONS. | _ => rel end. - Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t := + Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : abst_insn_out := match instr with | Inop _ | Icond _ _ _ _ _ - | Ijumptable _ _ => Some rel + | Ijumptable _ _ => Abst_same (Some rel) | Istore chunk addr args src _ => - Some (store tenv chunk addr args src rel) - | Iop op args dst _ => Some (oper dst (SOp op) args rel) - | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel) - | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) - | Ibuiltin ef _ res _ => Some (kill_builtin_res res (apply_external_call ef rel)) - | Itailcall _ _ _ | Ireturn _ => RB.bot + Abst_same (Some (store tenv chunk addr args src rel)) + | Iop op args dst _ => Abst_same (Some (oper dst (SOp op) args rel)) + | Iload trap chunk addr args dst _ => Abst_same (Some (oper dst (SLoad chunk addr) args rel)) + | Icall _ _ _ dst _ => Abst_same (Some (kill_reg dst (kill_mem rel))) + | Ibuiltin ef _ res _ => Abst_same (Some (kill_builtin_res res (apply_external_call ef rel))) + | Itailcall _ _ _ | Ireturn _ => Abst_same RB.bot end. End PER_NODE. -Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : RB.t := +Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : abst_insn_out := match ro with - | None => None + | None => Abst_same RB.bot | Some x => match code ! pc with - | None => RB.bot + | None => Abst_same RB.bot | Some instr => apply_instr pc tenv instr x end end. @@ -504,10 +507,12 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva match PMap.get pc inv with | None => true | Some rel => - let rel' := apply_instr pc tenv instr rel in - List.forallb - (fun pc' => relb_leb rel' (PMap.get pc' inv)) - (RTL.successors_instr instr) + match apply_instr pc tenv instr rel with + | Abst_same rel' => + List.forallb + (fun pc' => relb_leb rel' (PMap.get pc' inv)) + (RTL.successors_instr instr) + end end). (* No longer used. Incompatible with transfer functions that yield a different result depending on the successor. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 7e456748..10ffe760 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1298,7 +1298,10 @@ Section SOUNDNESS. 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)). + (match apply_instr' (ctx:=ctx) tenv (fn_code fn) pc + (PMap.get pc inv) with + | Abst_same rel' => rel' + end). Definition is_inductive_allstep := forall pc pc', is_inductive_step pc pc'. @@ -1317,11 +1320,14 @@ Section SOUNDNESS. 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. + destruct apply_instr. + { (* same *) + rewrite List.forallb_forall in AT_PC. + apply relb_leb_correct. + auto. + } Qed. Lemma checked_is_inductive_entry: diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 7af62b95..9a55f529 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -449,6 +449,7 @@ Lemma step_simulation: exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. Proof. induction 1; intros S1' MS; inv MS. + all: try set (ctx := (context_from_hints (snd (preanalysis tenv f)))). - (* Inop *) exists (State ts tf sp pc' rs m). split. + apply exec_Inop; auto. @@ -779,9 +780,14 @@ Proof. cbn in IND. rewrite H in IND. assert (RB.ge (fst (preanalysis tenv f)) # (if b then ifso else ifnot) - match (fst (preanalysis tenv f)) # pc with - | Some x => apply_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc tenv (Icond cond args ifso ifnot predb) x - | None => None + match + match (fst (preanalysis tenv f)) # pc with + | Some x => + apply_instr (ctx:=ctx) pc tenv (Icond cond args ifso ifnot predb) x + | None => Abst_same RB.bot + end + with + | Abst_same rel' => rel' end) as INDUCTIVE by (destruct b; intuition). clear IND. -- cgit