From e16b34d9fc1aa7854759787fd52ad59c964c2d4b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 3 Jul 2019 11:06:07 +0200 Subject: Perform constant propagation for known built-in functions When an external function is a known built-in function and it is applied to compile-time integer or FP constants, we can use the known semantics of the builtin to compute the result at compile-time. --- backend/Constprop.v | 44 ++++++++++++++++++++++++++++++++++++++-- backend/Constpropproof.v | 44 ++++++++++++++++++++++++++++++---------- backend/ValueAnalysis.v | 52 +++++++++++++++++++++++++++++++++++++++++++++++- backend/ValueDomain.v | 44 ++++++++++++++++++++++++++++++++++++++-- 4 files changed, 168 insertions(+), 16 deletions(-) diff --git a/backend/Constprop.v b/backend/Constprop.v index d8211ffe..4aab7677 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -15,7 +15,7 @@ and the corresponding code rewriting. *) Require Import Coqlib Maps Integers Floats Lattice Kildall. -Require Import AST Linking. +Require Import AST Linking Builtins. Require Compopts Machregs. Require Import Op Registers RTL. Require Import Liveness ValueDomain ValueAOp ValueAnalysis. @@ -139,6 +139,30 @@ Definition builtin_strength_reduction | _ => builtin_args_strength_reduction ae al (Machregs.builtin_constraints ef) end. +(* +Definition transf_builtin + (ae: AE.t) (am: amem) (rm: romem) + (ef: external_function) + (args: list (builtin_arg reg)) (res: builtin_res reg) (s: node) := + let dfl := Ibuiltin ef (builtin_strength_reduction ae ef args) res s in + match ef, res with + | EF_builtin name sg, BR rd => + match lookup_builtin_function name sg with + | Some bf => + match eval_static_builtin_function ae am rm bf args with + | Some a => + match const_for_result a with + | Some cop => Iop cop nil rd s + | None => dfl + end + | None => dfl + end + | None => dfl + end + | _, _ => dfl + end. +*) + Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) (pc: node) (instr: instruction) := match an!!pc with @@ -176,7 +200,23 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) | Itailcall sig ros args => Itailcall sig (transf_ros ae ros) args | Ibuiltin ef args res s => - Ibuiltin ef (builtin_strength_reduction ae ef args) res s + let dfl := Ibuiltin ef (builtin_strength_reduction ae ef args) res s in + match ef, res with + | EF_builtin name sg, BR rd => + match lookup_builtin_function name sg with + | Some bf => + match eval_static_builtin_function ae am rm bf args with + | Some a => + match const_for_result a with + | Some cop => Iop cop nil rd s + | None => dfl + end + | None => dfl + end + | None => dfl + end + | _, _ => dfl + end | Icond cond args s1 s2 => let aargs := aregs ae args in match resolve_branch (eval_static_condition cond aargs) with diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index e28519ca..a5d08a0f 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -14,7 +14,7 @@ Require Import Coqlib Maps Integers Floats Lattice Kildall. Require Import AST Linking. -Require Import Values Events Memory Globalenvs Smallstep. +Require Import Values Builtins Events Memory Globalenvs Smallstep. Require Compopts Machregs. Require Import Op Registers RTL. Require Import Liveness ValueDomain ValueAOp ValueAnalysis. @@ -474,19 +474,41 @@ Proof. - (* Ibuiltin *) rename pc'0 into pc. TransfInstr; intros. Opaque builtin_strength_reduction. - exploit builtin_strength_reduction_correct; eauto. intros (vargs' & P & Q). - exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)). + set (dfl := Ibuiltin ef (builtin_strength_reduction ae ef args) res pc') in *. + set (rm := romem_for cu) in *. + assert (DFL: (fn_code (transf_function rm f))!pc = Some dfl -> + exists (n2 : nat) (s2' : state), + step tge + (State s' (transf_function rm f) (Vptr sp0 Ptrofs.zero) pc rs' m'0) t s2' /\ + match_states n2 + (State s f (Vptr sp0 Ptrofs.zero) pc' (regmap_setres res vres rs) m') s2'). + { + exploit builtin_strength_reduction_correct; eauto. intros (vargs' & P & Q). + exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)). apply REGS. eauto. eexact P. - intros (vargs'' & U & V). - exploit external_call_mem_extends; eauto. - intros [v' [m2' [A [B [C D]]]]]. + intros (vargs'' & U & V). + exploit external_call_mem_extends; eauto. + intros (v' & m2' & A & B & C & D). + econstructor; econstructor; split. + eapply exec_Ibuiltin; eauto. + eapply eval_builtin_args_preserved. eexact symbols_preserved. eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + eapply match_states_succ; eauto. + apply set_res_lessdef; auto. + } + destruct ef; auto. + destruct res; auto. + destruct (lookup_builtin_function name sg) as [bf|] eqn:LK; auto. + destruct (eval_static_builtin_function ae am rm bf args) as [a|] eqn:ES; auto. + destruct (const_for_result a) as [cop|] eqn:CR; auto. + clear DFL. simpl in H1; red in H1; rewrite LK in H1; inv H1. + exploit const_for_result_correct; eauto. + eapply eval_static_builtin_function_sound; eauto. + intros (v' & A & B). left; econstructor; econstructor; split. - eapply exec_Ibuiltin; eauto. - eapply eval_builtin_args_preserved. eexact symbols_preserved. eauto. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. + eapply exec_Iop; eauto. eapply match_states_succ; eauto. - apply set_res_lessdef; auto. - + apply set_reg_lessdef; auto. - (* Icond, preserved *) rename pc'0 into pc. TransfInstr. set (ac := eval_static_condition cond (aregs ae args)). diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 1f80c293..8dbb67a7 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -13,7 +13,7 @@ Require Import FunInd. Require Import Coqlib Maps Integers Floats Lattice Kildall. Require Import Compopts AST Linking. -Require Import Values Memory Globalenvs Events. +Require Import Values Memory Globalenvs Builtins Events. Require Import Registers Op RTL. Require Import ValueDomain ValueAOp Liveness. @@ -78,6 +78,15 @@ Definition transfer_builtin_default let (av, am') := analyze_call am (map (abuiltin_arg ae am rm) args) in VA.State (set_builtin_res res av ae) am'. +Definition eval_static_builtin_function + (ae: aenv) (am: amem) (rm: romem) + (bf: builtin_function) (args: list (builtin_arg reg)) := + match builtin_function_sem bf + (map val_of_aval (map (abuiltin_arg ae am rm) args)) with + | Some v => aval_of_val v + | None => None + end. + Definition transfer_builtin (ae: aenv) (am: amem) (rm: romem) (ef: external_function) (args: list (builtin_arg reg)) (res: builtin_res reg) := @@ -105,6 +114,15 @@ Definition transfer_builtin | EF_annot_val _ _ _, v :: nil => let av := abuiltin_arg ae am rm v in VA.State (set_builtin_res res av ae) am + | EF_builtin name sg, _ => + match lookup_builtin_function name sg with + | Some bf => + match eval_static_builtin_function ae am rm bf args with + | Some av => VA.State (set_builtin_res res av ae) am + | None => transfer_builtin_default ae am rm args res + end + | None => transfer_builtin_default ae am rm args res + end | _, _ => transfer_builtin_default ae am rm args res end. @@ -372,6 +390,31 @@ Proof. intros. destruct res; simpl; auto. apply ematch_update; auto. Qed. +Lemma eval_static_builtin_function_sound: + forall bc ge rs sp m ae rm am (bf: builtin_function) al vl v va, + ematch bc rs ae -> + romatch bc m rm -> + mmatch bc m am -> + genv_match bc ge -> + bc sp = BCstack -> + eval_builtin_args ge (fun r => rs#r) (Vptr sp Ptrofs.zero) m al vl -> + eval_static_builtin_function ae am rm bf al = Some va -> + builtin_function_sem bf vl = Some v -> + vmatch bc v va. +Proof. + unfold eval_static_builtin_function; intros. + exploit abuiltin_args_sound; eauto. + set (vla := map (abuiltin_arg ae am rm) al) in *. intros VMA. + destruct (builtin_function_sem bf (map val_of_aval vla)) as [v0|] eqn:A; try discriminate. + assert (LD: Val.lessdef v0 v). + { apply val_inject_lessdef. + exploit (bs_inject _ (builtin_function_sem bf)). + apply val_inject_list_lessdef. eapply list_val_of_aval_sound; eauto. + rewrite A, H6; simpl. auto. + } + inv LD. apply aval_of_val_sound; auto. discriminate. +Qed. + (** ** Constructing block classifications *) Definition bc_nostack (bc: block_classification) : Prop := @@ -1343,6 +1386,13 @@ Proof. } unfold transfer_builtin in TR. destruct ef; auto. ++ (* builtin function *) + destruct (lookup_builtin_function name sg) as [bf|] eqn:LK; auto. + destruct (eval_static_builtin_function ae am rm bf args) as [av|] eqn:ES; auto. + simpl in H1. red in H1. rewrite LK in H1. inv H1. + eapply sound_succ_state; eauto. simpl; auto. + apply set_builtin_res_sound; auto. + eapply eval_static_builtin_function_sound; eauto. + (* volatile load *) inv H0; auto. inv H3; auto. inv H1. exploit abuiltin_arg_sound; eauto. intros VM1. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index f6afa836..fd3bd5ae 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -13,7 +13,7 @@ Require Import FunInd. Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice. Require Import Compopts AST. -Require Import Values Memory Globalenvs Events. +Require Import Values Memory Globalenvs Builtins Events. Require Import Registers RTL. (** The abstract domains for value analysis *) @@ -3038,7 +3038,47 @@ Proof with (auto using provenance_monotone with va). - destruct (zlt n 16)... Qed. -(** Abstracting memory blocks *) +(** Analysis of known builtin functions. All we have is a dynamic semantics + as a function [list val -> option val], but we can still perform + some constant propagation. *) + +Definition val_of_aval (a: aval) : val := + match a with + | I n => Vint n + | L n => Vlong n + | F f => Vfloat f + | FS f => Vsingle f + | _ => Vundef + end. + +Definition aval_of_val (v: val) : option aval := + match v with + | Vint n => Some (I n) + | Vlong n => Some (L n) + | Vfloat f => Some (F f) + | Vsingle f => Some (FS f) + | _ => None + end. + +Lemma val_of_aval_sound: + forall v a, vmatch v a -> Val.lessdef (val_of_aval a) v. +Proof. + destruct 1; simpl; auto. +Qed. + +Corollary list_val_of_aval_sound: + forall vl al, list_forall2 vmatch vl al -> Val.lessdef_list (map val_of_aval al) vl. +Proof. + induction 1; simpl; constructor; auto using val_of_aval_sound. +Qed. + +Lemma aval_of_val_sound: + forall v a, aval_of_val v = Some a -> vmatch v a. +Proof. + intros v a E; destruct v; simpl in E; inv E; constructor. +Qed. + +(** * Abstracting memory blocks *) Inductive acontent : Type := | ACval (chunk: memory_chunk) (av: aval). -- cgit