From 0b76b98fcec5b13565f5403f7f7f63f46c09829c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 25 Nov 2020 12:59:29 +0100 Subject: two lemmas admitted --- backend/CSE3analysis.v | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) (limited to 'backend/CSE3analysis.v') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 5ed04bc4..8b7f1190 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -181,12 +181,24 @@ Definition eq_depends_on_mem eq := | SOp op => op_depends_on_memory op end. +Definition eq_depends_on_store eq := + match eq_op eq with + | SLoad _ _ => true + | SOp op => false + end. + Definition get_mem_kills (eqs : PTree.t equation) : PSet.t := PTree.fold (fun already (eqno : eq_id) (eq : equation) => if eq_depends_on_mem eq then PSet.add eqno already else already) eqs PSet.empty. +Definition get_store_kills (eqs : PTree.t equation) : PSet.t := + PTree.fold (fun already (eqno : eq_id) (eq : equation) => + if eq_depends_on_store eq + then PSet.add eqno already + else already) eqs PSet.empty. + Definition is_move (op : operation) : { op = Omove } + { op <> Omove }. Proof. @@ -216,6 +228,7 @@ Record eq_context := mkeqcontext eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t; eq_kill_reg : reg -> PSet.t; eq_kill_mem : unit -> PSet.t; + eq_kill_store : unit -> PSet.t; eq_moves : reg -> PSet.t }. Section OPERATIONS. @@ -342,6 +355,9 @@ Section OPERATIONS. (oper1 dst op args' rel) end. + Definition kill_store (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_store ctx tt). + Definition clever_kill_store (chunk : memory_chunk) (addr: addressing) (args : list reg) (src : reg) @@ -358,7 +374,7 @@ Section OPERATIONS. may_overlap chunk addr args chunk' addr' (eq_args eq) end end) - (PSet.inter rel (eq_kill_mem ctx tt))). + (PSet.inter rel (eq_kill_store ctx tt))). Definition store2 (chunk : memory_chunk) (addr: addressing) (args : list reg) @@ -366,7 +382,7 @@ Section OPERATIONS. (rel : RELATION.t) : RELATION.t := if Compopts.optim_CSE3_alias_analysis tt then clever_kill_store chunk addr args src rel - else kill_mem rel. + else kill_store rel. Definition store1 (chunk : memory_chunk) (addr: addressing) (args : list reg) @@ -501,6 +517,7 @@ Definition context_from_hints (hints : analysis_hints) := let eqs := hint_eq_catalog hints in let reg_kills := get_reg_kills eqs in let mem_kills := get_mem_kills eqs in + let store_kills := get_store_kills eqs in let moves := get_moves eqs in {| eq_catalog := fun eq_id => PTree.get eq_id eqs; @@ -508,5 +525,6 @@ Definition context_from_hints (hints : analysis_hints) := eq_rhs_oracle := hint_eq_rhs_oracle hints; eq_kill_reg := fun reg => PMap.get reg reg_kills; eq_kill_mem := fun _ => mem_kills; + eq_kill_store := fun _ => store_kills; eq_moves := fun reg => PMap.get reg moves |}. -- cgit