Module Sylvie

Control-flow graph based language to build product programs.

Require Sexpr.
Require RTL.
Import Utf8 RelationClasses Relations.
Import Coqlib Maps.
Import Events Globalenvs Integers Values.
Import Util.
Import Sexpr.

Set Implicit Arguments.
Unset Elimination Schemes.

Notation node := RTL.node.

Definition hashmap X : Type := PTree.t (list X).
Definition ptree_get_all {X} (m: hashmap X) : node → list X :=
λ x, match m ! x with Some s => s | None => nil end.
Coercion ptree_get_all : hashmap >-> Funclass.

Section REGISTER.

Variable reg : Type.
Context (reg_dec: EqDec reg).

Inductive operation : Type :=
| Havoc
| Operation (op: Op.operation).

Global Instance operation_dec : EqDec operation.

Proof.

  intros x x'.
  refine
  match x, x' with
  | Havoc, Havoc => left eq_refl
  | Operation o, Operation o' =>
    match Op.eq_operation o o' with
    | left EQ => left (f_equal Operation EQ)
    | right NE => right _
    end
  | _, _ => right _
  end; try abstract congruence.
Defined.

Inductive edge : Type :=
| Egoto (i: node)
| Ebranch (cond: Op.condition) (args: list reg) (t f: node)
| Eop (dst: reg) (op: operation) (args: list reg) (i: node)
| Estop
.

Global Instance edge_dec : EqDec edge.

Proof.

  intros e e'.
  refine
  match e, e' with
  | Egoto i, Egoto i' =>
    match eq_dec i i' with
    | left EQ => left (f_equal Egoto EQ)
    | right NE => right _
    end
  | Ebranch cond args t f, Ebranch cond' args' t' f' =>
    match Op.eq_condition cond cond' with
    | left EQ =>
      match eq_dec args args' with
      | left EQa =>
        match eq_dec t t' with
        | left EQt =>
          match eq_dec f f' with
          | left EQf => left (f_equal4 Ebranch EQ EQa EQt EQf)
          | right NE => right _
          end
        | right NE => right _
        end
      | right NE => right _
      end
    | right NE => right _
    end
  | Eop dst op args i, Eop dst' op' args' i' =>
    match eq_dec dst dst' with
    | left EQ =>
      match eq_dec op op' with
      | left EQo =>
        match eq_dec args args' with
        | left EQa =>
          match eq_dec i i' with
          | left EQi => left (f_equal4 Eop EQ EQo EQa EQi)
          | right NE => right _
          end
        | right NE => right _
        end
      | right NE => right _
      end
    | right NE => right _
    end
  | Estop, Estop => left eq_refl
  | _, _ => right _
  end; try abstract congruence.
Defined.

Definition successors (e: edge) : list node :=
  match e with
  | Egoto i
  | Eop _ _ _ i
    => i :: nil
  | Ebranch _ _ t f => t :: f :: nil
  | Estop => nil
  end.

Definition code : Type := PTree.t edge.

Definition make_predecessors (c: code) : PTree.t (list (node * option bool)) :=
  PTree.fold
    (λ (m: hashmap (positive * option bool)) pc e,
     match successors e with
     | i :: nil => PTree.set i ((pc, None) :: m i) m
     | t :: f :: nil =>
       if Pos.eqb t f
       then PTree.set t ((pc, None) :: m t) m
       else
       let m : hashmap _ := PTree.set t ((pc, Some true) :: m t) m in
       PTree.set f ((pc, Some false) :: m f) m
     | _ => m
     end)
    c (PTree.empty _).

Record function : Type :=
  Function {
      fn_code: code;
      fn_entrypoint: node
    }.

Definition env : Type := reg → val.

Definition eq_env (e e': env) : Prop :=
  ∀ r, e r = e' r.

Instance eq_env_equiv: Equivalence eq_env.

Proof.

  constructor.
  exact (λ x r, eq_refl).
  exact (λ x y Hxy r, eq_sym (Hxy r)).
  exact (λ x y z Hxy Hyz r, eq_trans (Hxy r) (Hyz r)).
Qed.

Record rstate : Type :=
  State {
      pc: node;
      e: env
    }.

Inductive state : Type :=
| Run `(rstate)
| Stop.

Section SEM.

Context (find_symbol: AST.ident → option block) (sp: val) (valid_pointer: block → Z → bool) (fn: function).

Definition step (s: state) (s': state) : Prop :=
  match s with
  | Run s =>
    match (fn_code fn) ! (pc s) with
    | None => False
    | Some i =>
      match i with
      | Egoto j => ∃ e', eq_env (e s) e' ∧ s' = Run (State j e')
      | Ebranch cond args t f =>
        let vargs := List.map (e s) args in
        ∃ b, eval_condition valid_pointer cond vargs = Some b ∧
             ∃ e', eq_env (e s) e' ∧ s' = Run (State (if b then t else f) e')
      | Eop dst (Operation op) args j =>
        let vargs := List.map (e s) args in
        ∃ v, eval_operation find_symbol sp valid_pointer op vargs = Some v ∧
             ∃ e', upd_spec (e s) dst v e' ∧ s' = Run (State j e')
      | Eop dst Havoc _ j =>
        ∃ e' v, upd_spec (e s) dst v e' ∧ s' = Run (State j e')
      | Estop =>
        s' = Stop
      end
    end
  | Stop => False
  end.

Definition initial_state (pre: env → Prop) (s: state) : Prop :=
  ∃ rs, s = Run rs ∧ (pc rs) = (fn_entrypoint fn) ∧ pre (e rs).

Definition final_state (s: state) : Prop :=
  s = Stop.

Definition reachable (pre: env → Prop) (s: state) : Prop :=
  ∃ ι, initial_state pre ι ∧ clos_refl_trans _ step ι s.

Lemma reachable_step {pre s s'} :
  reachable pre s →
  step s s' →
  reachable pre s'.

Proof.

  intros (i & INIT & STAR) STEP.
  exists i. split. exact INIT.
  clear INIT. vauto.
Qed.

Definition invariant (pre: env → Prop) (i: state → Prop) : Prop :=
  reachable pre ⊆ i.

Definition invariant_weaken (i j: state → Prop) pre :
  i ⊆ j →
  invariant pre i →
  invariant pre j :=
  λ Hij Hi s R, Hij s (Hi s R).

Section INVARIANT.

Context (pre: env → Prop).
Context (P: state → Prop).

Hypothesis invariant_init : initial_state pre ⊆ P.

Hypothesis invariant_step :
  ∀ s, reachable pre s → P s → step s ⊆ P.

Theorem invariant_ind: invariant pre P.

Proof.

  intros s (i & INIT & STAR).
  assert (reachable pre i) as REACH by ( exists i; vauto ).
  apply invariant_init in INIT.
  apply clos_rt_rt1n in STAR.
  induction STAR. exact INIT. eauto using reachable_step.
Qed.

End INVARIANT.

Context (deco: node → list (assertion reg)).

Definition well_annotated_state (s: state) : Prop :=
  match s with
  | Stop => Logic.True
  | Run rs => ∀ a, In a (deco (pc rs)) → eval_assertion reg_dec find_symbol sp valid_pointer (e rs) a
  end.

Definition well_annotated_function (pre: env → Prop) : Prop :=
    invariant pre well_annotated_state.

End SEM.

End REGISTER.

Arguments Egoto {reg} _.
Arguments Estop {reg}.
Arguments invariant_weaken [reg reg_dec find_symbol sp valid_pointer fn] _ _ _ _ _ _ _.