example.v

From Coq Require Import Strings.String.
From Coq Require Import Init.Nat.
From Coq Require Import Bool.Bool.
From Coq Require Import Arith.Arith.
From Coq Require Import Lists.List.
From Coq Require Import Program.Wf.
From Hammer Require Import Tactics.

(* A simplified version of a symbolic interpreter for an o-o language.
   Expressions are evaluated against heaps. Values can be either 
   concrete (numbers or references to the heap) or symbolic 
   (just references to the heap). Symbolic values stand for
   unknown inputs provided before the start of the execution. *)

Definition field_name : Type := string.

Inductive value : Type := 
| Unassumed : value     (* a symbol for an unspecified value of any type *)
| Nat : nat -> value    (* a natural value *)
| Null : value          (* the null reference *)
| Loc : nat -> value    (* a nonnull concrete reference to the heap *)
| Symbol : nat -> value (* a symbolic reference to the heap *)
| Equ : value -> value -> value (* a term expressing equality of two values *)
| Ite : value -> value -> value -> value. (* an if-then-else term *)

Inductive expression : Type :=
(* Value v evaluates to v *)
| Value : value -> expression
(* Getfield e f evaluates to the value of field f of object e *)
| Getfield : expression -> field_name -> expression 
(* Putfield e1 f e2 evaluates to (the evaluation of) e2; as a side
   effect puts the value (obtained by evaluating) e2 into field f 
   of object e1 *)
| Putfield : expression -> field_name -> expression -> expression. 

Definition object : Type := field_name -> option value.

Definition heap : Type := nat -> option object.

Definition config : Type := heap * expression.

(* An object of which we do not assume anything about
   the values stored in its fields *)
Definition empty_object : object :=
  fun fname => Some Unassumed.
  (* well, here the fields that do not belong to the
     class of empty_object should be mapped to None, 
     but we gloss over this detail. *)

(* 'Updates' an object o by 'setting' the value of 
   field f to v *)
Definition update_object (o : object) (f : field_name) (v : value) : object :=
  fun fname => if String.eqb fname f then Some v else o fname.

(* 'Updates' a heap H by 'setting' the object at position n to o *)
Definition update_heap (H : heap) (n : nat) (o : object) : heap :=
  fun pos => if Nat.eqb pos n then Some o else H pos.

(* Merges two heaps obtained by distinct updates applied to a same 
   starting heap into a heap with conditional field values 
   (see the semantics of Putfield) *) 
