Library C_cmd

Require Import ssreflect ssrbool.
Require Import Arith_ext ZArith_ext String_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
Require Import C_types C_expr C_bipl.

Inductive cmd0 : Type :=
| skip
| assign of var & exp
| lookup of var & exp
| mutation of exp & exp
| malloc of var & exp
| free of exp.

Notation "x <- e" := (assign x e) (at level 80) : minC_cmd_scope.
Notation "x '<-*' e" := (lookup x e) (at level 80) : minC_cmd_scope.
Notation "e '*<-' f" := (mutation e f) (at level 80) : minC_cmd_scope.
Notation "x '<-malloc' e" := (malloc x e) (at level 80) : minC_cmd_scope.
Local Open Scope minC_cmd_scope.

Definition state := (store * hp.t)%type.

Local Open Scope zarith_ext_scope.
Local Open Scope heap_scope.
Local Open Scope minC_expr_scope.

Parameter ctrl : nat -> hp.t. Parameter ctrl_len : forall a h, h = ctrl a -> nat. Parameter block_len : forall a h, h = ctrl a -> nat.
Notation "'Block_len' b" := (block_len _ b (refl_equal _))
  (at level 76) : minC_cmd_scope.

Local Open Scope minC_types.

Require Import nodup.

Local Open Scope machine_int_scope.

Reserved Notation " s '--' c '---->' t " (at level 74, no associativity).

Inductive exec0 : option state -> cmd0 -> option state -> Prop :=
| exec0_skip : forall s, Some s -- skip ----> Some s

| exec0_assign : forall (s : store) h (x : var) (t : typ) (e : exp) (v : value),
  [ e ]_ s = Some v ->
  typof s (var_e x) =ot _ctxt s ot= t ->
  typof s e =ot (_ctxt s) ot= t ->
  Some (s, h) -- x <- e ----> Some (store_upd x v s, h)

| exec0_assign_err : forall s h (x : var) (e : exp),
  (~ (exists tx, typof s (var_e x) =ot _ctxt s ot= tx) \/
    (exists tx, typof s (var_e x) =ot _ctxt s ot= tx /\
        (~ typof s e =ot (_ctxt s) ot= tx \/
          [ e ]_ s = None))) ->
  Some (s, h) -- x <- e ----> None

| exec0_lookup : forall s h tx x e v p,
  typof s (var_e x) =ot _ctxt s ot= tx ->
  typof s e =ot (_ctxt s) ot= ptyp tx ->
  [ e ]_ s = Some (pval p) ->
  heap_get (Zabs_nat (u2Z p)) tx h = Some v ->
  Some (s, h) -- x <-* e ----> Some (store_upd x v s, h)

| exec0_lookup_err : forall (s : store) h (x : var) (e : exp),
  (~ (exists tx, typof s (var_e x) =ot _ctxt s ot= tx ) \/
    (exists tx, typof s (var_e x) =ot _ctxt s ot= tx /\
        (~ typof s e =ot (_ctxt s) ot= ptyp tx \/
          ( ( (~ exists p, [ e ]_ s = Some (pval p)) \/ (
            typof s e =ot (_ctxt s) ot= ptyp tx /\
            (exists p, [ e ]_ s = Some (pval p) /\
              heap_get (Zabs_nat (u2Z p)) tx h = None))))))) ->
  Some (s, h) -- x <-* e ----> None
  
