Require Export Programs.
Require Export Outcomes.

Inductive cchunk_id := points_to_id(l: Z) | malloc_block_id(l: Z).

Definition cchunk_id_dec (i1 i2: cchunk_id): {i1 = i2} + {i1 '_x"><> i2}.
Defined.

Definition cheap := cchunk_id -> option Z.
Definition cstate := (store * cheap)%type.

Definition cheap_update (h: cheap) l v l' := if cchunk_id_dec l l' then v else h l'.

Section RoutineDefs.

Variable routine_defs: routine_table.

Definition coutcome A := outcome cstate A.
Definition cmutatora A := cstate -> coutcome A.
Definition cmutator := cmutatora unit.

Definition pick{S}: mutator S S Z :=
  fun st => demonic (set_img Z_set (fun z => single st z)).

Definition assumeb(b: bool): cmutator :=
  fun st => if b then single st tt else oblock.

Definition update_cstore x v: cmutator :=
  fun st => let (s, h) := st in
  single (store_update s x v, h) tt.

Definition cwith_store s {A} (C: cmutatora A): cmutatora A :=
  fun st => let (s0, h) := st in
  bindf (C (s, h)) (fun a st' => let (_, h') := st' in single (s0, h') a).

Definition ceval_mut(e: expr): cmutatora Z :=
  fun st => let (s, h) := st in
  single st (eval s e).

Definition cevals_mut(es: list expr) :=
  fun st: cstate => let (s, h) := st in
  single st (map (eval s) es).

Definition cassume_bexpr(b: bexpr): cmutator :=
  fun st => let (s, h) := st in
  if beval s b then single st tt else oblock.

Definition ccons_chunk i: cmutatora Z :=
  fun st => let (s, h) := st in
  match h i with
    None => ofail
  | Some v => single (s, cheap_update h i None) v
  end.

Definition ccons_pointsto l: cmutatora Z := ccons_chunk (points_to_id l).

Definition ccons_malloc_block l: cmutatora Z := ccons_chunk (malloc_block_id l).

Fixpoint ccons_pointstos l n :=
  match n with
    O => noop
  | S n =>
    ccons_pointsto l;
    ccons_pointstos (l + 1) n
  end.

Definition cprod_chunk i v: cmutator :=
  fun st => let (s, h) := st in
  match h i with
    None => single (s, cheap_update h i (Some v)) tt
  | Some _ => oblock
  end.

Definition cprod_pointsto l v: cmutator := cprod_chunk (points_to_id l) v.

Fixpoint cprod_pointstos l n :=
  match n with
    O => noop
  | S n =>
    v <- pick;
    cprod_pointsto l v;
    cprod_pointstos (l + 1) n
  end.

Fixpoint fpow(n: nat){A}(f: A -> A)(x: A): A :=
  match n with
    O => x
  | S n => f (fpow n f x)
  end.

Definition iterate_n(n: nat){S}(C: mutator S S unit): mutator S S unit :=
  fpow n (fun C' => fork (C; C') noop) block.

Definition iterate{S}(C: mutator S S unit): mutator S S unit :=
  n <- pick;
  iterate_n (Z.to_nat n) C.

