Skip to content

Commit 951404f

Browse files
lichyelichye
committed
modify test benchmark
1 parent 25d1348 commit 951404f

File tree

12 files changed

+249
-209
lines changed

12 files changed

+249
-209
lines changed

‎src/main/scala/uclid/ConcreteSimulator.scala‎

Lines changed: 18 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -620,7 +620,6 @@ object ConcreteSimulator {
620620
//Debuging Functions
621621
def printVar (vars: List[(Expr, String)]) : Unit = {
622622
if (vars.isEmpty) {
623-
println("\tVarmap:")
624623
for ((key,value) <- varMap){
625624
println(s"${key.toString}: ${value.toString}")
626625
}
@@ -661,7 +660,7 @@ object ConcreteSimulator {
661660
if(idArg.toString == "\"Default\""){
662661
runtimeMod = Default;
663662
}
664-
if(idArg.toString == "\"Random\""){
663+
if(idArg.toString == "\"Fuzzing\""){
665664
runtimeMod = Fuzzing;
666665
}
667666
if(idArg.toString == "\"Json\""){
@@ -1026,8 +1025,11 @@ object ConcreteSimulator {
10261025
}
10271026
}
10281027
case ConcreteUndef() => {
1029-
undetCount = undetCount + 1;
1030-
ConcreteUndef()
1028+
runtimeMod match{
1029+
case Fuzzing => ConcreteInt(random.nextInt())
1030+
case Default => ConcreteInt(0)
1031+
case _ => throw new Error("Hit undefine value of "+operands.tail.head.toString)
1032+
}
10311033
}
10321034
case _ => throw new NotImplementedError("add integer with undefine value of "+ expr.toString)
10331035
}
@@ -1064,8 +1066,11 @@ object ConcreteSimulator {
10641066
}
10651067
}
10661068
case ConcreteUndef() => {
1067-
undetCount = undetCount + 1;
1068-
ConcreteUndef()
1069+
runtimeMod match{
1070+
case Fuzzing => ConcreteBV(random.nextInt(pow(2,length).toInt),length)
1071+
case Default => ConcreteBV(0,length)
1072+
case _ => throw new Error("Hit undefine value of "+operands.tail.head.toString)
1073+
}
10691074
}
10701075
case _ => {
10711076
throw new NotImplementedError("Operand_1 is "+operands.tail.head.toString)
@@ -1082,8 +1087,11 @@ object ConcreteSimulator {
10821087
}
10831088
}
10841089
case ConcreteUndef() => {
1085-
undetCount = undetCount + 1;
1086-
ConcreteUndef()
1090+
runtimeMod match {
1091+
case Fuzzing => ConcreteEnum(ids,random.nextInt(ids.size))
1092+
case Default => ConcreteEnum(ids,0)
1093+
case _ => throw new Error("Hit undefine value of "+operands.tail.head.toString)
1094+
}
10871095
}
10881096
case _ => {
10891097
throw new NotImplementedError("Operand_1 is "+operands.tail.head.toString)
@@ -1139,11 +1147,11 @@ object ConcreteSimulator {
11391147
}
11401148
}
11411149
case _ => {
1142-
throw new NotImplementedError(s"Expression evaluation for ${expr}")
1150+
ConcreteUndef()
11431151
}
11441152
}
11451153
}
1146-
case _ => throw new NotImplementedError(s"Expression evaluation for ${expr}")
1154+
case _ => ConcreteUndef()
11471155
}}
11481156

