Version of the main interfaces in VPL hierarchy
where the backend is trusted to be pure !
Require Export NumC.
Require Export ProgVar.
Require Import Itv.
Require Import DomainInterfaces.
Require Export OptionMonad.
Require Export Debugging.
Require Import Itv.
Global Transparent pure bind imp mayReturn impeq.
Hint Unfold mayReturn impeq.
Ltac VPLsimplify :=
xsimplify ltac:(
eauto with vpl).
Module Type BasicDomain (
N:
NumSig).
Parameter t:
Type.
Parameter gamma:
t ->
Mem.t N.t ->
Prop.
Declare Instance gamma_ext:
Proper (
Logic.eq ==>
pointwise_relation PVar.t Logic.eq ==>
iff)
gamma.
Parameter isIncl:
t ->
t ->
bool.
Parameter isIncl_correct:
forall a1 a2,
If isIncl a1 a2 THEN forall m,
gamma a1 m ->
gamma a2 m.
Parameter top:
t.
Parameter top_correct:
forall m,
gamma top m.
Parameter join:
t ->
t ->
t.
Parameter join_correct1:
forall a1 a2 m,
gamma a1 m ->
gamma (
join a1 a2)
m.
Parameter join_correct2:
forall a1 a2 m,
gamma a2 m ->
gamma (
join a1 a2)
m.
Parameter widen:
t ->
t ->
t.
Parameter bottom:
t.
Parameter bottom_correct:
forall m, (
gamma bottom m)->
False.
Parameter isBottom :
t ->
bool.
Parameter isBottom_correct :
forall a,
If isBottom a THEN forall m,
gamma a m ->
False.
Parameter project:
t ->
PVar.t ->
t.
Parameter project_correct:
forall a x m v,
gamma a m ->
gamma (
project a x) (
Mem.assign x v m).
Hint Resolve isIncl_correct top_correct join_correct1 join_correct2 bottom_correct isBottom_correct project_correct:
vpl.
End BasicDomain.
Module Type HasSimplePrinting (
N:
NumSig) (
Import D:
BasicDomain N).
Parameter pr:
t ->
String.string.
End HasSimplePrinting.
Module Type HasRename (
N:
NumSig) (
Import D:
BasicDomain N).
Require Import Program.Basics.
rename x y a renames variable x by y in a.
WARNING: For the underlying "shadow" implementation in ML,
y must be a fresh variable in a
However, we do not need to make this precondition explicit
for correctness (thus, this is simpler to let it hidden).
Hence, this precondition is only dynamically verified by an "assert" in ML code.
Parameter rename:
PVar.t ->
PVar.t ->
t ->
t.
Parameter rename_correct:
forall x y a m,
gamma a (
Mem.assign x (
m y)
m) ->
gamma (
rename x y a)
m.
End HasRename.
Interval from Terms
Module Type TermSig(
N:
NumSig).
Parameter t:
Type.
Parameter eval:
t ->
Mem.t N.t ->
N.t.
End TermSig.
Module Type HasGetItv (
N:
NumSig) (
Import T:
TermSig N) (
Import I:
ItvSig N) (
Import D:
BasicDomain N).
Parameter get_itv:
T.t ->
t ->
I.t.
Parameter get_itv_correct:
forall te m a,
gamma a m ->
I.sat (
get_itv te a) (
T.eval te m).
Hint Resolve get_itv_correct:
vpl.
End HasGetItv.
Assume/Assert of conditions
Module Type CondSig(
N:
NumSig).
Parameter t:
Type.
Parameter sat:
t ->
Mem.t N.t ->
Prop.
End CondSig.
Module Type HasAssume (
N:
NumSig) (
Cond:
CondSig N) (
D:
BasicDomain N).
Import Cond.
Import D.
Parameter assume:
Cond.t ->
t ->
t.
Parameter assume_correct:
forall c a m,
sat c m ->
gamma a m ->
gamma (
assume c a)
m.
Hint Resolve assume_correct:
vpl.
End HasAssume.
Module Type HasAssert (
N:
NumSig) (
Cond:
CondSig N) (
D:
BasicDomain N).
Import Cond.
Import D.
Parameter assert:
Cond.t ->
t ->
bool.
Parameter assert_correct:
forall c a,
If assert c a THEN forall m,
gamma a m ->
sat c m.
Hint Resolve assert_correct:
vpl.
End HasAssert.
Module Type HasConcreteConditions (
N:
NumSig) (
Cond:
CondSig N) (
D:
BasicDomain N)
:=
HasAssume N Cond D <+
HasAssert N Cond D.
Module Type WeakAbstractDomain (
N:
NumSig) (
Cond:
CondSig N)
:=
BasicDomain N <+
HasAssume N Cond.
Module Type AbstractDomain (
N:
NumSig) (
Cond:
CondSig N)
:=
WeakAbstractDomain N Cond <+
HasAssert N Cond.
Module Type XCondSig(
N:
NumSig).
Declare Module Term:
TermSig N.
Include CondSig N.
two state semantics:
xsat c old new means that "c" is a relation between "old" state and "new" state.
Parameter xsat:
t ->
Mem.t N.t ->
Mem.t N.t ->
Prop.
Parameter xsat_sat:
forall c m,
xsat c m m =
sat c m.
End XCondSig.
Module Type HasAssign (
N:
NumSig) (
Cond:
XCondSig N) (
D:
BasicDomain N).
Import Cond.Term.
Import Cond.
Import D.
Parameter assign:
PVar.t ->
Term.t ->
t ->
t.
Parameter assign_correct:
forall x te a m,
gamma a m ->
gamma (
assign x te a) (
Mem.assign x (
eval te m)
m).
Parameter guassign:
PVar.t ->
Cond.t ->
t ->
t.
Parameter guassign_correct:
forall x c a m v,
(
xsat c m (
Mem.assign x v m)) ->
gamma a m ->
gamma (
guassign x c a) (
Mem.assign x v m).
End HasAssign.
Module Type FullAbstractDomain (
N:
NumSig) (
Cond:
XCondSig N) :=
AbstractDomain N Cond <+
HasAssign N Cond.
Module Type FullItvAbstractDomain (
N:
NumSig) (
Cond:
XCondSig N) (
I:
ItvSig N) :=
FullAbstractDomain N Cond <+
HasGetItv N Cond.Term I.
BoundVar
Module Type HasBoundVar (
N:
NumSig) (
Import D:
BasicDomain N).
Parameter boundVar:
t ->
PVar.t.
Definition mayDependOn a x :=
PVar.Le x (
boundVar a).
Parameter gamma_mdo:
mdoExt mayDependOn gamma iff.
End HasBoundVar.
Module Type FullBoundVarDomain (
N:
NumSig) (
Cond:
XCondSig N) :=
FullAbstractDomain N Cond <+
HasBoundVar N.