Library RuntimeStructuresImpl

An implementation of RUNTIME_STRUCTURES based on FMaps. @author Patryk Czarnik

Require Import List.
Require Import Common.
Require Import ValuesNTypes.
Require Import ProgramStructures.
Require Import RuntimeStructures.
Require Import Heap.

Implementation of PROGRAM_STRUCTURES

This functor provides an implementation of PROGRAM_STRUCTURES signature using FMaps as variable arrays.
Other structures have been already defined in the signature as lists or records.
See signature for documentation of module fields.
Module RuntimeStructuresImpl
  (_Heap: HEAP with Module M_ProgramStructures := _ProgramStructures)

Included modules

Open Scope type_scope.

Module M_Heap := _Heap.
Import M_Heap.M_ProgramStructures.M_ValuesAndTypes.
Import M_Heap.M_ProgramStructures.
Import M_Heap.

Local variables array

Definition TVarsGeneric: SetType := M_VarMap.t.
Section GenericVarsDefinition.
  Variable t: Set.
Definition varsEmpty := @M_VarMap.empty t.
Definition varsGet := @M_VarMap.find t.
Definition varsSet := @M_VarMap.add t.
Definition varsEquiv (vars1 vars2: TVarsGeneric t): Prop :=
   var, varsGet var vars1 = varsGet var vars2.

Section VarsProperties.
Variable vars: TVarsGeneric t.
Variable x y: TVar.
Variable v: t.

Lemma PvarsEmptyGet: varsGet x varsEmpty = None.
  case_eq (varsGet x varsEmpty); intros.
  apply M_VarMap.find_2 in H.
  apply M_VarMap.empty_1 in H.

Lemma PvarsSetGet:
  varsGet x (varsSet x v vars) = Some v.
  apply M_VarMap.find_1.
  apply M_VarMap.add_1.

Lemma noneNotMapsTo:
   vars' y,
  varsGet y vars' = None
   w, ¬ M_VarMap.MapsTo y w vars'.
  unfold not.
  apply M_VarMap.find_1 in H0.
  unfold varsGet in H.
  rewrite H in H0.
  discriminate H0.

Lemma notMapsToNone:
   vars' y,
  ( w, ¬ M_VarMap.MapsTo y w vars') →
  varsGet y vars' = None.
  unfold not.
  case_eq (varsGet y0 vars'); intros.
  apply M_VarMap.find_2 in H0.
  apply H in H0.

Lemma PvarsSetGetOther:
  x y
  varsGet y vars = varsGet y (varsSet x v vars).
  case_eq (varsGet y (varsSet x v vars)); intros.
  apply M_VarMap.find_1.
  apply M_VarMap.find_2 in H.
  apply M_VarMap.add_3 in H.

  eapply notMapsToNone; intros.
  eapply noneNotMapsTo in H.
  unfold not; intros.
  apply H; clear H.
  unfold varsSet.
  eapply M_VarMap.add_2.
  apply H0.

Axiom PvarsEqEquiv:
  varsEquiv vars vars.
Axiom PvarsSetSameEquiv:
  varsGet x vars = Some v
  varsEquiv (varsSet x v vars) vars.
End VarsProperties.
  End GenericVarsDefinition.
  Arguments varsEmpty [t].
  Arguments varsGet [t] _ _.
  Arguments varsSet [t] _ _ _.
  Arguments PvarsEmptyGet [t] _.
  Arguments PvarsSetGet [t] _ _ _.
  Arguments PvarsSetGetOther [t] _ _ _ _ _.

Section GenericStackDefinition.
  Variable t: Set.
  Definition TLocalStackGeneric: Set := list t.
End GenericStackDefinition.

Concretisation of generic structures introduced above

Projections between actual and "shadow" structures

Frame (corresponding to method call)

Threads and whole JVMs

  Definition TRichFrame :=
    TCurrentMethod × TFrame.

  Definition TEvalState := TLoc.

  Record TThread := threadMake {
    threadGetId: M_Heap.TThreadId;
    threadGetEvalState: TEvalState;
    threadGetCallStack: list TRichFrame

  Record TJVM := jvmMake {
    jvmGetHeap: M_Heap.THeap;
    jvmGetThreads: list TThread

  Inductive TResultOrException (A: Type): Type :=
  | Result (result: A)
  | Exception (cn: TClassName).
End RuntimeStructuresImpl.