11491157
def checkAssumes(assumes: List[AxiomDecl],context:ConcreteContext,iter:Int, module: Module){

‎src/main/scala/uclid/UclidMain.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,7 @@ object UclidMain {
114114
(exec, c) => c.copy(synthesizer = exec.split(" ").toList)
115115
}.text("Command line to invoke SyGuS synthesizer.")
116116

117-
opt[String]('c', "simulate").valueName("<Cmd>").action{
117+
opt[Unit]('c', "simulate").action{
118118
(exec, c) => c.copy(simulate = true)
119119
}.text("Perform concrete execution.")
120120

‎src/test/scala/ConcreteSpec.scala‎

Lines changed: 18 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,16 @@ object ConcreteSpec {
5858
assert (results.count((e) => e.result.isUndefined) == 0)
5959
outputString
6060
}
61+
def expectedError(filename: String, nFail: Int): Unit = {
62+
try {
63+
expectedFails(filename, nFail)
64+
} catch {
65+
case e: Error =>
66+
println(s"Test passed: caught expected Error - ${e.getMessage}")
67+
case _: Throwable =>
68+
throw new AssertionError("Expected an Error, but a different exception was thrown.")
69+
}
70+
}
6171
}
6272
class ConcreteSpec extends AnyFlatSpec {
6373
"concrete-0.ucl" should "fail one assertion." in {
@@ -66,31 +76,31 @@ class ConcreteSpec extends AnyFlatSpec {
6676
"concrete-1.ucl" should "pass." in {
6777
ConcreteSpec.expectedFails("./test/concrete/concrete-1.ucl", 0)
6878
}
69-
"concrete-2.ucl" should "pass." in {
70-
ConcreteSpec.expectedFails("./test/concrete/concrete-2.ucl", 0)
79+
"concrete-2.ucl" should "catch runtime error" in {
80+
ConcreteSpec.expectedError("./test/concrete/concrete-2.ucl", 0)
7181
}
7282
"concrete-3.ucl" should "fail one assertion." in {
7383
ConcreteSpec.expectedFails("./test/concrete/concrete-3.ucl", 1)
7484
}
75-
"concrete-4.ucl" should "pass." in {
76-
ConcreteSpec.expectedFails("./test/concrete/concrete-4.ucl", 0)
85+
"concrete-4.ucl" should "fail one assertion." in {
86+
ConcreteSpec.expectedFails("./test/concrete/concrete-4.ucl", 1)
7787
}
7888
"concrete-5.ucl" should "pass." in {
7989
ConcreteSpec.expectedFails("./test/concrete/concrete-5.ucl", 0)
8090
}
8191
"concrete-6.ucl" should "fail one assertion." in {
8292
ConcreteSpec.expectedFails("./test/concrete/concrete-6.ucl", 1)
8393
}
84-
"concrete-7.ucl" should "pass." in {
85-
ConcreteSpec.expectedFails("./test/concrete/concrete-7.ucl", 0)
94+
"concrete-7.ucl" should "fail two assertion." in {
95+
ConcreteSpec.expectedFails("./test/concrete/concrete-7.ucl", 2)
8696
}
8797
"concrete-8.ucl" should "pass." in {
8898
ConcreteSpec.expectedFails("./test/concrete/concrete-8.ucl", 1)
8999
}
90100
"concrete-9.ucl" should "fail one assertion." in {
91101
ConcreteSpec.expectedFails("./test/concrete/concrete-9.ucl", 1)
92102
}
93-
"concrete-10.ucl" should "fail one assertion." in {
94-
ConcreteSpec.expectedFails("./test/concrete/concrete-10.ucl", 1)
103+
"concrete-10.ucl" should "pass." in {
104+
ConcreteSpec.expectedFails("./test/concrete/concrete-10.ucl", 0)
95105
}
96106
}

‎test/concrete/concrete-10.ucl‎

Lines changed: 18 additions & 116 deletions
Original file line numberDiff line numberDiff line change
@@ -1,121 +1,23 @@
1-
module common {
2-
type op_t = enum {push, pop, nop};
3-
4-
const c0 : [integer]integer;
5-
}
6-
7-
8-
module queue
9-
{
10-
type op_t = common.op_t;
11-
12-
var contents : [integer]integer;
13-
var head, tail: integer;
14-
var inited : boolean;
15-
16-
output first: integer;
17-
18-
input op : op_t;
19-
input data : integer;
20-
21-
define is_empty() : boolean = (head == tail);
22-
define in_queue(v : integer) : boolean =
23-
(exists (i : integer) :: (i >= head && i < tail && contents[i] == v));
24-
25-
init {
26-
inited = false;
27-
head = 0;
28-
tail = 0;
29-
first = contents[head];
30-
}
31-
32-
procedure _push_q() returns (contentsP : [integer]integer, tailP : integer)
33-
{
34-
contentsP = contents;
35-
contentsP[tail] = data;
36-
tailP = tail + 1;
37-
}
38-
39-
procedure _pop_q() returns (headP : integer)
40-
{
41-
headP = head+1;
42-
}
43-
44-
next {
45-
inited' = true;
46-
first' = contents[head];
47-
case
48-
(op == push) : {
49-
call (contents', tail') = _push_q();
50-
}
51-
(op == pop) : {
52-
if (!is_empty()) {
53-
call(head') = _pop_q();
54-
}
55-
}
56-
(op == nop) : { } /* no change */
57-
esac;
58-
}
59-
60-
const pushed_data : integer;
61-
invariant[LTL] head_le_tail : G(head <= tail);
62-
invariant[LTL] queue_inserts : G((inited && op == push && data == pushed_data && X(op != pop))
63-
==> X(in_queue(pushed_data)));
64-
invariant[LTL] push_eventually_pops :
65-
G(F(op == pop)) ==> // assume a pop will always happen.
66-
G((inited && op == push && data == pushed_data) ==>
67-
F(op == pop && first == pushed_data));
68-
control {
69-
// print_module;
70-
v = concrete(5);
71-
check;
72-
print_results;
73-
//v.print_cex(op, data, pushed_data, head, tail, contents);
74-
}
75-
}
76-
1+
/*
2+
Test-conctete-6:
3+
1. test of assume
4+
2. test of Fuzzing
5+
*/
776
module main
787
{
79-
type op_t = common.op_t;
80-
81-
var op : op_t;
82-
var data : integer;
83-
84-
var step : integer;
85-
var head : integer;
86-
87-
instance queue_i : queue(op : (op'), data : (data), first : (head));
88-
89-
init {
90-
op = nop;
91-
data = 0;
92-
step = 0;
93-
}
94-
95-
next {
96-
//assert false;
97-
case
98-
(step == 0) || (step == 1) : { op' = push; }
99-
(step == 2) || (step == 3) : { op' = pop; }
100-
esac
101-
102-
step' = step+1;
103-
data' = data+2;
104-
next(queue_i);
105-
106-
if (step' == 2) {
107-
assert (head' == 1);
8+
var a : integer;
9+
var b : integer;
10+
init {
11+
assume(a==3);
12+
}
13+
next {
14+
a' = a + 1;
15+
assert(a>=3);
10816
}
109-
if (step' == 3) {
110-
assert (head' == 2);
111-
}
112-
}
11317

114-
control {
115-
//v = bmc(5);
116-
v = concrete(5);
117-
check;
118-
print_results;
119-
//v.print_concrete_trace();
120-
}
18+
control {
19+
v = concrete(5,"Default");
20+
check;
21+
print_results;
22+
}
12123
}

‎test/concrete/concrete-2.ucl‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
1. test of array
44
2. test of assert
55
3. test of touching undefine variable
6+
4. Should throw an Error on touch undefine variable (read)
67
*/
78
module main
89
{

‎test/concrete/concrete-3.ucl‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1+
/*
2+
concrete-3.ucl
3+
1. test of branch
4+
2. test of assert(false)
5+
*/
16
module main
27
{
38
var flag : boolean;

‎test/concrete/concrete-4.ucl‎

Lines changed: 20 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,23 @@
1+
/*
2+
Test-conctete-4:
3+
1. test of property failure
4+
2. test of concrete's Default
5+
3. test of avoid of property
6+
*/
17
module main
28
{
3-
var flag : boolean;
4-
5-
init { flag = true; }
6-
next {
7-
if (flag) {
8-
skip;
9-
} else {
10-
assert (false);
9+
var a : integer;
10+
var b : integer;
11+
init {
12+
b = 1;
1113
}
12-
}
13-
14-
control {
15-
v = concrete(5);
16-
check;
17-
print_results;
18-
}
19-
}
14+
next {
15+
a' = a + 1;
16+
}
17+
property jump_a: a!=3;
18+
19+
control {
20+
v = concrete(5,"Default");
21+
check;
22+
}
23+
}

‎test/concrete/concrete-5.ucl‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,7 @@
1+
/*
2+
Test-conctete-5:
3+
1. test of BV operation
4+
*/
15
module main
26
{
37
var a : bv4;

‎test/concrete/concrete-6.ucl‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,21 @@
1+
/*
2+
Test-conctete-6:
3+
1. test of property failure
4+
2. test of concrete's Default
5+
3. test of avoid of property
6+
*/
17
module main
28
{
39
var a : integer;
410
init {
5-
a = 0;
611
}
712
next {
813
a' = a + 1;
914
assert(a'< 3);
1015
}
1116

1217
control {
13-
v = concrete(5);
18+
v = concrete(5,"Default");
1419
check;
1520
print_results;
1621
//v.print_cex(n);

0 commit comments

Comments
 (0)