diff options
Diffstat (limited to 'Chalice/src/Prelude.scala')
| -rw-r--r-- | Chalice/src/Prelude.scala | 251 |
1 files changed, 251 insertions, 0 deletions
diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala new file mode 100644 index 00000000..876a5abe --- /dev/null +++ b/Chalice/src/Prelude.scala @@ -0,0 +1,251 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+object TranslatorPrelude {
+
+ val P =
+"""// Copyright (c) 2008, Microsoft
+type Field a;
+type HeapType = <a>[ref,Field a]a;
+type MaskType = <a>[ref,Field a][PermissionComponent]int;
+type ref;
+const null: ref;
+
+var Heap: HeapType;
+
+type PermissionComponent;
+const unique perm$R: PermissionComponent;
+const unique perm$N: PermissionComponent;
+const Permission$MinusInfinity: int;
+axiom Permission$MinusInfinity < -10000;
+const Permission$PlusInfinity: int;
+axiom 10000 < Permission$PlusInfinity;
+var Mask: MaskType where IsGoodMask(Mask);
+const Permission$Zero: [PermissionComponent]int;
+axiom Permission$Zero[perm$R] == 0 && Permission$Zero[perm$N] == 0;
+const Permission$Full: [PermissionComponent]int;
+axiom Permission$Full[perm$R] == 100 && Permission$Full[perm$N] == 0;
+const ZeroMask: MaskType;
+axiom (forall<T> o: ref, f: Field T, pc: PermissionComponent :: ZeroMask[o,f][pc] == 0);
+axiom IsGoodMask(ZeroMask);
+function {:expand false} CanRead<T>(m: MaskType, obj: ref, f: Field T) returns (bool)
+{
+ 0 < m[obj,f][perm$R] || 0 < m[obj,f][perm$N]
+}
+function {:expand false} CanWrite<T>(m: MaskType, obj: ref, f: Field T) returns (bool)
+{
+ m[obj,f][perm$R] == 100 && m[obj,f][perm$N] == 0
+}
+function {:expand true} IsGoodMask(m: MaskType) returns (bool)
+{
+ (forall<T> o: ref, f: Field T ::
+ 0 <= m[o,f][perm$R] &&
+ (NonPredicateField(f) ==>
+ (m[o,f][perm$R]<=100 &&
+ (0 < m[o,f][perm$N] ==> m[o,f][perm$R] < 100))) &&
+ (m[o,f][perm$N] < 0 ==> 0 < m[o,f][perm$R]))
+}
+
+function IsGoodState<T>(T) returns (bool);
+function combine<T,U>(T, U) returns (T);
+const nostate: HeapType;
+
+axiom (forall<T,U> a: T, b: U :: {IsGoodState(combine(a, b))} IsGoodState(combine(a, b)) <==> IsGoodState(a) && IsGoodState(b));
+axiom IsGoodState(nostate);
+
+type ModuleName;
+const CurrentModule: ModuleName;
+type TypeName;
+function dtype(ref) returns (TypeName);
+const CanAssumeFunctionDefs: bool;
+
+type Mu;
+const unique mu: Field Mu;
+axiom NonPredicateField(mu);
+function MuBelow(Mu, Mu) returns (bool); // strict partial order
+axiom (forall m: Mu, n: Mu ::
+ { MuBelow(m,n), MuBelow(n,m) }
+ !(MuBelow(m,n) && MuBelow(n,m)));
+axiom (forall m: Mu, n: Mu, o: Mu ::
+ { MuBelow(m,n), MuBelow(n,o) }
+ MuBelow(m,n) && MuBelow(n,o) ==> MuBelow(m,o));
+const $LockBottom: Mu;
+axiom (forall m, n: Mu :: MuBelow(m, n) ==> n != $LockBottom);
+
+const unique held: Field int;
+function Acquire$Heap(int) returns (HeapType);
+function Acquire$Mask(int) returns (MaskType);
+axiom NonPredicateField(held);
+
+function LastSeen$Heap(Mu, int) returns (HeapType);
+function LastSeen$Mask(Mu, int) returns (MaskType);
+
+const unique rdheld: Field bool;
+axiom NonPredicateField(rdheld);
+function wf(h: HeapType, m: MaskType) returns (bool);
+
+function IsGoodInhaleState(ih: HeapType, h: HeapType,
+ m: MaskType) returns (bool)
+{
+ (forall<T> o: ref, f: Field T :: { ih[o, f] } CanRead(m, o, f) ==> ih[o, f] == h[o, f]) &&
+ (forall o: ref :: { ih[o, held] } (0<ih[o, held]) == (0<h[o, held])) &&
+ (forall o: ref :: { ih[o, rdheld] } ih[o, rdheld] == h[o, rdheld]) &&
+ (forall o: ref :: { h[o, held] } (0<h[o, held]) ==> ih[o, mu] == h[o, mu])
+}
+
+function ite<T>(bool, T, T) returns (T);
+axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} con ==> ite(con, a, b) == a);
+axiom (forall<T> con: bool, a: T, b: T :: {ite(con, a, b)} ! con ==> ite(con, a, b) == b);
+
+type Seq T;
+
+function Seq#Length<T>(Seq T) returns (int);
+axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));
+
+function Seq#Empty<T>() returns (Seq T);
+axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);
+axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());
+
+function Seq#Singleton<T>(T) returns (Seq T);
+axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);
+
+function Seq#Build<T>(s: Seq T, index: int, val: T, newLength: int) returns (Seq T);
+axiom (forall<T> s: Seq T, i: int, v: T, len: int :: { Seq#Length(Seq#Build(s,i,v,len)) }
+ Seq#Length(Seq#Build(s,i,v,len)) == len);
+
+function Seq#Append<T>(Seq T, Seq T) returns (Seq T);
+axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }
+ Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1));
+
+function Seq#Index<T>(Seq T, int) returns (T);
+axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t);
+axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) }
+ (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) &&
+ (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0))));
+axiom (forall<T> s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Build(s,i,v,len),n) }
+ (i == n ==> Seq#Index(Seq#Build(s,i,v,len),n) == v) &&
+ (i != n ==> Seq#Index(Seq#Build(s,i,v,len),n) == Seq#Index(s,n)));
+
+function Seq#Contains<T>(Seq T, T) returns (bool);
+axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
+ Seq#Contains(s,x) <==>
+ (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));
+axiom (forall x: ref ::
+ { Seq#Contains(Seq#Empty(), x) }
+ !Seq#Contains(Seq#Empty(), x));
+axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::
+ { Seq#Contains(Seq#Append(s0, s1), x) }
+ Seq#Contains(Seq#Append(s0, s1), x) <==>
+ Seq#Contains(s0, x) || Seq#Contains(s1, x));
+axiom (forall<T> s: Seq T, i: int, v: T, len: int, x: T ::
+ { Seq#Contains(Seq#Build(s, i, v, len), x) }
+ Seq#Contains(Seq#Build(s, i, v, len), x) <==>
+ x == v || Seq#Contains(s, x));
+axiom (forall<T> s: Seq T, n: int, x: T ::
+ { Seq#Contains(Seq#Take(s, n), x) }
+ Seq#Contains(Seq#Take(s, n), x) <==>
+ (exists i: int :: { Seq#Index(s, i) }
+ 0 <= i && i < n && n <= Seq#Length(s) && Seq#Index(s, i) == x));
+axiom (forall<T> s: Seq T, n: int, x: T ::
+ { Seq#Contains(Seq#Drop(s, n), x) }
+ Seq#Contains(Seq#Drop(s, n), x) <==>
+ (exists i: int :: { Seq#Index(s, i) }
+ 0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
+
+function Seq#Equal<T>(Seq T, Seq T) returns (bool);
+axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }
+ Seq#Equal(s0,s1) <==>
+ Seq#Length(s0) == Seq#Length(s1) &&
+ (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
+ 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
+axiom(forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) } // extensionality axiom for sequences
+ Seq#Equal(a,b) ==> a == b);
+
+function Seq#SameUntil<T>(Seq T, Seq T, int) returns (bool);
+axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) }
+ Seq#SameUntil(s0,s1,n) <==>
+ (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
+ 0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
+
+function Seq#Take<T>(Seq T, howMany: int) returns (Seq T);
+axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }
+ 0 <= n ==>
+ (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&
+ (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));
+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) }
+ 0 <= j && j < n && j < Seq#Length(s) ==>
+ Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));
+
+function Seq#Drop<T>(Seq T, howMany: int) returns (Seq T);
+axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }
+ 0 <= n ==>
+ (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&
+ (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));
+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) }
+ 0 <= n && 0 <= j && j < Seq#Length(s)-n ==>
+ Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));
+
+function Seq#Range(min: int, max: int) returns (Seq int);
+
+axiom (forall min: int, max: int :: { Seq#Length(Seq#Range(min, max)) } (min < max ==> Seq#Length(Seq#Range(min, max)) == max-min) && (max <= min ==> Seq#Length(Seq#Range(min, max)) == 0));
+axiom (forall min: int, max: int, j: int :: { Seq#Index(Seq#Range(min, max), j) } 0<=j && j<max-min ==> Seq#Index(Seq#Range(min, max), j) == min + j);
+
+axiom (forall h: HeapType, m: MaskType, o: ref, q: ref :: {wf(h, m), h[o, mu], h[q, mu]} wf(h, m) && o!=q && (0 < h[o, held]) && (0 < h[q, held]) ==> h[o, mu] != h[q, mu]);
+
+function DecPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$R]}
+ DecPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] - howMuch, m[q, g][perm$R])
+);
+
+function DecEpsilons<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {DecPerm(m, o, f, howMuch)[q, g][perm$N]}
+ DecEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] - howMuch, m[q, g][perm$N])
+);
+
+function IncPerm<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$R]}
+ IncPerm(m, o, f, howMuch)[q, g][perm$R] == ite(o==q && f ==g, m[q, g][perm$R] + howMuch, m[q, g][perm$R])
+);
+
+function IncEpsilons<T>(m: MaskType, o: ref, f: Field T, howMuch: int) returns (MaskType);
+
+axiom (forall<T,U> m: MaskType, o: ref, f: Field T, howMuch: int, q: ref, g: Field U :: {IncPerm(m, o, f, howMuch)[q, g][perm$N]}
+ IncEpsilons(m, o, f, howMuch)[q, g][perm$N] == ite(o==q && f ==g, m[q, g][perm$N] + howMuch, m[q, g][perm$N])
+);
+
+function Havocing<T,U>(h: HeapType, o: ref, f: Field T, newValue: U) returns (HeapType);
+
+axiom (forall<T,U> h: HeapType, o: ref, f: Field T, newValue: U, q: ref, g: Field U :: {Havocing(h, o, f, newValue)[q, g]}
+ Havocing(h, o, f, newValue)[q, g] == ite(o==q && f ==g, newValue, h[q, g])
+);
+
+const unique joinable: Field int;
+axiom NonPredicateField(joinable);
+const unique token#t: TypeName;
+
+function Call$Heap(int) returns (HeapType);
+function Call$Mask(int) returns (MaskType);
+function Call$Args(int) returns (ArgSeq);
+type ArgSeq = <T>[int]T;
+
+function EmptyMask(m: MaskType) returns (bool);
+axiom (forall m: MaskType :: {EmptyMask(m)} EmptyMask(m) <==> (forall<T> o: ref, f: Field T :: NonPredicateField(f) ==> m[o, f][perm$R]<=0 && m[o, f][perm$N]<=0));
+
+function NonPredicateField<T>(f: Field T) returns (bool);
+function PredicateField<T>(f: Field T) returns (bool);
+axiom (forall<T> f: Field T :: NonPredicateField(f) ==> ! PredicateField(f));
+axiom (forall<T> f: Field T :: PredicateField(f) ==> ! NonPredicateField(f));
+
+function submask(m1: MaskType, m2: MaskType) returns (bool);
+
+axiom (forall m1: MaskType, m2: MaskType :: {submask(m1, m2)}
+ submask(m1, m2) <==> (forall<T> o: ref, f: Field T :: (m1[o, f][perm$R] < m2[o, f][perm$R]) || (m1[o, f][perm$R] == m2[o, f][perm$R] && m1[o, f][perm$N] <= m2[o, f][perm$N]))
+);
+
+"""
+}
|