Definition merge (H1' H2' : heap) (cond: value) (fname : string) : heap :=
  fun pos => 
    match H1' pos, H2' pos with
    | None, None => None
    | Some o1', None => Some o1'
    | None, Some o2' => Some o2'
    | Some o1', Some o2' => 
      Some (fun f => if String.eqb f fname then 
        match o1' fname, o2' fname with
        | None, None => None
        | Some v1, None => Some (Ite cond v1 Unassumed)
        | None, Some v2 => Some (Ite cond Unassumed v2)
        | Some v1, Some v2 => Some (Ite cond v1 v2)
        end else o1' f)
    end.


(* Declarative step relation *)
(* Some comments: 
   - A concrete nonnull reference,
     i.e., a Loc n, always has an associated object
     in a heap. On converse, a Symbol n may initially
     have no associated object in a heap, so upon 
     first access to the heap by the symbol the
     heap must be refined by adding an empty object
     associated to the symbol. In other words, even
     a Getfield, a read operation, may have a side
     effect on the heap.
   - The ite values are introduced to model the effect
     of some kinds of operations on symbolic values,
     that are not represented in this simplified version
     of the specification.
   - For the sake of simplicity both Symbol n and
     Loc n encapsulate in n the heap position of the
     corresponding object, but in the real specification 
     the heap management is less hackish.
*)

Reserved Notation " x '-->' y " (at level 50, left associativity).

Inductive step_decl : config -> config -> Prop :=
| StepGetfield1: forall H e e' fname n o v,
  e = Getfield (Value (Loc n)) fname ->
  H n = Some o -> 
  o fname = Some v ->
  e' = Value v ->
  (H, e) --> (H, e')
| StepGetfield2: forall H e e' fname n o v,
  e = Getfield (Value (Symbol n)) fname ->
  H n = Some o -> 
  o fname = Some v ->
  e' = Value v ->
  (H, e) --> (H, e')
| StepGetfield3: forall H H' e e' fname n o v,
  e = Getfield (Value (Symbol n)) fname ->
  H n = None -> 
  o = empty_object -> (* In the real specification, o fname is updated with a symbol standing for the unknown value *)
  H' = update_heap H n o ->
  o fname = Some v ->
  e' = Value v ->
  (H, e) --> (H', e')
| StepGetfield4: forall H Htmp H' e e' e1 e2 cond v1 v1' v2 v2' fname,
  e = Getfield (Value (Ite cond v1 v2)) fname ->
  e1 = Getfield (Value v1) fname ->
  (H, e1) --> (Htmp, Value v1') ->
  e2 = Getfield (Value v2) fname ->
  (Htmp, e2) --> (H', Value v2') ->
  e' = Value (Ite cond v1' v2') ->
  (H, e) --> (H', e')
| StepPutfield1 : forall H H' n o o' e e' fname v,
  e = Putfield (Value (Loc n)) fname (Value v) ->
  H n = Some o ->
  o' = update_object o fname v ->
  H' = update_heap H n o' ->
  e' = Value v ->
  (H, e) --> (H', e')
| StepPutfield2 : forall H H' n o o' e e' fname v,
  e = Putfield (Value (Symbol n)) fname (Value v) ->
  H n = Some o ->
  o' = update_object o fname v ->
  H' = update_heap H n o' ->
  e' = Value v ->
  (H, e) --> (H', e')
| StepPutfield3 : forall H H' n o' e e' fname v,
  e = Putfield (Value (Symbol n)) fname (Value v) ->
  H n = None ->
  o' = update_object empty_object fname v ->
  H' = update_heap H n o' ->
  e' = Value v ->
  (H, e) --> (H', e')
| StepPutfield4 : forall H H' H1' H2' e e' e1 e2 fname v v1 v2 cond,
  e = Putfield (Value (Ite cond v1 v2)) fname (Value v) ->
  e1 = Putfield (Value v1) fname (Value v) ->
  (H, e1) --> (H1', Value v) ->
  e2 = Putfield (Value v2) fname (Value v) ->
  (H, e2) --> (H2', Value v) ->
  H' = merge H1' H2' cond fname ->
  e' = Value v ->
  (H, e) --> (H', e') 
| Ctx1 : forall H H' e e' fname,
  (H, e) --> (H', e') ->
  (H, Getfield e fname) --> (H', Getfield e' fname)
| Ctx2 : forall H H' e1 e1' e2 fname,
  (H, e1) --> (H', e1') ->
  (H, Putfield e1 fname e2) --> (H', Putfield e1' fname e2)
| Ctx3 : forall H H' e2 e2' fname v1,
  (H, e2) --> (H', e2') ->
  (H, Putfield (Value v1) fname e2) --> (H', Putfield (Value v1) fname e2')
where " x '-->' y " := (step_decl x y).

(* Function for step *)

Fixpoint height_v (v : value) : nat :=
  match v with
  | Unassumed => 0
  | Nat _ => 0
  | Null => 0
  | Loc _ => 0
  | Symbol _ => 0
  | Equ v1 v2 => (Nat.max (height_v v1) (height_v v2)) + 1
  | Ite v1 v2 v3 => (Nat.max (height_v v1) (Nat.max (height_v v2) (height_v v3))) + 1
  end.

Fixpoint height (e : expression) : nat :=
  match e with
  | Value v => height_v v + 1
  | Getfield e1 _ => height e1 + 1
  | Putfield e1 _ e2 => height e1 + height e2 + 1
  end.

Program Fixpoint step_comp (H : heap) (e : expression) {measure (height e)} : option config :=
  match e with
  | Getfield (Value (Loc n)) fname =>
    match H n with
    | Some o => match o fname with
      | Some v => 
        let e' := Value v in
        Some (H, e')
      | _ => None
      end
    | _ => None
    end
  | Getfield (Value (Symbol n)) fname =>
    match H n with
    | Some o => match o fname with
      | Some v => 
        let e' := Value v in
        Some (H, e')
      | _ => None
      end
    | None => 
      let H' := update_heap H n empty_object in
      match H' n with
      | Some o => match o fname with
        | Some v => 
          let e' := Value v in
          Some (H', e')
        | _ => None
        end
      | _ => None
      end
    end
  | Getfield (Value (Ite cond v1 v2)) fname =>
    let e1 := Getfield (Value v1) fname in
    let e2 := Getfield (Value v2) fname in
    match step_comp H e1 with
    | Some (Htmp, Value v1') => match step_comp Htmp e2 with
      | Some (H', Value v2') =>
        let e' := Value (Ite cond v1' v2') in
        Some (H', e')
      | _ => None
      end
    | _ => None
    end
  | Putfield (Value (Loc n)) fname (Value v) =>
    match H n with
    | Some o => 
      let o' := update_object o fname v in
      let H' := update_heap H n o' in
      let e' := Value v in
      Some (H', e')
    | _ => None
    end
  | Putfield (Value (Symbol n)) fname (Value v) =>
    match H n with
    | Some o => 
      let o' := update_object o fname v in
      let H' := update_heap H n o' in
      let e' := Value v in
      Some (H', e')
    | None =>
      let o' := update_object empty_object fname v in
      let H' := update_heap H n o' in
      let e' := Value v in
      Some (H', e')
    end
  | Putfield (Value (Ite cond v1 v2)) fname (Value v) =>
    let e1 := Putfield (Value v1) fname (Value v) in
    let e2 := Putfield (Value v2) fname (Value v) in
    match step_comp H e1, step_comp H e2 with
    | Some (H1', _), Some (H2', _) =>
      let H' := merge H1' H2' cond fname in
      let e' := Value v in
      Some (H', e')
    | _, _ => None
    end
  | Getfield e fname => match step_comp H e with
    | Some (H', e') => Some (H', Getfield e' fname)
    | _ => None
    end
  | Putfield (Value v1) fname e2 => match step_comp H e2 with
    | Some (H', e2') => Some (H', Putfield (Value v1) fname e2')
    | _ => None
    end
  | Putfield e1 fname e2 => match step_comp H e1 with
    | Some (H', e1') => Some (H', Putfield e1' fname e2)
    | _ => None
    end
  | _ => None
  end.
Solve All Obligations with sauto.