| Idealized assembly language |
Require Import Arith List.
Require Import LambdaTamer.ListUtil.
Require Import CTPC.AllocMonad.
Require Import CTPC.Trace.
Require Import CTPC.Dict.
Require Import CTPC.Alloc.
Require Import CTPC.Flat.
Require Import CTPC.Safety.
Set Implicit Arguments.
Term language (no types here!) |
Syntax |
Inductive genop : Set :=
| Slot : nat -> genop
| Const : nat -> genop
| New : list nat -> list nat -> genop
| Proj : nat -> nat -> genop.
Inductive instrs : Set :=
| Jump : nat -> instrs
| Assign : nat -> genop -> instrs -> instrs.
Record program : Set := {
blocks : list instrs;
body : instrs
}.
A definition of correct runtime systems |
Definition store := nat -> nat.
Section AllS2.
Variables A B : Set.
Variable f : A -> B -> Prop.
Fixpoint AllS2 (ls1 : list A) (ls2 : list B) {struct ls1} : Prop :=
match ls1, ls2 with
| nil, nil => True
| x1 :: ls1, x2 :: ls2 => f x1 x2 /\ AllS2 ls1 ls2
| _, _ => False
end.
End AllS2.
Section valComp.
Variable ptrComp : nat -> nat.
Definition valComp (a : adom) : nat :=
match a with
| (Untraced, v) => v
| (Traced, v) => ptrComp v
end.
End valComp.
Record runtime : Type := {
doNew : store -> list nat -> list nat -> store * list nat * nat;
doRead : store -> nat -> nat -> nat;
heapComp : mem adom -> store;
ptrComp : mem adom -> nat -> nat;
readUntraced : forall m1 n1 fds,
nth_error m1 n1 = Some fds
-> forall n2 v, nth_error fds n2 = Some (Untraced, v)
-> doRead (heapComp m1) (ptrComp m1 n1) n2 = v;
readTraced : forall m1 n1 fds,
nth_error m1 n1 = Some fds
-> forall n2 ptr, nth_error fds n2 = Some (Traced, ptr)
-> doRead (heapComp m1) (ptrComp m1 n1) n2 = ptrComp m1 ptr
/\ (forall fnums, validPath m1 ptr fnums);
newOk : forall m1 roots1 fds,
let m1' := m1 ++ fds :: nil in
exists m2, exists roots2, exists a,
doNew (heapComp m1) (map (ptrComp m1) roots1) (map (valComp (ptrComp m1)) fds)
= (heapComp m2, map (ptrComp m2) roots2, ptrComp m2 a)
/\ AllS2 (isomorphic_pointers m1' m2) roots1 roots2
/\ isomorphic_pointers m1' m2 (length m1) a
}.
Denotational semantics |
Section withRuntime.
Variable rt : runtime.
Definition argsDenote (e : list nat) (sls : slots) :=
map (NatDict.sel sls) e.
Fixpoint rootsIn (sls : slots) (roots vals : list nat) {struct roots} : slots :=
match roots, vals with
| root :: roots', val :: vals' =>
NatDict.upd (rootsIn sls roots' vals') root val
| _, _ => sls
end.
Definition genopDenote (op : genop) (sls : slots) (m : store) : store * slots * nat :=
match op with
| Slot sl => (m, sls, NatDict.sel sls sl)
| Const n => (m, sls, n)
| New roots fs =>
match doNew rt m (argsDenote roots sls) (argsDenote fs sls) with
| (m', roots', a) => (m', rootsIn sls roots roots', a)
end
| Proj a n => (m, sls, doRead rt m (NatDict.sel sls a) n)
end.
Fixpoint instrsDenote (lin : instrs) (sls : slots) (m : store) {struct lin}
: store * nat * slots :=
match lin with
| Jump sl => (m, NatDict.sel sls sl, sls)
| Assign sl op lin' =>
match genopDenote op sls m with
| (m', sls', v) => instrsDenote lin' (NatDict.upd sls' sl v) m'
end
end.
Co-inductive trace semantics |
Section Traces.
Variable pr : program.
CoFixpoint makeTrace (m : store) (pc : nat) (sls : slots) : trace nat :=
match pc with
| O => Output (NatDict.sel sls 1)
| S pc =>
match nth_error (blocks pr) pc with
| None => Crash
| Some ins =>
match instrsDenote ins sls m with
| (m', pc', sls') => Call (makeTrace m' pc' sls')
end
end
end.
Definition programDenote (sls : slots) (m : store) :=
match instrsDenote (body pr) sls m with
| (m', pc, sls') => makeTrace m' pc sls'
end.
End Traces.
End withRuntime.