/* Tests for the local instructions of tinyEVM. To be run on local-contract.txt */

op pcToConfig(pc: int): Config := 
	match pc with
	| 0 => @C(	0, 
				[@V(0)], 
				UPDATELISTDUMMY,  
				UPDATELISTDUMMY)
	| 1 => @C(	1, 
				store [@V(0)] 0 @V(1), 
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 2 => @C(	2, 
				store (store [@V(0)] 0 @V(1)) 1 @V(~2), 
				UPDATELISTDUMMY,
				UPDATELISTDUMMY)
	| 3 => @C(	1, 
				store [@V(0)] 0 @V(~1),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 4 => @C(	2, 
				store (store [@V(0)] 0 @V(~1)) 1 @V(1),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 5 => @C(	1, 
				store [@V(0)] 0 @V(0),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 6 => @C(	2, 
				store (store [@V(0)] 0 @V(0)) 1 @V(2),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 7 => @C(	1, 
				store [@V(0)] 0 @V(0),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 8 => @C(	2, 
				store (store [@V(0)] 0 @V(0)) 1 @V(~1),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 9 => @C(	1, 
				store [@V(0)] 0 @V(1),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 10 => @C(	2, 
				store (store [@V(0)] 0 @V(1)) 1 @V(336633572),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 11 => @C(	1, 
				store [@V(0)] 0 @V(1),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 12 => @C(	0, 
				[@V(0)],
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 13 => @C(	1, 
				store [@V(0)] 0 @V(246435),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 14 => @C(	1, 
				[@V(0)],
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 15 => @C(	2, 
				store [@V(0)] 1 @V(2),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 16 => @C(	1, 
				store [@V(0)] 0 @V(2),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 17 => @C(	2, 
				store (store [@V(0)] 0 @V(2)) 1 @V(1),
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY)
	| 18 => @C(	0, 
				[@V(0)],
				addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
				UPDATELISTDUMMY)
	| 19 => @C(	1, 
				store [@V(0)] 0 @V(1),
				addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
				UPDATELISTDUMMY)
	| 20 => @C(	1, 
				store [@V(0)] 0 @V(2),
				addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
				UPDATELISTDUMMY)
	| 21 => @C(	2, 
				store (store [@V(0)] 0 @V(2)) 1 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
				UPDATELISTDUMMY)
	| 22 => @C(	2, 
				store (store [@V(0)] 0 @V(2)) 1 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
				UPDATELISTDUMMY)
	| 23 => @C(	0, 
				[@V(0)],
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				UPDATELISTDUMMY)
	| 24 => @C(	1, 
				store [@V(0)] 0 @V(~42),
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				UPDATELISTDUMMY)
	| 25 => @C(	1, 
				store [@V(0)] 0 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				UPDATELISTDUMMY)
	| 26 => @C(	1, 
				store [@V(0)] 0 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				UPDATELISTDUMMY)
	| 27 => @C(	0, 
				[@V(0)],
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				UPDATELISTDUMMY)
	| 28 => @C(	1, 
				store [@V(0)] 0 @V(~1337),
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				UPDATELISTDUMMY)
	| 29 => @C(	2, 
				store (store [@V(0)] 0 @V(~1337)) 1 @V(~67),
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				UPDATELISTDUMMY)
	| 30 => @C(	0, 
				[@V(0)],
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
	| 31 => @C(	1, 
				store [@V(0)] 0 @V(~67),
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
	| 32 => @C(	1, 
				store [@V(0)] 0 @V(~1337),
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
	| 33 => @C(	1, 
				store [@V(0)] 0 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
	| 34 => @C(	1, 
				store [@V(0)] 0 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
	| 35 => @C(	2, 
				store (store [@V(0)] 0 @T) 1 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
	| 36 => @C(	0, 
				[@V(0)],
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 37 => @C(	1, 
				store [@V(0)] 0 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 38 => @C(	2, 
				store (store [@V(0)] 0 @T) 1 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 40 => @C(	2, 
				store (store [@V(0)] 0 @T) 1 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 41 => @C(	1, 
				store [@V(0)] 0 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 42 => @C(	1, 
				store [@V(0)] 0 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 43 => @C(	1, 
				store [@V(0)] 0 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 44 => @C(	0, 
				[@V(0)],
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 45 => @C(	0, 
				[@V(0)],
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 46 => @C(	1, 
				store [@V(0)] 0 @T,
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 47 => @C(	0, 
				[@V(0)],
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 48 => @C(	0, 
				[@V(0)],
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 49 => @C(	1, 
				store [@V(0)] 0 @V(1),
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| 51 => @C(	0, 
				[@V(0)],
				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
	| _ => @C(	0, 
				[@V(0)], 
				UPDATELISTDUMMY, 
				UPDATELISTDUMMY);

const INTERVALS := 3; 

test pcToStackTest expect SAT [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
	ExState{1}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
	(@V(1)) = (select (getStackArray(pcToConfig(1))) 0);


test soundnessTest expect SAT 
	for (!i: int) in interval(0, INTERVALS), (!pc: int) in interval((!i = 0)? (0): ((!i = 1)?(40):(51)), (!i = 0)? (39): ((!i = 1)?(50):(52))) // ugly way to only invoke the rule on certain intervals
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(getStackSize(pcToConfig(!pc)), ?sa, ?mem, @T, ?stor, false),
		stackMoreAbstractThanForall{getStackSize(pcToConfig(!pc))}(?sa, getStackArray(pcToConfig(!pc))),
		arrayMoreAbstractThan{getUpdateSize(getMemUpdateList(pcToConfig(!pc)))}(?mem, getUpdates(getMemUpdateList(pcToConfig(!pc)))),
		arrayMoreAbstractThan{getUpdateSize(getStorUpdateList(pcToConfig(!pc)))}(?stor, getUpdates(getStorUpdateList(pcToConfig(!pc))))
		;

test precisionPossibleTest expect SAT
 	for (!i: int) in interval(0, INTERVALS), (!pc: int) in interval((!i = 0)? (0): ((!i = 1)?(40):(51)), (!i = 0)? (39): ((!i = 1)?(50):(52)))
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(getStackSize(pcToConfig(!pc)), ?sa, ?mem, @T, ?stor, false),
		stackEqualForall{getStackSize(pcToConfig(!pc))}(?sa, getStackArray(pcToConfig(!pc))),
		arrayEqual{getUpdateSize(getMemUpdateList(pcToConfig(!pc)))}(?mem, getUpdates(getMemUpdateList(pcToConfig(!pc)))),
		arrayEqual{getUpdateSize(getStorUpdateList(pcToConfig(!pc)))}(?stor, getUpdates(getStorUpdateList(pcToConfig(!pc))))
		;

test precisionUniqueTest expect UNSAT
	for (!i: int) in interval(0, INTERVALS), (!pc: int) in interval((!i = 0)? (0): ((!i = 1)?(40):(51)), (!i = 0)? (39): ((!i = 1)?(50):(52)))
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, false),
		(?size != getStackSize(pcToConfig(!pc))) 
		|| (stackInequalExists{getStackSize(pcToConfig(!pc))}(?sa, getStackArray(pcToConfig(!pc)))) 
		|| (arrayInequalExists{getUpdateSize(getMemUpdateList(pcToConfig(!pc)))}(?mem, getUpdates(getMemUpdateList(pcToConfig(!pc)))))
		|| (?in != @T) 
		|| (arrayInequalExists{getUpdateSize(getStorUpdateList(pcToConfig(!pc)))}(?stor, getUpdates(getStorUpdateList(pcToConfig(!pc)))))
		;


/* Additional Tests concerning reachability, halting, etc. */

// pcs 39 and 50 should be unreachable because they are over-jumped
test unreachable39Test expect UNSAT
		[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{39}(?size, ?sa, ?mem, ?in, ?stor, ?cl);

test unreachable50Test expect UNSAT
		[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
		ExState{50}(?size, ?sa, ?mem, ?in, ?stor, ?cl);

// Tests for correct halting
test haltSoundnessTest expect SAT
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?res: AbsDom]
	Halt(?stor, ?res, false),
	valueMoreAbstractThan(?res, @V(0)); 

test haltPrecisePossibleTest expect SAT
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?res: AbsDom]
	Halt(?stor, @V(0), false);

// the only possible return results are 0 and T (due to stop and RETURN)
test haltPreciionUniquenessTest expect UNSAT
	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?res: AbsDom]
	Halt(?stor, ?res, false),
	(?res != @V(0) && ?res != @T); 

// Reaching an exceptional state should be possible
test exceptionPossibleTest expect SAT
	Exc(false);

test noCallTest2 expect UNSAT
	Exc(true);


/*
query testQuery [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?res: AbsDom, ?p: AbsDom]
	ExState{13}(?size, ?sa, ?mem, ?in, ?stor, ?cl), ?size > 0, 
		?p = select ?sa (?size -1),
		?res = (isConcrete(?p))? (select ?mem (extractConcrete(?p))):(@T), 
		?res = @V(0); */