From 7698300cfe2d3f944ce2e1d4a60a263620487718 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 20 Dec 2013 13:05:53 +0000
Subject: Merge of branch value-analysis.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Constprop.v | 447 +++++++++++++---------------------------------------
 1 file changed, 111 insertions(+), 336 deletions(-)

(limited to 'backend/Constprop.v')

diff --git a/backend/Constprop.v b/backend/Constprop.v
index e5ea64d8..76d8e6ca 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -25,242 +25,30 @@ Require Import RTL.
 Require Import Lattice.
 Require Import Kildall.
 Require Import Liveness.
+Require Import ValueDomain.
+Require Import ValueAOp.
+Require Import ValueAnalysis.
 Require Import ConstpropOp.
 
-(** * Static analysis *)
-
-(** The type [approx] of compile-time approximations of values is
-  defined in the machine-dependent part [ConstpropOp]. *)
-
-(** We equip this type of approximations with a semi-lattice structure.
-  The ordering is inclusion between the sets of values denoted by
-  the approximations. *)
-
-Module Approx <: SEMILATTICE_WITH_TOP.
-  Definition t := approx.
-  Definition eq (x y: t) := (x = y).
-  Definition eq_refl: forall x, eq x x := (@refl_equal t).
-  Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
-  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).
-  Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}.
-  Proof.
-    decide equality.
-    apply Int.eq_dec.
-    apply Float.eq_dec.
-    apply Int64.eq_dec.
-    apply Int.eq_dec.
-    apply ident_eq.
-    apply Int.eq_dec.
-  Defined.
-  Definition beq (x y: t) := if eq_dec x y then true else false.
-  Lemma beq_correct: forall x y, beq x y = true -> x = y.
-  Proof.
-    unfold beq; intros.  destruct (eq_dec x y). auto. congruence.
-  Qed.
-
-  Definition ge (x y: t) : Prop := x = Unknown \/ y = Novalue \/ x = y.
-
-  Lemma ge_refl: forall x y, eq x y -> ge x y.
-  Proof.
-    unfold eq, ge; tauto.
-  Qed.
-  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
-  Proof.
-    unfold ge; intuition congruence.
-  Qed.
-  Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
-  Proof.
-    unfold eq, ge; intros; congruence.
-  Qed.
-  Definition bot := Novalue.
-  Definition top := Unknown.
-  Lemma ge_bot: forall x, ge x bot.
-  Proof.
-    unfold ge, bot; tauto.
-  Qed.
-  Lemma ge_top: forall x, ge top x.
-  Proof.
-    unfold ge, bot; tauto.
-  Qed.
-  Definition lub (x y: t) : t :=
-    if eq_dec x y then x else
-    match x, y with
-    | Novalue, _ => y
-    | _, Novalue => x
-    | _, _ => Unknown
-    end.
-  Lemma ge_lub_left: forall x y, ge (lub x y) x.
-  Proof.
-    unfold lub; intros.
-    case (eq_dec x y); intro.
-    apply ge_refl. apply eq_refl.
-    destruct x; destruct y; unfold ge; tauto.
-  Qed.
-  Lemma ge_lub_right: forall x y, ge (lub x y) y.
-  Proof.
-    unfold lub; intros.
-    case (eq_dec x y); intro.
-    apply ge_refl. subst. apply eq_refl.
-    destruct x; destruct y; unfold ge; tauto.
-  Qed.
-End Approx.
-
-Module D := LPMap Approx.
-
-(** We keep track of read-only global variables (i.e. "const" global
-  variables in C) as a map from their names to their initialization
-  data. *)
-
-Definition global_approx : Type := PTree.t (list init_data).
-
-(** Given some initialization data and a byte offset, compute a static
-  approximation of the result of a memory load from a memory block
-  initialized with this data. *)
-
-Fixpoint eval_load_init (chunk: memory_chunk) (pos: Z) (il: list init_data): approx :=
-  match il with
-  | nil => Unknown
-  | Init_int8 n :: il' =>
-      if zeq pos 0 then
-        match chunk with
-        | Mint8unsigned => I (Int.zero_ext 8 n)
-        | Mint8signed => I (Int.sign_ext 8 n)
-        | _ => Unknown
-        end
-      else eval_load_init chunk (pos - 1) il'
-  | Init_int16 n :: il' =>
-      if zeq pos 0 then
-        match chunk with
-        | Mint16unsigned => I (Int.zero_ext 16 n)
-        | Mint16signed => I (Int.sign_ext 16 n)
-        | _ => Unknown
-        end
-      else eval_load_init chunk (pos - 2) il'
-  | Init_int32 n :: il' =>
-      if zeq pos 0 
-      then match chunk with Mint32 => I n | _ => Unknown end
-      else eval_load_init chunk (pos - 4) il'
-  | Init_int64 n :: il' =>
-      if zeq pos 0 
-      then match chunk with Mint64 => L n | _ => Unknown end
-      else eval_load_init chunk (pos - 8) il'
-  | Init_float32 n :: il' =>
-      if zeq pos 0
-      then match chunk with 
-           | Mfloat32 => if propagate_float_constants tt then F (Float.singleoffloat n) else Unknown
-           | _ => Unknown
-           end
-      else eval_load_init chunk (pos - 4) il'
-  | Init_float64 n :: il' =>
-      if zeq pos 0 
-      then match chunk with
-           | Mfloat64 => if propagate_float_constants tt then F n else Unknown
-           | _ => Unknown
-           end
-      else eval_load_init chunk (pos - 8) il'
-  | Init_addrof symb ofs :: il' =>
-      if zeq pos 0
-      then match chunk with Mint32 => G symb ofs | _ => Unknown end
-      else eval_load_init chunk (pos - 4) il'
-  | Init_space n :: il' =>
-      eval_load_init chunk (pos - Zmax n 0) il'
-  end.
-
-(** Compute a static approximation for the result of a load at an address whose
-  approximation is known.  If the approximation points to a global variable,
-  and this global variable is read-only, we use its initialization data
-  to determine a static approximation.  Otherwise, [Unknown] is returned. *)
-
-Definition eval_static_load (gapp: global_approx) (chunk: memory_chunk) (addr: approx) : approx :=
-  match addr with
-  | G symb ofs =>
-      match gapp!symb with
-      | None => Unknown
-      | Some il => eval_load_init chunk (Int.unsigned ofs) il
-      end
-  | _ => Unknown
-  end.
-
-(** The transfer function for the dataflow analysis is straightforward.
-  For [Iop] instructions, we set the approximation of the destination
-  register to the result of executing abstractly the operation.
-  For [Iload] instructions, we set the approximation of the destination
-  register to the result of [eval_static_load].
-  For [Icall] and [Ibuiltin], the destination register becomes [Unknown].
-  Other instructions keep the approximations unchanged, as they preserve
-  the values of all registers. *)
-
-Definition approx_reg (app: D.t) (r: reg) := 
-  D.get r app.
-
-Definition approx_regs (app: D.t) (rl: list reg):=
-  List.map (approx_reg app) rl.
-
-Definition transfer (gapp: global_approx) (f: function) (pc: node) (before: D.t) :=
-  match f.(fn_code)!pc with
-  | None => before
-  | Some i =>
-      match i with
-      | Iop op args res s =>
-          let a := eval_static_operation op (approx_regs before args) in
-          D.set res a before
-      | Iload chunk addr args dst s =>
-          let a := eval_static_load gapp chunk
-                     (eval_static_addressing addr (approx_regs before args)) in
-          D.set dst a before
-      | Icall sig ros args res s =>
-          D.set res Unknown before
-      | Ibuiltin ef args res s =>
-          D.set res Unknown before
-      | _ =>
-          before
-      end
-  end.
-
-(** To reduce the size of approximations, we preventively set to [Top]
-  the approximations of registers used for the last time in the
-  current instruction. *)
-
-Definition transfer' (gapp: global_approx) (f: function) (lastuses: PTree.t (list reg))
-                     (pc: node) (before: D.t) :=
-  let after := transfer gapp f pc before in
-  match lastuses!pc with
-  | None => after
-  | Some regs => List.fold_left (fun a r => D.set r Unknown a) regs after
-  end.
-
-(** The static analysis itself is then an instantiation of Kildall's
-  generic solver for forward dataflow inequations. [analyze f]
-  returns a mapping from program points to mappings of pseudo-registers
-  to approximations.  It can fail to reach a fixpoint in a reasonable
-  number of iterations, in which case we use the trivial mapping
-  (program point -> [D.top]) instead. *)
-
-Module DS := Dataflow_Solver(D)(NodeSetForward).
-
-Definition analyze (gapp: global_approx) (f: RTL.function): PMap.t D.t :=
-  let lu := Liveness.last_uses f in
-  match DS.fixpoint f.(fn_code) successors_instr (transfer' gapp f lu) 
-                    ((f.(fn_entrypoint), D.top) :: nil) with
-  | None => PMap.init D.top
-  | Some res => res
-  end.
-
-(** * Code transformation *)
-
-(** The code transformation proceeds instruction by instruction.
-    Operators whose arguments are all statically known are turned
-    into ``load integer constant'', ``load float constant'' or
-    ``load symbol address'' operations.  Likewise for loads whose
-    result can be statically predicted.  Operators for which some
-    but not all arguments are known are subject to strength reduction,
-    and similarly for the addressing modes of load and store instructions.
-    Conditional branches and multi-way branches are statically resolved
-    into [Inop] instructions if possible. Other instructions are unchanged.
-
-    In addition, we try to jump over conditionals whose condition can
-    be statically resolved based on the abstract state "after" the
-    instruction that branches to the conditional.  A typical example is:
+(** The code transformation builds on the results of the static analysis
+  of values from module [ValueAnalysis].  It proceeds instruction by
+  instruction.
+- Operators whose arguments are all statically known are turned into
+  ``load integer constant'', ``load float constant'' or ``load
+  symbol address'' operations.  Likewise for loads whose result can
+  be statically predicted.
+- Operators for which some but not all arguments are known are subject
+  to strength reduction (replacement by cheaper operators) and
+  similarly for the addressing modes of load and store instructions.
+- Cast operators that have no effect (because their arguments are
+  already normalized to the destination type) are removed.
+- Conditional branches and multi-way branches are statically resolved
+  into [Inop] instructions when possible.
+- Other instructions are unchanged.
+
+  In addition, we try to jump over conditionals whose condition can
+  be statically resolved based on the abstract state "after" the
+  instruction that branches to the conditional.  A typical example is:
 <<
           1: x := 0 and goto 2
           2: if (x == 0) goto 3 else goto 4
@@ -273,37 +61,35 @@ Definition analyze (gapp: global_approx) (f: RTL.function): PMap.t D.t :=
 >>
 *)
 
-Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident :=
+Definition transf_ros (ae: AE.t) (ros: reg + ident) : reg + ident :=
   match ros with
   | inl r =>
-      match D.get r app with
-      | G symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros
+      match areg ae r with
+      | Ptr(Gl symb ofs) => if Int.eq ofs Int.zero then inr _ symb else ros
       | _ => ros
       end
   | inr s => ros
   end.
 
-Parameter generate_float_constants : unit -> bool.
-
-Definition const_for_result (a: approx) : option operation :=
+Definition const_for_result (a: aval) : option operation :=
   match a with
   | I n => Some(Ointconst n)
   | F n => if generate_float_constants tt then Some(Ofloatconst n) else None
-  | G symb ofs => Some(Oaddrsymbol symb ofs)
-  | S ofs => Some(Oaddrstack ofs)
+  | Ptr(Gl symb ofs) => Some(Oaddrsymbol symb ofs)
+  | Ptr(Stk ofs) => Some(Oaddrstack ofs)
   | _ => None
   end.
 
-Fixpoint successor_rec (n: nat) (f: function) (app: D.t) (pc: node) : node :=
+Fixpoint successor_rec (n: nat) (f: function) (ae: AE.t) (pc: node) : node :=
   match n with
   | O => pc
-  | Datatypes.S n' =>
+  | S n' =>
       match f.(fn_code)!pc with
       | Some (Inop s) =>
-          successor_rec n' f app s
+          successor_rec n' f ae s
       | Some (Icond cond args s1 s2) =>
-          match eval_static_condition cond (approx_regs app args) with
-          | Some b => if b then s1 else s2
+          match resolve_branch (eval_static_condition cond (aregs ae args)) with
+          | Some b => successor_rec n' f ae (if b then s1 else s2)
           | None => pc
           end
       | _ => pc
@@ -312,15 +98,15 @@ Fixpoint successor_rec (n: nat) (f: function) (app: D.t) (pc: node) : node :=
 
 Definition num_iter := 10%nat.
 
-Definition successor (f: function) (app: D.t) (pc: node) : node :=
-  successor_rec num_iter f app pc.
+Definition successor (f: function) (ae: AE.t) (pc: node) : node :=
+  successor_rec num_iter f ae pc.
 
-Function annot_strength_reduction
-     (app: D.t) (targs: list annot_arg) (args: list reg) :=
+Fixpoint annot_strength_reduction
+     (ae: AE.t) (targs: list annot_arg) (args: list reg) :=
   match targs, args with
   | AA_arg ty :: targs', arg :: args' =>
-      let (targs'', args'') := annot_strength_reduction app targs' args' in
-      match ty, approx_reg app arg with
+      let (targs'', args'') := annot_strength_reduction ae targs' args' in
+      match ty, areg ae arg with
       | Tint, I n => (AA_int n :: targs'', args'')
       | Tfloat, F n => if generate_float_constants tt
                        then (AA_float n :: targs'', args'')
@@ -328,117 +114,106 @@ Function annot_strength_reduction
       | _, _ => (AA_arg ty :: targs'', arg :: args'')
       end
   | targ :: targs', _ =>
-      let (targs'', args'') := annot_strength_reduction app targs' args in
+      let (targs'', args'') := annot_strength_reduction ae targs' args in
       (targ :: targs'', args'')
   | _, _ =>
       (targs, args)
   end.
 
 Function builtin_strength_reduction
-      (app: D.t) (ef: external_function) (args: list reg) :=
+      (ae: AE.t) (ef: external_function) (args: list reg) :=
   match ef, args with
   | EF_vload chunk, r1 :: nil =>
-      match approx_reg app r1 with
-      | G symb n1 => (EF_vload_global chunk symb n1, nil)
+      match areg ae r1 with
+      | Ptr(Gl symb n1) => (EF_vload_global chunk symb n1, nil)
       | _ => (ef, args)
       end
   | EF_vstore chunk, r1 :: r2 :: nil =>
-      match approx_reg app r1 with
-      | G symb n1 => (EF_vstore_global chunk symb n1, r2 :: nil)
+      match areg ae r1 with
+      | Ptr(Gl symb n1) => (EF_vstore_global chunk symb n1, r2 :: nil)
       | _ => (ef, args)
       end
   | EF_annot text targs, args =>
-      let (targs', args') := annot_strength_reduction app targs args in
+      let (targs', args') := annot_strength_reduction ae targs args in
       (EF_annot text targs', args')
   | _, _ =>
       (ef, args)
   end.
 
-Definition transf_instr (gapp: global_approx) (f: function) (apps: PMap.t D.t)
-                       (pc: node) (instr: instruction) :=
-  let app := apps!!pc in
-  match instr with
-  | Iop op args res s =>
-      let a := eval_static_operation op (approx_regs app args) in
-      let s' := successor f (D.set res a app) s in
-      match const_for_result a with
-      | Some cop =>
-          Iop cop nil res s'
-      | None =>
-          let (op', args') := op_strength_reduction op args (approx_regs app args) in
-          Iop op' args' res s'
-      end
-  | Iload chunk addr args dst s =>
-      let a := eval_static_load gapp chunk
-                  (eval_static_addressing addr (approx_regs app args)) in
-      match const_for_result a with
-      | Some cop =>
-          Iop cop nil dst s
-      | None =>
-          let (addr', args') := addr_strength_reduction addr args (approx_regs app args) in
-          Iload chunk addr' args' dst s      
-      end
-  | Istore chunk addr args src s =>
-      let (addr', args') := addr_strength_reduction addr args (approx_regs app args) in
-      Istore chunk addr' args' src s      
-  | Icall sig ros args res s =>
-      Icall sig (transf_ros app ros) args res s
-  | Itailcall sig ros args =>
-      Itailcall sig (transf_ros app ros) args
-  | Ibuiltin ef args res s =>
-      let (ef', args') := builtin_strength_reduction app ef args in
-      Ibuiltin ef' args' res s
-  | Icond cond args s1 s2 =>
-      match eval_static_condition cond (approx_regs app args) with
-      | Some b =>
-          if b then Inop s1 else Inop s2
-      | None =>
-          let (cond', args') := cond_strength_reduction cond args (approx_regs app args) in
-          Icond cond' args' s1 s2
-      end
-  | Ijumptable arg tbl =>
-      match approx_reg app arg with
-      | I n =>
-          match list_nth_z tbl (Int.unsigned n) with
-          | Some s => Inop s
-          | None => instr
+Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem)
+                        (pc: node) (instr: instruction) :=
+  match an!!pc with
+  | VA.Bot =>
+      instr
+  | VA.State ae am =>
+      match instr with
+      | Iop op args res s =>
+          let aargs := aregs ae args in
+          let a := eval_static_operation op aargs in
+          let s' := successor f (AE.set res a ae) s in
+          match const_for_result a with
+          | Some cop =>
+              Iop cop nil res s'
+          | None =>
+              let (op', args') := op_strength_reduction op args aargs in
+              Iop op' args' res s'
+          end
+      | Iload chunk addr args dst s =>
+          let aargs := aregs ae args in
+          let a := ValueDomain.loadv chunk rm am (eval_static_addressing addr aargs) in
+          match const_for_result a with
+          | Some cop =>
+              Iop cop nil dst s
+          | None =>
+              let (addr', args') := addr_strength_reduction addr args aargs in
+              Iload chunk addr' args' dst s      
+          end
+      | Istore chunk addr args src s =>
+          let aargs := aregs ae args in
+          let (addr', args') := addr_strength_reduction addr args aargs in
+          Istore chunk addr' args' src s      
+      | Icall sig ros args res s =>
+          Icall sig (transf_ros ae ros) args res s
+      | Itailcall sig ros args =>
+          Itailcall sig (transf_ros ae ros) args
+      | Ibuiltin ef args res s =>
+          let (ef', args') := builtin_strength_reduction ae ef args in
+          Ibuiltin ef' args' res s
+      | Icond cond args s1 s2 =>
+          let aargs := aregs ae args in
+          match resolve_branch (eval_static_condition cond aargs) with
+          | Some b =>
+              if b then Inop s1 else Inop s2
+          | None =>
+              let (cond', args') := cond_strength_reduction cond args aargs in
+              Icond cond' args' s1 s2
           end
-      | _ => instr
+      | Ijumptable arg tbl =>
+          match areg ae arg with
+          | I n =>
+              match list_nth_z tbl (Int.unsigned n) with
+              | Some s => Inop s
+              | None => instr
+              end
+          | _ => instr
+          end
+      | _ =>
+          instr
       end
-  | _ =>
-      instr
   end.
 
-Definition transf_code (gapp: global_approx) (f: function) (app: PMap.t D.t) (instrs: code) : code :=
-  PTree.map (transf_instr gapp f app) instrs.
-
-Definition transf_function (gapp: global_approx) (f: function) : function :=
-  let approxs := analyze gapp f in
+Definition transf_function (rm: romem) (f: function) : function :=
+  let an := ValueAnalysis.analyze rm f in
   mkfunction
     f.(fn_sig)
     f.(fn_params)
     f.(fn_stacksize)
-    (transf_code gapp f approxs f.(fn_code))
+    (PTree.map (transf_instr f an rm) f.(fn_code))
     f.(fn_entrypoint).
 
-Definition transf_fundef (gapp: global_approx) (fd: fundef) : fundef :=
-  AST.transf_fundef (transf_function gapp) fd.
-
-Fixpoint make_global_approx (gapp: global_approx) (gdl: list (ident * globdef fundef unit)): global_approx :=
-  match gdl with
-  | nil => gapp
-  | (id, gl) :: gdl' =>
-      let gapp1 :=
-        match gl with
-        | Gfun f => PTree.remove id gapp
-        | Gvar gv =>
-            if gv.(gvar_readonly) && negb gv.(gvar_volatile)
-            then PTree.set id gv.(gvar_init) gapp
-            else PTree.remove id gapp
-        end in
-      make_global_approx gapp1 gdl'
-  end.
+Definition transf_fundef (rm: romem) (fd: fundef) : fundef :=
+  AST.transf_fundef (transf_function rm) fd.
 
 Definition transf_program (p: program) : program :=
-  let gapp := make_global_approx (PTree.empty _) p.(prog_defs) in
-  transform_program (transf_fundef gapp) p.
+  let rm := romem_for_program p in
+  transform_program (transf_fundef rm) p.
-- 
cgit