Skip to content

Commit ba905f4

Browse files
lichyelichye
committed
add ConcreteSimutalor with the same output result
add autotester fix up bugs
1 parent c5c474c commit ba905f4

File tree

13 files changed

+572
-128
lines changed

13 files changed

+572
-128
lines changed

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

Lines changed: 96 additions & 128 deletions
Large diffs are not rendered by default.

‎src/test/scala/ConcreteSpec.scala‎

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
/*
2+
* UCLID5 Verification and Synthesis Engine
3+
*
4+
* Copyright (c) 2017.
5+
* Sanjit A. Seshia, Rohit Sinha and Pramod Subramanyan.
6+
*
7+
* All Rights Reserved.
8+
* Redistribution and use in source and binary forms, with or without
9+
* modification, are permitted provided that the following conditions are
10+
* met:
11+
* 1. Redistributions of source code must retain the above copyright notice,
12+
*
13+
* this list of conditions and the following disclaimer.
14+
* 2. Redistributions in binary form must reproduce the above copyright
15+
* notice, this list of conditions and the following disclaimer in the
16+
*
17+
* documentation and/or other materials provided with the distribution.
18+
* 3. Neither the name of the copyright holder nor the names of its
19+
* contributors may be used to endorse or promote products derived from this
20+
* software without specific prior written permission.
21+
*
22+
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
23+
* IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
24+
* THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
25+
* PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR
26+
* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
27+
* EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
28+
* PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
29+
* PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
30+
* LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
31+
* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
32+
* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
33+
*
34+
* Author: Leiqi Ye
35+
*
36+
* UCLID concrte tests
37+
*
38+
*/
39+
40+
package uclid
41+
package test
42+
43+
import org.scalatest.flatspec.AnyFlatSpec
44+
import java.io.File
45+
import uclid.{lang => l}
46+
47+
object ConcreteSpec {
48+
def expectedFails(filename: String, nFail : Int) : String = {
49+
UclidMain.enableStringOutput()
50+
UclidMain.clearStringOutput()
51+
val config = UclidMain.Config().copy(simulate=true)
52+
val modules = UclidMain.compile(ConfigCons.createConfig(filename), lang.Identifier("main"), true)
53+
val mainModule = UclidMain.instantiate(config, modules, l.Identifier("main"))
54+
assert (mainModule.isDefined)
55+
val results = UclidMain.execute(mainModule.get, config)
56+
val outputString = UclidMain.stringOutput.toString()
57+
assert (results.count((e) => e.result.isFalse) == nFail)
58+
assert (results.count((e) => e.result.isUndefined) == 0)
59+
outputString
60+
}
61+
}
62+
class ConcreteSpec extends AnyFlatSpec {
63+
"concrete-0.ucl" should "fail one assertion." in {
64+
ConcreteSpec.expectedFails("./test/concrete/concrete-0.ucl", 1)
65+
}
66+
"concrete-1.ucl" should "pass." in {
67+
ConcreteSpec.expectedFails("./test/concrete/concrete-1.ucl", 0)
68+
}
69+
"concrete-2.ucl" should "pass." in {
70+
ConcreteSpec.expectedFails("./test/concrete/concrete-2.ucl", 0)
71+
}
72+
"concrete-3.ucl" should "fail one assertion." in {
73+
ConcreteSpec.expectedFails("./test/concrete/concrete-3.ucl", 1)
74+
}
75+
"concrete-4.ucl" should "pass." in {
76+
ConcreteSpec.expectedFails("./test/concrete/concrete-4.ucl", 0)
77+
}
78+
"concrete-5.ucl" should "pass." in {
79+
ConcreteSpec.expectedFails("./test/concrete/concrete-5.ucl", 0)
80+
}
81+
"concrete-6.ucl" should "fail one assertion." in {
82+
ConcreteSpec.expectedFails("./test/concrete/concrete-6.ucl", 1)
83+
}
84+
"concrete-7.ucl" should "pass." in {
85+
ConcreteSpec.expectedFails("./test/concrete/concrete-7.ucl", 0)
86+
}
87+
"concrete-8.ucl" should "pass." in {
88+
ConcreteSpec.expectedFails("./test/concrete/concrete-8.ucl", 1)
89+
}
90+
"concrete-9.ucl" should "fail one assertion." in {
91+
ConcreteSpec.expectedFails("./test/concrete/concrete-9.ucl", 1)
92+
}
93+
"concrete-10.ucl" should "fail one assertion." in {
94+
ConcreteSpec.expectedFails("./test/concrete/concrete-10.ucl", 1)
95+
}
96+
}

