90 lines
3.2 KiB
Plaintext
90 lines
3.2 KiB
Plaintext
/* Testing infrastructure */
|
|
|
|
sel interval: int * int -> [int]; // interval function: interval (m, n) provides the numbers m, ..., n-1
|
|
|
|
op valueMoreAbstractThan (a: AbsDom, b:AbsDom): bool :=
|
|
match (a, b) with
|
|
| (@T, _) => true
|
|
| (@V(x), @V(y)) => x = y
|
|
| _ => false;
|
|
|
|
// Checks whether there exists a position where the two stacks disagree
|
|
op stackInequalExists{!size: int}(sa: array<AbsDom>, sb: array<AbsDom>): bool :=
|
|
for (!i: int) in interval(0,!size): || ((select sa !i) != (select sb !i));
|
|
|
|
// Checks whether the stacks agree at all positions
|
|
op stackEqualForall{!size: int}(sa: array<AbsDom>, sb: array<AbsDom>): bool :=
|
|
for (!i: int) in interval(0,!size): && ((select sa !i) = (select sb !i));
|
|
|
|
// Checks that the first stack is more abstract than the second one at all positions
|
|
op stackMoreAbstractThanForall{!size: int}(sa: array<AbsDom>, sb: array<AbsDom>): bool :=
|
|
for (!i: int) in interval(0,!size): && (valueMoreAbstractThan(select sa !i, select sb !i));
|
|
|
|
// Update representation for AbsDom arrays. Used for easily checking against a sequence of probing points in memory or storage
|
|
datatype Update := @UP<int*AbsDom>;
|
|
datatype UpdateList := @UPLIST<int*array<Update>>;
|
|
|
|
const UPDATEDUMMY := @UP(0, @T);
|
|
const UPDATELISTDUMMY := @UPLIST(0, [UPDATEDUMMY]);
|
|
|
|
op addUpdate(updates: UpdateList, up: Update): UpdateList :=
|
|
match updates with
|
|
| @UPLIST(size, ups) => @UPLIST(size + 1, store ups size up)
|
|
| _ => UPDATELISTDUMMY;
|
|
|
|
// Checks whether the array sa agrees with all updates of the Update array sb
|
|
op arrayEqual{!size:int} (sa: array<AbsDom>, sb: array<Update>): bool :=
|
|
for (!i:int) in interval(0, !size): &&
|
|
(match (select sb !i) with
|
|
| @UP(p, v) => (select sa p) = v
|
|
| _ => false)
|
|
;
|
|
|
|
// Checks whether the array sa is at all update points more concrete than the updates in sb
|
|
op arrayMoreAbstractThan{!size:int} (sa: array<AbsDom>, sb: array<Update>): bool :=
|
|
for (!i:int) in interval(0, !size): &&
|
|
(match (select sb !i) with
|
|
| @UP(p, v) => valueMoreAbstractThan(select sa p, v)
|
|
| _ => false)
|
|
;
|
|
|
|
// Checks whether array sa disagrees on one of the update points with the updates in sb
|
|
op arrayInequalExists{!size:int} (sa: array<AbsDom>, sb: array<Update>): bool :=
|
|
for (!i:int) in interval(0, !size): ||
|
|
(match (select sb !i) with
|
|
| @UP(p, v) => (select sa p) != v
|
|
| _ => false)
|
|
;
|
|
|
|
// Configurations that we use for testing. Consist of the stack size, the stack array, and update lists for memory and storage (to probe at the specified points)
|
|
datatype Config := @C<int*array<AbsDom>*UpdateList*UpdateList>;
|
|
|
|
op getStackSize(conf: Config): int :=
|
|
match conf with
|
|
| @C(size, sa, mem, stor) => size
|
|
| _ => 0;
|
|
|
|
op getStackArray(conf: Config): array<AbsDom> :=
|
|
match conf with
|
|
| @C(size, sa, mem, stor) => sa
|
|
| _ => [@T];
|
|
|
|
op getMemUpdateList(conf: Config): UpdateList :=
|
|
match conf with
|
|
| @C(size, sa, mem, stor) => mem
|
|
| _ => UPDATELISTDUMMY;
|
|
|
|
op getStorUpdateList(conf: Config): UpdateList :=
|
|
match conf with
|
|
| @C(size, sa, mem, stor) => stor
|
|
| _ => UPDATELISTDUMMY;
|
|
|
|
op getUpdateSize(ul: UpdateList): int :=
|
|
match ul with
|
|
| @UPLIST(s, ua) => s
|
|
| _ => 0;
|
|
|
|
op getUpdates(ul: UpdateList): array<Update> :=
|
|
match ul with
|
|
| @UPLIST(s, ua) => ua
|
|
| _ => [UPDATEDUMMY]; |