Fixpoint c_exec_n(n: nat)(c: cmd): cmutator :=
  match n with
    O => block
  | S n =>
    match c with
    | Assign x e =>
      v <- ceval_mut e;
      update_cstore x v
    | Malloc x n =>
      l <- pick;
      update_cstore x l;
      assumeb (Z_ltb 0 l);
      cprod_chunk (malloc_block_id l) (Z.of_nat n);
      cprod_pointstos l n
    | Free e =>
      l <- ceval_mut e;
      n <- ccons_malloc_block l;
      ccons_pointstos l (Z.to_nat n)
    | Read x e =>
      l <- ceval_mut e;
      v <- ccons_pointsto l;
      cprod_pointsto l v;
      update_cstore x v
    | Write e1 e2 =>
      l <- ceval_mut e1;
      v <- ceval_mut e2;
      _ <- ccons_pointsto l;
      cprod_pointsto l v
    | Call x r es =>
      match routine_defs r with
        None => fail
      | Some (RoutineDef xs c') =>
        vs <- cevals_mut es;
        v <- cwith_store (store_updates store0 xs vs) (c_exec_n n c'; ceval_mut result);
        update_cstore x v
      end
    | IfCmd b c1 c2 =>
      fork (
        cassume_bexpr b;
        c_exec_n n c1
      ) (
        cassume_bexpr (b_not b);
        c_exec_n n c2
      )
    | While b a c =>
      iterate (
        cassume_bexpr b;
        c_exec_n n c
      );
      cassume_bexpr (b_not b)
    | Seq c1 c2 =>
      c_exec_n n c1;
      c_exec_n n c2
    | Open p es => noop
    | Close p es => noop
    | Skip => noop
    | Message m => message_mut m
    end
  end.

Definition c_exec(c: cmd): cmutator :=
  n <- pick;
  c_exec_n (Z.to_nat n) c.

Definition cheap0: cheap := fun _ => None.
Definition cstate0 := (store0, cheap0).

Definition cvalid_program(c: cmd): Prop :=
  safe (cstate0 '_x">|> c_exec c).

Fixpoint is_ofail{A}(o: coutcome A): Prop :=
  match o with
    angelic (set_ n_Empty_set _) => True
  | _ => False
  end.

Fixpoint subformula{A}(f: coutcome A)(ps: list Z) {struct ps}: coutcome A :=
  match ps with
    nil => f
  | p::ps =>
    match f with
      demonic (set_ n_Z F) => subformula (F p) ps
    | demonic (set_ n_bool F) =>
      if Z_eq_dec p 0 then
        subformula (F true) ps
      else
        subformula (F false) ps
    | _ => f
    end
  end.

Lemma is_ofail_subformula_not_safe A ps:
  forall (o: coutcome A),
  is_ofail (subformula o ps) -> ~ safe o.

End RoutineDefs.

Open Local Scope string_scope.

Inductive outcome_kind :=
  o_single | o_block | o_fork | o_demonic | o_fail | o_fork_angelic | o_angelic | o_message(m: string).

Fixpoint get_outcome_kind{A}(o: coutcome A): outcome_kind :=
  match o with
    single _ _ => o_single
  | demonic (set_ n_Empty_set _) => o_block
  | demonic (set_ n_bool _) => o_fork
  | demonic _ => o_demonic
  | angelic (set_ n_Empty_set _) => o_fail
  | angelic (set_ n_bool _) => o_fork_angelic
  | angelic _ => o_angelic
  | message m _ => o_message m
  end.

Fixpoint get_outcome_kinds{A}(f: coutcome A)(ps: list Z): list (Z * outcome_kind) :=
  match ps with
    nil => nil
  | p::ps =>
    (p, get_outcome_kind f)::
    match f with
      demonic (set_ n_Z F) => get_outcome_kinds (F p) ps
    | demonic (set_ n_bool F) =>
      if Z_eq_dec p 0 then
        get_outcome_kinds (F true) ps
      else
        get_outcome_kinds (F false) ps
    | message m o => get_outcome_kinds o ps
    | _ => nil
    end
  end.

Definition is_single{A}(o: coutcome A): Prop :=
  match o with
    single _ _ => True
  | _ => False
  end.

Local Notation x := "x".
Local Notation y := "y".
Local Notation z := "z".

Definition rt0: routine_table := fun _ => None.

Goal is_ofail (c_exec_n rt0 1 (x ':=' [0]) cstate0).

Definition exec0 c := c_exec rt0 c cstate0.

Definition assert b := (If b Then Skip Else call "fail"())%cmd.

Goal is_single
  (subformula
    (exec0 (
       x ':=' malloc(2); [x] ':=' 0; [x + 1] ':=' 1;
       y ':=' [x + 1];
       assert (y == 1)
     ))
    [10, 17, 42, 19, 0]).

Goal is_ofail
  (subformula
    (exec0 (
       x ':=' malloc(2); [x] ':=' 0; [x + 1] ':=' 1;
       y ':=' [x + 1];
       assert (y == 0)
     ))
    [10, 17, 42, 19, 1]).

Local Notation a := "a".
Local Notation b := "b".
Local Notation tail := "tail".

Definition make_range :=
  RoutineDef [a, b] (
    If a == b Then
      result ':=' 0
    Else (
      tail ':=' call "make_range"(a + 1, b);
      result ':=' malloc(2); [result] ':=' a; [result + 1] ':=' tail
    )
  ).

Definition reverse :=
  RoutineDef [a, b] (
    If a == 0 Then
      result ':=' b
    Else (
      tail ':=' [a + 1];
      [a + 1] ':=' b;
      result ':=' call "reverse"(tail, a)
    )
  ).

Definition dispose :=
  RoutineDef [a] (
    If a == 0 Then
      Skip
    Else (
      tail ':=' [a + 1];
      free(a);
      call "dispose"(tail)
    )
  ).

Definition reverse_loop :=
  RoutineDef [a] (
    while ~ (a == 0) invariant b_true do (
      tail ':=' [a + 1];
      [a + 1] ':=' b;
      b ':=' a;
      a ':=' tail
    );
    result ':=' b
  ).

Definition dispose_loop :=
  RoutineDef [a] (
    while ~ (a == 0) invariant b_true do (
      tail ':=' [a + 1];
      free(a);
      a ':=' tail
    )
  ).

Definition my_rt :=
  fun r =>
    if string_dec r "make_range" then Some make_range else
    if string_dec r "reverse" then Some reverse else
    if string_dec r "reverse_loop" then Some reverse_loop else
    if string_dec r "dispose" then Some dispose else
    if string_dec r "dispose_loop" then Some dispose_loop else
    None.

Definition reverse_test :=
  (
    a ':=' call "make_range"(0, 5);
    b ':=' call "reverse"(a, 0);
    a ':=' call "reverse"(b, 0);
    call "dispose"(a)
  )%cmd.

Goal
  is_single
    (subformula
       (c_exec my_rt reverse_test cstate0)
       [200, 1, 1, 1, 1, 1, 0, 410, 9, 9, 310, 9, 9, 210, 9, 9, 110, 9, 9, 10, 9, 9, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 1, 0]).

Definition reverse_test_broken :=
  (
    a ':=' call "make_range"(0, 5);
    b ':=' call "reverse"(a, 0);
    call "reverse"(b + 10, 0)
  )%cmd.

Goal
  is_ofail
    (subformula
       (c_exec my_rt reverse_test_broken cstate0)
       [200, 1, 1, 1, 1, 1, 0, 410, 9, 9, 310, 9, 9, 210, 9, 9, 110, 9, 9, 10, 9, 9, 1, 1, 1, 1, 1, 0, 1]).

Definition reverse_loop_test :=
  (
    a ':=' call "make_range"(0, 5);
    b ':=' call "reverse_loop"(a, 0);
    a ':=' call "reverse_loop"(b, 0);
    call "dispose_loop"(a)
  )%cmd.

Goal
  is_single
    (subformula
       (c_exec my_rt reverse_loop_test cstate0)
       [200, 1, 1, 1, 1, 1, 0, 410, 9, 9, 310, 9, 9, 210, 9, 9, 110, 9, 9, 10, 9, 9, 50, 0, 0, 0, 0, 0, 1, 50, 0, 0, 0, 0, 0, 1, 50, 0, 0, 0, 0, 0, 1]).

Definition reverse_loop_test_broken :=
  (
    a ':=' call "make_range"(0, 5);
    b ':=' call "reverse_loop"(a, 0);
    call "reverse_loop"(b + 10, 0)
  )%cmd.

Goal
  is_ofail
    (subformula
       (c_exec my_rt reverse_loop_test_broken cstate0)
       [200, 1, 1, 1, 1, 1, 0, 410, 9, 9, 310, 9, 9, 210, 9, 9, 110, 9, 9, 10, 9, 9, 50, 0, 0, 0, 0, 0, 1, 50, 0]).