Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Values Memory Builtins Events Globalenvs Smallstep.
Require Import Op Registers RTL.
Require Import ValueDomain ValueAOp ValueAnalysis.
Require Import CSEdomain CombineOp CombineOpproof CSE.

Definition match_prog (prog tprog: RTL.program) :=
  match_program (fun cu f tf => transf_fundef (romem_for cu) f = OK tf) eq prog tprog.

Lemma transf_program_match:
  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.

Soundness of operations over value numberings

Remark wf_equation_incr:
  forall next1 next2 e,
  wf_equation next1 e -> Ple next1 next2 -> wf_equation next2 e.


Definition valu_agree (valu1 valu2: valuation) (upto: valnum) :=
  forall v, Plt v upto -> valu2 v = valu1 v.

Section EXTEN.

Variable valu1: valuation.
Variable upto: valnum.
Variable valu2: valuation.
Hypothesis AGREE: valu_agree valu1 valu2 upto.
Variable bc: block_classification.
Variable ge: genv.
Variable sp: val.
Variable rs: regset.
Variable m: mem.

Lemma valnums_val_exten:
  forall vl,
  (forall v, In v vl -> Plt v upto) ->
  map valu2 vl = map valu1 vl.

Lemma rhs_eval_to_exten:
  forall r v,
  rhs_eval_to valu1 ge sp m r v ->
  (forall v, In v (valnums_rhs r) -> Plt v upto) ->
  rhs_eval_to valu2 ge sp m r v.

Lemma rhs_valid_exten:
  forall r,
  rhs_valid bc valu1 ge sp r ->
  (forall v, In v (valnums_rhs r) -> Plt v upto) ->
  rhs_valid bc valu2 ge sp r.

Lemma equation_holds_exten:
  forall e,
  equation_holds bc valu1 ge sp m e ->
  wf_equation upto e ->
  equation_holds bc valu2 ge sp m e.

Lemma numbering_holds_exten:
  forall n,
  numbering_holds bc valu1 ge sp rs m n ->
  Ple n.(num_next) upto ->
  numbering_holds bc valu2 ge sp rs m n.

End EXTEN.

Ltac splitall := repeat (match goal with |- _ /\ _ => split end).

