Library AndersenModel
Require Import List TheoryList.
Require Import Maps.
Require Import Pointer.
Set Implicit Arguments.
Definition allocation_site := nat.
Module AllocMap : MAP with Definition dom := allocation_site := NatMap.
Module AllocSet : SET with Definition dom := allocation_site := ListSet(NatEq).
Inductive abstract_instruction : Set :=
| AbsAllocate : var -> allocation_site -> abstract_instruction
| AbsCopy : var -> var -> abstract_instruction
| AbsRead : var -> var -> abstract_instruction
| AbsWrite : var -> var -> abstract_instruction.
Record abstract_state : Set := {
avars : VarMap.map AllocSet.set;
aheap : AllocMap.map AllocSet.set
}.
Definition abstract_exec (i : abstract_instruction) (s : abstract_state)
: abstract_state :=
match i with
| AbsAllocate dst site =>
Build_abstract_state
(VarMap.upd (avars s) dst
(AllocSet.add (VarMap.sel (avars s) dst) site))
(aheap s)
| AbsCopy dst src =>
Build_abstract_state
(VarMap.upd (avars s) dst
(AllocSet.union (VarMap.sel (avars s) dst) (VarMap.sel (avars s) src)))
(aheap s)
| AbsRead dst src =>
Build_abstract_state
(VarMap.upd (avars s) dst
(fold_left (fun known site => AllocSet.union known (AllocMap.sel (aheap s) site))
(AllocSet.elems (VarMap.sel (avars s) src)) (VarMap.sel (avars s) dst)))
(aheap s)
| AbsWrite dst src =>
Build_abstract_state
(avars s)
(fold_left (fun known site => AllocMap.upd known site
(AllocSet.union (AllocMap.sel (aheap s) site) (VarMap.sel (avars s) src)))
(AllocSet.elems (VarMap.sel (avars s) dst)) (aheap s))
end.
Fixpoint abstractProgram' (next : allocation_site)
(program : list instruction) {struct program}
: list abstract_instruction :=
match program with
| nil => nil
| ins :: program' =>
match ins with
| Allocate dst => AbsAllocate dst next :: abstractProgram' (S next) program'
| Copy dst src => AbsCopy dst src :: abstractProgram' next program'
| Read dst src => AbsRead dst src :: abstractProgram' next program'
| Write dst src => AbsWrite dst src :: abstractProgram' next program'
| Goto _ => abstractProgram' next program'
end
end.
Definition abstractProgram := abstractProgram' 1.
Index
This page has been generated by coqdoc