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 ++++++++++++++++++++--------------- 1 file changed, 20 insertions(+), 15 deletions(-) (limited to 'backend/CSE3analysis.v') 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. -- cgit