Lemma valnum_reg_holds:
  forall bc valu1 ge sp rs m n r n' v,
  numbering_holds bc valu1 ge sp rs m n ->
  valnum_reg n r = (n', v) ->
  exists valu2,
     numbering_holds bc valu2 ge sp rs m n'
  /\ rs#r = valu2 v
  /\ valu_agree valu1 valu2 n.(num_next)
  /\ Plt v n'.(num_next)
  /\ Ple n.(num_next) n'.(num_next).

Lemma valnum_regs_holds:
  forall rl bc valu1 ge sp rs m n n' vl,
  numbering_holds bc valu1 ge sp rs m n ->
  valnum_regs n rl = (n', vl) ->
  exists valu2,
     numbering_holds bc valu2 ge sp rs m n'
  /\ rs##rl = map valu2 vl
  /\ valu_agree valu1 valu2 n.(num_next)
  /\ (forall v, In v vl -> Plt v n'.(num_next))
  /\ Ple n.(num_next) n'.(num_next).

Lemma find_valnum_rhs_charact:
  forall rh v eqs,
    find_valnum_rhs rh eqs = Some v ->
    exists rh', In (Eq v true rh') eqs /\ rhs_compat rh rh'.

Lemma find_valnum_rhs'_charact:
  forall rh v eqs,
   find_valnum_rhs' rh eqs = Some v ->
    exists strict rh', In (Eq v strict rh') eqs /\ rhs_compat rh rh'.

Lemma find_valnum_num_charact:
  forall v r eqs, find_valnum_num v eqs = Some r -> In (Eq v true r) eqs.

Lemma reg_valnum_sound:
  forall n v r bc valu ge sp rs m,
  reg_valnum n v = Some r ->
  numbering_holds bc valu ge sp rs m n ->
  rs#r = valu v.

Lemma regs_valnums_sound:
  forall n bc valu ge sp rs m,
  numbering_holds bc valu ge sp rs m n ->
  forall vl rl,
  regs_valnums n vl = Some rl ->
  rs##rl = map valu vl.

Lemma find_rhs_sound:
  forall n rh r bc valu ge sp rs m,
  find_rhs n rh = Some r ->
  numbering_holds bc valu ge sp rs m n ->
  exists v, rhs_eval_to valu ge sp m rh v /\ Val.lessdef v rs#r.

Lemma forget_reg_charact:
  forall n rd r v,
  wf_numbering n ->
  In r (PMap.get v (forget_reg n rd)) -> r <> rd /\ In r (PMap.get v n.(num_val)).

Lemma update_reg_charact:
  forall n rd vd r v,
  wf_numbering n ->
  In r (PMap.get v (update_reg n rd vd)) ->
  PTree.get r (PTree.set rd vd n.(num_reg)) = Some v.

Lemma rhs_eval_to_inj:
  forall valu ge sp m rh v1 v2,
  rhs_eval_to valu ge sp m rh v1 -> rhs_eval_to valu ge sp m rh v2 -> v1 = v2.

Lemma add_rhs_holds:
  forall bc valu1 ge sp rs m n rd rh rs',
  numbering_holds bc valu1 ge sp rs m n ->
  rhs_valid bc valu1 ge sp rh ->
  rhs_eval_to valu1 ge sp m rh (rs'#rd) ->
  wf_rhs n.(num_next) rh ->
  (forall r, r <> rd -> rs'#r = rs#r) ->
  exists valu2, numbering_holds bc valu2 ge sp rs' m (add_rhs n rd rh).

Lemma add_op_holds:
  forall bc valu1 ge sp rs m n op (args: list reg) v dst,
  numbering_holds bc valu1 ge sp rs m n ->
  eval_operation ge sp op rs##args m = Some v ->
  exists valu2, numbering_holds bc valu2 ge sp (rs#dst <- v) m (add_op n dst op args).

Lemma add_load_holds:
  forall bc valu1 ge sp rs m n addr (args: list reg) b ofs chunk v dst app ae am,
  numbering_holds bc valu1 ge (Vptr sp Ptrofs.zero) rs m n ->
  eval_addressing ge (Vptr sp Ptrofs.zero) addr rs##args = Some (Vptr b ofs) ->
  Mem.loadv chunk m (Vptr b ofs) = Some v ->
  app = VA.State ae am ->
  ematch bc rs ae ->
  bc sp = BCstack ->
  genv_match bc ge ->
  exists valu2, numbering_holds bc valu2 ge (Vptr sp Ptrofs.zero) (rs#dst <- v) m (add_load app n dst chunk addr args).

Lemma set_unknown_holds:
  forall bc valu ge sp rs m n r v,
  numbering_holds bc valu ge sp rs m n ->
  numbering_holds bc valu ge sp (rs#r <- v) m (set_unknown n r).

Lemma set_res_unknown_holds:
  forall bc valu ge sp rs m n r v,
  numbering_holds bc valu ge sp rs m n ->
  numbering_holds bc valu ge sp (regmap_setres r v rs) m (set_res_unknown n r).

Lemma kill_eqs_charact:
  forall pred l strict r eqs,
  In (Eq l strict r) (kill_eqs pred eqs) ->
  pred r = false /\ In (Eq l strict r) eqs.

Lemma kill_equations_hold:
  forall bc valu ge sp rs m n pred m',
  numbering_holds bc valu ge sp rs m n ->
  (forall r v,
      pred r = false ->
      rhs_valid bc valu ge sp r ->
      rhs_eval_to valu ge sp m r v ->
      rhs_eval_to valu ge sp m' r v) ->
  numbering_holds bc valu ge sp rs m' (kill_equations pred n).

Lemma wkill_eqs_charact:
  forall pred s l r eqs,
  In (Eq l s r) (wkill_eqs pred eqs) ->
  pred r = false /\ s = false /\ (exists strict, In (Eq l strict r) eqs).

Lemma external_call_readonly_load ef ge args m t res m' v chunk b ofs
 (EXTCALL: external_call ef ge args m t res m')
 (LOAD: Mem.load chunk m' b ofs = Some v)
 (VALIDB: Mem.valid_block m b)
 (RO: forall i:Z, ofs <= i < ofs + (size_chunk chunk) -> ~ Mem.perm m b i Max Writable):
 Mem.load chunk m b ofs = Some v.

Lemma kill_all_loads_hold:
  forall rm (bc bc': block_classification) valu ge sp rs m n m' ef args t res am
  (ROM: romatch bc m rm)
  (NUM: numbering_holds bc valu ge sp rs m n)
  (EXTCALL: external_call ef ge args m t res m')
  (MM: mmatch bc m am)
  (BCP: forall b, Plt b (Mem.nextblock m) -> bc' b = bc b),
  numbering_holds bc' valu ge sp rs m' (kill_all_loads rm n).

Lemma kill_loads_after_store_aux:
  forall rm valu sp ge rs m n b ofs chunk v m' bc ap
  (ROHYP: romatch bc m rm)
  (NUM: numbering_holds bc valu ge sp rs m n)
  (STORE: Mem.store chunk m b (Ptrofs.unsigned ofs) v = Some m')
  (PM: pmatch bc b ofs ap),
  numbering_holds bc valu ge sp rs m'
                              (kill_equations (filter_after_store rm n ap (size_chunk chunk)) n).

Lemma kill_loads_after_store_holds:
  forall rm valu ge sp rs m n addr args a chunk v m' bc approx ae am
  (ROHYP: romatch bc m rm),
  numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m n ->
  eval_addressing ge (Vptr sp Ptrofs.zero) addr rs##args = Some a ->
  Mem.storev chunk m a v = Some m' ->
  genv_match bc ge ->
  bc sp = BCstack ->
  ematch bc rs ae ->
  approx = VA.State ae am ->
  numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m'
                           (kill_loads_after_store rm approx n chunk addr args).

Lemma kill_loads_after_vstore_holds:
  forall rm valu ge sp rs m n addr b ofs chunk v m' bc approx ae am t
  (ROHYP: romatch bc m rm)
  (NUM: numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m n)
  (EVAL: eval_builtin_arg ge (fun r : positive => rs # r) (Vptr sp Ptrofs.zero) m addr (Vptr b ofs))
  (VOL: volatile_store ge chunk m b ofs v t m')
  (GE: genv_match bc ge)
  (SP: bc sp = BCstack)
  (EM: ematch bc rs ae)
  (MM: mmatch bc m am)
  (APP: approx = VA.State ae am),
  numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m'
                             (kill_loads_after_vstore rm approx n chunk addr).

Lemma store_normalized_range_sound:
  forall bc chunk v,
  vmatch bc v (store_normalized_range chunk) ->
  Val.lessdef (Val.load_result chunk v) v.


Lemma add_store_result_hold:
  forall valu1 ge sp rs m' n addr args a chunk m src (bc:block_classification) ae approx am
  (BCSP: bc sp = BCstack)
  (GE: genv_match bc ge),
  numbering_holds bc valu1 ge (Vptr sp Ptrofs.zero) rs m' n ->
  eval_addressing ge (Vptr sp Ptrofs.zero) addr rs##args = Some a ->
  Mem.storev chunk m a rs#src = Some m' ->
  genv_match bc ge ->
  bc sp = BCstack ->
  ematch bc rs ae ->
  approx = VA.State ae am ->
  exists valu2, numbering_holds bc valu2 ge (Vptr sp Ptrofs.zero) rs m' (add_store_result approx n chunk addr args src).

Lemma kill_loads_after_storebytes_holds rm valu ge sp rs m n dst b ofs bytes m' bc sz
  (ROHYP: romatch bc m rm):
  numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m n ->
  pmatch bc b ofs dst ->
  Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' ->
  genv_match bc ge ->
  bc sp = BCstack ->
  length bytes = Z.to_nat sz -> sz >= 0 ->
  numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m'
                           (kill_loads_after_storebytes rm n dst sz).


Lemma option_equiv A (x y: option A): (forall v, x = Some v <-> y = Some v) -> x=y.

Lemma load_memcpy:
  forall m b1 ofs1 sz bytes b2 ofs2 m' chunk i,
  Mem.loadbytes m b1 ofs1 sz = Some bytes ->
  Mem.storebytes m b2 ofs2 bytes = Some m' ->
  ofs1 <= i -> i + size_chunk chunk <= ofs1 + sz ->
  (align_chunk chunk | ofs2 - ofs1) ->
  Mem.load chunk m b1 i = Mem.load chunk m' b2 (i + (ofs2 - ofs1)).

Lemma shift_memcpy_eq_wf:
  forall src sz delta e e' next,
  shift_memcpy_eq src sz delta e = Some e' ->
  wf_equation next e ->
  wf_equation next e'.

Lemma shift_memcpy_eq_holds:
  forall (bc:block_classification) src dst sz e e' m sp bytes m' valu ge
  (BCSP: bc sp = BCstack),
  shift_memcpy_eq src sz (dst - src) e = Some e' ->
  Mem.loadbytes m sp src sz = Some bytes ->
  Mem.storebytes m sp dst bytes = Some m' ->
  equation_holds bc valu ge (Vptr sp Ptrofs.zero) m e ->
  equation_holds bc valu ge (Vptr sp Ptrofs.zero) m' e'.

Lemma add_memcpy_eqs_charact:
  forall e' src sz delta eqs2 eqs1,
  In e' (add_memcpy_eqs src sz delta eqs1 eqs2) ->
  In e' eqs2 \/ exists e, In e eqs1 /\ shift_memcpy_eq src sz delta e = Some e'.

Lemma add_memcpy_holds:
  forall m bsrc osrc sz bytes bdst odst m' valu ge sp rs n1 n2 bc asrc adst,
  Mem.loadbytes m bsrc (Ptrofs.unsigned osrc) sz = Some bytes ->
  Mem.storebytes m bdst (Ptrofs.unsigned odst) bytes = Some m' ->
  numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m n1 ->
  numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m' n2 ->
  pmatch bc bsrc osrc asrc ->
  pmatch bc bdst odst adst ->
  bc sp = BCstack ->
  Ple (num_next n1) (num_next n2) ->
  numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m' (add_memcpy n1 n2 asrc adst sz).


Section REDUCE.

Variable A: Type.
Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum).
Variable V: Type.
Variable ge: genv.
Variable sp: val.
Variable rs: regset.
Variable m: mem.
Variable sem: A -> list val -> option V.
Hypothesis f_sound:
  forall eqs valu op args op' args',
  (forall v rhs, eqs v = Some rhs -> rhs_eval_to valu ge sp m rhs (valu v)) ->
  f eqs op args = Some(op', args') ->
  sem op' (map valu args') = sem op (map valu args).
Variable bc: block_classification.
Variable n: numbering.
Variable valu: valnum -> val.
Hypothesis n_holds: numbering_holds bc valu ge sp rs m n.

Lemma reduce_rec_sound:
  forall niter op args op' rl' res,
  reduce_rec A f n niter op args = Some(op', rl') ->
  sem op (map valu args) = Some res ->
  sem op' (rs##rl') = Some res.

Lemma reduce_sound:
  forall op rl vl op' rl' res,
  reduce A f n op rl vl = (op', rl') ->
  map valu vl = rs##rl ->
  sem op rs##rl = Some res ->
  sem op' rs##rl' = Some res.

End REDUCE.


Section REDUCELD.

Variable A: Type.
Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum).
Variable ge: genv.
Variable sp: val.
Variable rs: regset.
Variable m: mem.
Variable sem: A -> list val -> option val.
Hypothesis f_sound:
  forall eqs valu op args op' args' r,
  (forall v rhs, eqs v = Some rhs -> rhs_eval_to valu ge sp m rhs (valu v)) ->
  f eqs op args = Some(op', args') ->
  sem op (map valu args) = Some r ->
  exists r',
  sem op' (map valu args') = Some r' /\ Val.lessdef r r'.
Variable bc: block_classification.
Variable n: numbering.
Variable valu: valnum -> val.
Hypothesis n_holds: numbering_holds bc valu ge sp rs m n.

Lemma reduce_rec_lessdef_sound:
  forall niter op args op' rl' r,
  reduce_rec A f n niter op args = Some(op', rl') ->
  sem op (map valu args) = Some r ->
  exists r',
  sem op' (rs##rl') = Some r' /\ Val.lessdef r r'.

Lemma reduce_lessdef_sound:
  forall op rl vl op' rl' r,
  reduce A f n op rl vl = (op', rl') ->
  map valu vl = rs##rl ->
  sem op rs##rl = Some r ->
  exists r', sem op' rs##rl' = Some r' /\ Val.lessdef r r'.

End REDUCELD.



Theorem analysis_correct_1:
  forall bc ge sp rs m f rm vapprox approx pc pc' i,
  analyze f rm vapprox = Some approx ->
  f.(fn_code)!pc = Some i -> In pc' (successors_instr i) ->
  (exists valu, numbering_holds bc valu ge sp rs m (transfer f rm vapprox pc approx!!pc)) ->
  (exists valu, numbering_holds bc valu ge sp rs m approx!!pc').

Theorem analysis_correct_entry:
  forall bc ge sp rs m f rm vapprox approx,
  analyze f rm vapprox = Some approx ->
  exists valu, numbering_holds bc valu ge sp rs m approx!!(f.(fn_entrypoint)).

Semantic preservation

Section PRESERVATION.

Variable prog: program.
Variable tprog : program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
  forall (s: qualident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match TRANSF).

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_match TRANSF).

Lemma functions_translated:
  forall (v: val) (f: RTL.fundef),
  Genv.find_funct ge v = Some f ->
  exists cu tf, Genv.find_funct tge v = Some tf /\ transf_fundef (romem_for cu) f = OK tf /\ linkorder cu prog.
Proof (Genv.find_funct_match TRANSF).

Lemma funct_ptr_translated:
  forall (b: block) (f: RTL.fundef),
  Genv.find_funct_ptr ge b = Some f ->
  exists cu tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef (romem_for cu) f = OK tf /\ linkorder cu prog.
Proof (Genv.find_funct_ptr_match TRANSF).

Lemma sig_preserved:
  forall rm f tf, transf_fundef rm f = OK tf -> funsig tf = funsig f.

Definition transf_function' (f: function) (approxs: PMap.t numbering) : function :=
  mkfunction
    f.(fn_sig)
    f.(fn_params)
    f.(fn_stacksize)
    (transf_code approxs f.(fn_code))
    f.(fn_entrypoint).

Definition regs_lessdef (rs1 rs2: regset) : Prop :=
  forall r, Val.lessdef (rs1#r) (rs2#r).

Lemma regs_lessdef_regs:
  forall rs1 rs2, regs_lessdef rs1 rs2 ->
  forall rl, Val.lessdef_list rs1##rl rs2##rl.

Lemma set_reg_lessdef:
  forall r v1 v2 rs1 rs2,
  Val.lessdef v1 v2 -> regs_lessdef rs1 rs2 -> regs_lessdef (rs1#r <- v1) (rs2#r <- v2).

Lemma init_regs_lessdef:
  forall rl vl1 vl2,
  Val.lessdef_list vl1 vl2 ->
  regs_lessdef (init_regs vl1 rl) (init_regs vl2 rl).

Lemma find_function_translated:
  forall ros rs fd rs',
  find_function ge ros rs = Some fd ->
  regs_lessdef rs rs' ->
  exists cu tfd, find_function tge ros rs' = Some tfd
              /\ transf_fundef (romem_for cu) fd = OK tfd
              /\ linkorder cu prog.


Definition analyze (cu: program) (f: function) :=
  CSE.analyze f (romem_for cu) (vanalyze (romem_for cu) f).

Inductive match_stackframes: list stackframe -> list stackframe -> Prop :=
  | match_stackframes_nil:
      match_stackframes nil nil
  | match_stackframes_cons:
      forall res sp pc rs f s rs' s' cu approx
           (LINK: linkorder cu prog)
           (ANALYZE: analyze cu f = Some approx)
           (SAT: forall v bc m,
                  exists valu, numbering_holds bc valu ge sp (rs#res <- v) m approx!!pc)
           (RLD: regs_lessdef rs rs')
           (STACKS: match_stackframes s s'),
    match_stackframes
      (Stackframe res f sp pc rs :: s)
      (Stackframe res (transf_function' f approx) sp pc rs' :: s').

Inductive match_states: state -> state -> Prop :=
  | match_states_intro:
      forall bc s sp pc rs m s' rs' m' f cu approx
             (LINK: linkorder cu prog)
             (ANALYZE: analyze cu f = Some approx)
             (SOUND: sound_state_base vrelax cu ge bc (State s f sp pc rs m))
             (SAT: exists valu, numbering_holds bc valu ge sp rs m approx!!pc)
             (RLD: regs_lessdef rs rs')
             (MEXT: Mem.extends m m')
             (STACKS: match_stackframes s s'),
      match_states (State s f sp pc rs m)
                   (State s' (transf_function' f approx) sp pc rs' m')
  | match_states_call:
      forall bc s f tf args m s' args' m' cu
             (LINK: linkorder cu prog)
             (SOUND: sound_state_base vrelax cu ge bc (Callstate s f args m))
             (STACKS: match_stackframes s s')
             (TFD: transf_fundef (romem_for cu) f = OK tf)
             (ARGS: Val.lessdef_list args args')
             (MEXT: Mem.extends m m'),
      match_states (Callstate s f args m)
                   (Callstate s' tf args' m')
  | match_states_return:
      forall s s' v v' m m'
             (STACK: match_stackframes s s')
             (RES: Val.lessdef v v')
             (MEXT: Mem.extends m m'),
      match_states (Returnstate s v m)
                   (Returnstate s' v' m').

Ltac TransfInstr :=
  match goal with
  | H1: (PTree.get ?pc ?c = Some ?instr), f: function, approx: PMap.t numbering |- _ =>
      cut ((transf_function' f approx).(fn_code)!pc = Some(transf_instr approx!!pc instr));
      [ simpl transf_instr
      | unfold transf_function', transf_code; simpl; rewrite PTree.gmap;
        unfold option_map; rewrite H1; reflexivity ]
  end.


Lemma transf_step_correct:
  forall s1 t s2, step ge s1 t s2 ->
  forall s1' (MS: match_states s1 s1') (NXT_SOUND: sound_state vrelax prog s2),
  exists s2', step tge s1' t s2' /\ match_states s2 s2'.

Lemma transf_initial_states:
  forall st1, initial_state prog st1 ->
  exists st2, initial_state tprog st2 /\ match_states st1 st2 .

Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> final_state st1 r -> final_state st2 r.


Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).

End PRESERVATION.