From c6ebd73465ef895c6ea5e240f9c784463a6a0fe5 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 12 Mar 2020 16:46:06 +0100 Subject: removed second analysis phase --- backend/CSE3.v | 33 ++++++++++----------------------- backend/CSE3analysis.v | 4 +++- backend/CSE3analysisaux.ml | 15 +++++++++------ backend/CSE3proof.v | 2 ++ extraction/extraction.v | 2 +- 5 files changed, 25 insertions(+), 31 deletions(-) diff --git a/backend/CSE3.v b/backend/CSE3.v index 2ef16376..e82b7cdb 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -6,31 +6,21 @@ Require Import RTLtyping. Local Open Scope error_monad_scope. -Axiom preanalysis : typing_env -> RTL.function -> analysis_hints. - -Definition run f := preanalysis f. +Axiom preanalysis : typing_env -> RTL.function -> invariants * analysis_hints. Section REWRITE. Context {ctx : eq_context}. Definition find_op_in_fmap fmap pc op args := - match fmap with + match PMap.get pc fmap with + | Some rel => rhs_find (ctx:=ctx) pc (SOp op) args rel | None => None - | Some map => - match PMap.get pc map with - | Some rel => rhs_find (ctx:=ctx) pc (SOp op) args rel - | None => None - end end. Definition find_load_in_fmap fmap pc chunk addr args := - match fmap with + match PMap.get pc fmap with + | Some rel => rhs_find (ctx:=ctx) pc (SLoad chunk addr) args rel | None => None - | Some map => - match PMap.get pc map with - | Some rel => rhs_find (ctx:=ctx) pc (SLoad chunk addr) args rel - | None => None - end end. Definition forward_move_b (rb : RB.t) (x : reg) := @@ -39,15 +29,12 @@ Definition forward_move_b (rb : RB.t) (x : reg) := | Some rel => forward_move (ctx := ctx) rel x end. -Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg := - match fmap with - | None => x - | Some inv => forward_move_b (PMap.get pc inv) x - end. +Definition subst_arg (fmap : PMap.t RB.t) (pc : node) (x : reg) : reg := + forward_move_b (PMap.get pc fmap) x. Definition subst_args fmap pc := List.map (subst_arg fmap pc). -Definition transf_instr (fmap : option (PMap.t RB.t)) +Definition transf_instr (fmap : PMap.t RB.t) (pc: node) (instr: instruction) := match instr with | Iop op args dst s => @@ -80,8 +67,8 @@ End REWRITE. Definition transf_function (f: function) : res function := do tenv <- type_function f; - let ctx := context_from_hints (preanalysis tenv f) in - let invariants := internal_analysis (ctx := ctx) tenv f in + let (invariants, hints) := preanalysis tenv f in + let ctx := context_from_hints hints in OK {| fn_sig := f.(fn_sig); fn_params := f.(fn_params); fn_stacksize := f.(fn_stacksize); diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 643b752a..69c21113 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -329,9 +329,11 @@ Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : RB.t end end. +Definition invariants := PMap.t RB.t. + Definition internal_analysis (tenv : typing_env) - (f : RTL.function) := DS.fixpoint + (f : RTL.function) : option invariants := DS.fixpoint (RTL.fn_code f) RTL.successors_instr (apply_instr' tenv (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 392fd13f..23e20ea8 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -80,15 +80,18 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = Some coq_id end in - ignore - (internal_analysis + match + internal_analysis { eq_catalog = (fun eq_id -> PTree.get eq_id !cur_catalog); eq_find_oracle = mutating_eq_find_oracle; eq_rhs_oracle = rhs_find_oracle ; eq_kill_reg = (fun reg -> PMap.get reg !cur_kill_reg); eq_kill_mem = (fun () -> !cur_kill_mem); eq_moves = (fun reg -> PMap.get reg !cur_moves) - } tenv f); - { hint_eq_catalog = !cur_catalog; - hint_eq_find_oracle= eq_find_oracle; - hint_eq_rhs_oracle = rhs_find_oracle };; + } tenv f + with None -> failwith "CSE3analysisaux analysis failed, try re-running with -fno-cse3" + | Some invariants -> + invariants, + { hint_eq_catalog = !cur_catalog; + hint_eq_find_oracle= eq_find_oracle; + hint_eq_rhs_oracle = rhs_find_oracle };; diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index c7a882b6..72b3e7e1 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -76,6 +76,8 @@ Proof. destruct f; simpl; intros. - monadInv H. monadInv EQ. + destruct preanalysis. + inv EQ1. reflexivity. - monadInv H. reflexivity. diff --git a/extraction/extraction.v b/extraction/extraction.v index 79393cf8..9b47b203 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -191,7 +191,7 @@ Set Extraction AccessOpaque. Cd "extraction". Separate Extraction - CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem CSE3.run + CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env -- cgit