diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/ConstpropOp.vp | 11 | ||||
-rw-r--r-- | powerpc/ConstpropOpproof.v | 18 | ||||
-rw-r--r-- | powerpc/PrintAsm.ml | 6 |
3 files changed, 3 insertions, 32 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 973be925..9131a466 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -293,15 +293,4 @@ Nondetfunction addr_strength_reduction (addr, args) end. -Nondetfunction builtin_strength_reduction - (ef: external_function) (args: list reg) (vl: list approx) := - match ef, args, vl with - | EF_vload chunk, r1 :: nil, G symb n1 :: nil => - (EF_vload_global chunk symb n1, nil) - | EF_vstore chunk, r1 :: r2 :: nil, G symb n1 :: v2 :: nil => - (EF_vstore_global chunk symb n1, r2 :: nil) - | _, _, _ => - (ef, args) - end. - End STRENGTH_REDUCTION. diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 7d557c6d..84e1e5bb 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -430,24 +430,6 @@ Proof. auto. Qed. -Lemma builtin_strength_reduction_correct: - forall ef args vl m t vres m', - vl = approx_regs app args -> - external_call ef ge rs##args m t vres m' -> - let (ef', args') := builtin_strength_reduction ef args vl in - external_call ef' ge rs##args' m t vres m'. -Proof. - intros until m'. unfold builtin_strength_reduction. - destruct (builtin_strength_reduction_match ef args vl); simpl; intros; InvApproxRegs; SimplVMA. - unfold symbol_address in H. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H in H0. - rewrite volatile_load_global_charact. exists b; auto. - inv H0. - unfold symbol_address in H1. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H1 in H0. - rewrite volatile_store_global_charact. exists b; auto. - inv H0. - auto. -Qed. - End STRENGTH_REDUCTION. End ANALYSIS. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 9c0f471d..c9203ec6 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -231,9 +231,9 @@ let rolm_mask n = (* Handling of annotations *) -let print_annot_stmt oc txt args = +let print_annot_stmt oc txt targs args = fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "R1" oc txt args + PrintAnnot.print_annot_stmt preg "R1" oc txt targs args let print_annot_val oc txt args res = fprintf oc "%s annotation: " comment; @@ -737,7 +737,7 @@ let print_instruction oc tbl pc fallthrough = function | Pannot(ef, args) -> begin match ef with | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) args + print_annot_stmt oc (extern_atom txt) targs args | _ -> assert false end |