Library Pointer
Require Import Arith List.
Require Import Machine Maps.
Set Implicit Arguments.
Definition var := nat.
Inductive instruction : Set :=
| Allocate : var -> instruction
| Copy : var -> var -> instruction
| Read : var -> var -> instruction
| Write : var -> var -> instruction
| Goto : nat -> instruction.
Module NatEq <: EQ.
Definition dom := nat.
Definition dom_eq_dec := eq_nat_dec.
End NatEq.
Module NatMap := FuncMap(NatEq).
Module VarMap : MAP with Definition dom := var := NatMap.
Record state : Set := {
pc : nat;
vars : VarMap.map nat;
heap : NatMap.map nat;
limit : nat
}.
Definition initState :=
Build_state
0
(VarMap.init 0)
(NatMap.init 0)
0.
Definition exec (i : instruction) (s : state) : state :=
match i with
| Allocate dst =>
Build_state
(S (pc s))
(VarMap.upd (vars s) dst (S (limit s)))
(heap s)
(S (limit s))
| Copy dst src =>
Build_state
(S (pc s))
(VarMap.upd (vars s) dst (VarMap.sel (vars s) src))
(heap s)
(limit s)
| Read dst src =>
match NatMap.sel (heap s) (VarMap.sel (vars s) src) with
| O => s
| addr =>
Build_state
(S (pc s))
(VarMap.upd (vars s) dst addr)
(heap s)
(limit s)
end
| Write dst src =>
match VarMap.sel (vars s) dst with
| O => s
| addr =>
Build_state
(S (pc s))
(vars s)
(NatMap.upd (heap s) addr (VarMap.sel (vars s) src))
(limit s)
end
| Goto n =>
Build_state
n
(vars s)
(heap s)
(limit s)
end.
Section mustNotAlias.
Variable program : list instruction.
Variables v1 v2 : var.
Definition mustNotAlias :=
forall s, reachable program pc exec initState s
-> VarMap.sel (vars s) v1 = VarMap.sel (vars s) v2
-> VarMap.sel (vars s) v1 = 0.
Inductive mustNotAlias_answer : Set :=
| Unknown : mustNotAlias_answer
| NotAliased : mustNotAlias -> mustNotAlias_answer.
End mustNotAlias.
Definition mustNotAlias_procedure := forall program v1 v2,
mustNotAlias_answer program v1 v2.
Index
This page has been generated by coqdoc