‎test/concrete/concrete-0.ucl‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
module main
2+
{
3+
var a : integer;
4+
var b : integer;
5+
init {
6+
a = 0;
7+
b = 1;
8+
}
9+
next {
10+
a' = a + 1;
11+
// assert(a !=3);
12+
}
13+
property jump_a: a!=3;
14+
15+
control {
16+
v = bmc(5);
17+
// v = concrete(5);
18+
//v = concrete(5,"Panic");
19+
//v = concrete(5,"Default");
20+
// v = concrete(5,"Json","Leiqi.json");
21+
22+
23+
// v = concrete(5,"Random");
24+
// v = concrete(5,"Fuzzing");
25+
26+
check;
27+
//v.read_from_json("cex.json");
28+
// v.print_concrete_trace(a);
29+
}
30+
}

‎test/concrete/concrete-1.ucl‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
module main
2+
{
3+
type color_t = enum { red, blue };
4+
5+
var red_cnt : integer;
6+
var color : color_t;
7+
8+
procedure next_color()
9+
modifies color;
10+
{
11+
color = blue;
12+
if (red_cnt > 0) {
13+
color = red;
14+
}
15+
if(color == red) {
16+
assert (red_cnt > 0);
17+
}
18+
}
19+
20+
init { }
21+
22+
next {
23+
call next_color();
24+
}
25+
26+
control {
27+
// print_module;
28+
x = concrete(3);
29+
check;
30+
print_results;
31+
}
32+
}

‎test/concrete/concrete-10.ucl‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
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+
77+
module main
78+
{
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);
108+
}
109+
if (step' == 3) {
110+
assert (head' == 2);
111+
}
112+
}
113+
114+
control {
115+
//v = bmc(5);
116+
v = concrete(5);
117+
check;
118+
print_results;
119+
//v.print_concrete_trace();
120+
}
121+
}

‎test/concrete/concrete-2.ucl‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
module main
2+
{
3+
type num_t = integer;
4+
var numbers : [boolean]integer;
5+
var zero : integer;
6+
var read: integer;
7+
init {
8+
numbers[true] = 0;
9+
zero = numbers[true];
10+
}
11+
12+
next {
13+
}
14+
15+
control {
16+
v = concrete (5);
17+
check;
18+
print_results;
19+
v.print_cex(numbers);
20+
}
21+
}

‎test/concrete/concrete-3.ucl‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module main
2+
{
3+
var flag : boolean;
4+
5+
init { flag = false; }
6+
next {
7+
if (flag) {
8+
skip;
9+
} else {
10+
assert (false);
11+
}
12+
}
13+
14+
control {
15+
v = concrete(5);
16+
check;
17+
print_results;
18+
}
19+
}

‎test/concrete/concrete-4.ucl‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module main
2+
{
3+
var flag : boolean;
4+
5+
init { flag = true; }
6+
next {
7+
if (flag) {
8+
skip;
9+
} else {
10+
assert (false);
11+
}
12+
}
13+
14+
control {
15+
v = concrete(5);
16+
check;
17+
print_results;
18+
}
19+
}

‎test/concrete/concrete-5.ucl‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
module main
2+
{
3+
var a : bv4;
4+
var b : bv4;
5+
var c : bv4;
6+
var d : bv4;
7+
var e : bv4;
8+
var compare: boolean;
9+
init {
10+
a = 0bv4;
11+
b = 10bv4;
12+
a = 16bv4-b; // a should be 6
13+
compare = a < b;
14+
c = ~a;
15+
d = -a;
16+
compare = a == b;
17+
assert(compare == false);
18+
compare = a !=b;
19+
assert(compare == true);
20+
}
21+
next {
22+
a' = a + 1bv4;
23+
}
24+
property jump_a: a!=3bv4;
25+
26+
control {
27+
v = concrete(5);
28+
check;
29+
print_results;
30+
//v.print_cex(n);
31+
}
32+
}

‎test/concrete/concrete-6.ucl‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
module main
2+
{
3+
var a : integer;
4+
init {
5+
a = 0;
6+
}
7+
next {
8+
a' = a + 1;
9+
assert(a'< 3);
10+
}
11+
12+
control {
13+
v = concrete(5);
14+
check;
15+
print_results;
16+
//v.print_cex(n);
17+
}
18+
}

0 commit comments

Comments
 (0)