| exec0_mutation : forall (s : store) h t (e : exp) (e' : exp) p v v',
  wf_tstore (_tstore s) ->
  [ e ]_ s = Some (pval p) ->
  typof s e =ot (_ctxt s) ot= ptyp t ->
  heap_get (Zabs_nat (u2Z p)) t h = Some v ->
  [ e' ]_ s = Some v' ->
  typof s e' =ot (_ctxt s) ot= t ->
  Some (s, h) -- e *<- e' ----> Some (s, heap_upd (Zabs_nat (u2Z p)) v' t h)

| exec0_mutation_err : forall (s : store) h (e1 e2 : exp),
  ((~ exists p, [ e1 ]_s = Some (pval p)) \/
  (exists p, [ e1 ]_s = Some (pval p) /\
    (~ (exists t : typ, typof s e1 =ot _ctxt s ot= ptyp t) \/
      (exists t, typof s e1 =ot (_ctxt s) ot= ptyp t /\
        ((heap_get (Zabs_nat (u2Z p)) t h = None \/
          (exists v, heap_get (Zabs_nat (u2Z p)) t h = Some v /\
            ([ e2 ]_ s = None \/
              (exists v2, [ e2 ]_ s = Some v2 /\
                ~ typof s e2 =ot (_ctxt s) ot= t))))))))) ->
  Some (s, h) -- e1 *<- e2 ----> None

| exec0_malloc : forall s h t x e a v l (lst : list (int 8)),
  typof s (var_e x) =ot _ctxt s ot= ptyp t ->
  wft t ->
  [ e ]_s = Some (bval32 v) ->
  u2Z v <> 0%Z ->
  l = sizeof t ->
  length lst = (Zabs_nat (u2Z v) * l)%nat ->
  (0 <= Z_of_nat (a + (Zabs_nat (u2Z v)) * l) < 2 ^^ ptr_len)%Z ->
  h # ctrl a ->
  h # chars2heap a lst ->
  ctrl a # chars2heap a lst ->
  (Block_len (ctrl a)) = length lst ->
  Some (s, h) -- x <-malloc e ---->
  Some (store_upd x (pval (Z2u ptr_len (Z_of_nat a))) s, h +++ ctrl a +++ chars2heap a lst)

| exec0_free : forall s h (e : exp) p,
  [ e ]_ s = Some (pval p) ->
  ctrl (Zabs_nat (u2Z p)) [<=m] h ->

    incl (seq (Zabs_nat (u2Z p)) (Block_len (ctrl (Zabs_nat (u2Z p))))) (seq_ext.s2l (hp.dom h)) ->

  Some (s, h) -- free e ---->
    Some (s, h [\m]
      (seq_ext.l2s (seq (Zabs_nat (u2Z p)) (Block_len (ctrl (Zabs_nat (u2Z p)) ))))
    [\m] hp.dom (ctrl (Zabs_nat (u2Z p))))

| exec0_free_err : forall s h (e : exp),
  [ e ]_ s = None \/
  (exists p, [ e ]_ s = Some (pval p) /\ ~ ctrl (Zabs_nat (u2Z p)) [<=m] h) ->
  Some (s, h) -- free e ----> None

where "s -- c ----> t" := (exec0 s c t) : minC_cmd_scope.

Require while.

Coercion cmd_cmd0_coercion := @while.cmd_cmd0 cmd0 bexp.

Lemma eval_b_neg : forall t s, [ bneg t ]b_ s = ~~ [ t ]b_ s.

Lemma from_none0 : forall c s, None -- c ----> s -> s = None.

Lemma cmd0_terminate : forall (c : cmd0) s, exists s', Some s -- c ----> s'.

Module MINC_Semop <: while.WHILE_SEMOP.

Definition store : Type := store.
Definition heap : Type := hp.t.
Definition state : Type := (store * heap)%type.

Definition cmd0 : Type := cmd0.

Definition exec0 : option state -> cmd0 -> option state -> Prop := exec0.
Notation "s -- c ----> t" := (exec0 s c t) (at level 74 , no associativity) : minC_cmd_scope.
Local Open Scope minC_cmd_scope.

Definition from_none0 : forall c s, None -- c ----> s -> s = None := from_none0.
Definition cmd0_terminate : forall (c : cmd0) s, exists s', Some s -- c ----> s' := cmd0_terminate.

Definition expr_b : Type := bexp.
Definition neg : expr_b -> expr_b := bneg.
Definition eval_b : expr_b -> state -> bool := fun eb s => [ eb ]b_ (fst s).
Lemma eval_b_neg : forall t s, eval_b (neg t) s = ~~ eval_b t s.
Definition cmd := @while.cmd cmd0 expr_b.
Coercion cmd_cmd0_coercion := @while.cmd_cmd0 cmd0 expr_b.
Definition exec : option state -> cmd -> option state -> Prop := (@while.exec store _ cmd0 exec0 expr_b eval_b).

End MINC_Semop.

Notation "c ; d" := (while.seq c d) (at level 81, right associativity) : minC_cmd_scope.

Module minC_semop_prop_m := while.While_Semop_Prop MINC_Semop.