Skip to content

Commit d157bf7

Browse files
muralitawsmuralitaws
authored
Merge pull request diffblue#10 from lefanz-amazon/funcs
Fixed problems with abst_funcs integrating into goto-programs.
2 parents d7f0bdd + 8e48d6b commit d157bf7

File tree

4 files changed

+51
-74
lines changed

4 files changed

+51
-74
lines changed

‎regression/abstraction/abst-funcs.c

Lines changed: 44 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -1,37 +1,38 @@
11
#include <stdint.h>
2-
#include <cassert>
2+
#include <assert.h>
33

44
//Some helper functions.
55

6-
//nondet_bool, nondet_int, nondet_sizet are available in CBMC.
6+
//nndt_bool, nndt_int, nndt_sizet are available in CBMC.
77

8-
int nondet_int(){
8+
int nndt_int(){
99
int i;
1010
return(i);
1111
}
1212

13-
int nondet_bool(){
14-
bool b;
15-
return(b);
13+
int nndt_bool(){
14+
int i;
15+
return(i % 2);
1616
}
1717

18-
int nondet_under(int bound){
18+
19+
int nndt_under(int bound){
1920
int nd;
2021
// Mod is an expensive operation. We need to get rid of this.
2122
//return(nd%bound);
22-
__CPROVER_ASSUME(nd < bound);
23+
__CPROVER_assume(nd < bound);
2324
return(nd);
2425
}
2526

26-
int nondet_between(int l, int u){
27+
int nndt_between(int l, int u){
2728
int diff = u - l;
28-
int nd = nondet_under(diff);
29+
int nd = nndt_under(diff);
2930
if (nd == 0) return(l+1);
3031
else return(nd + l);
3132
}
3233

33-
int nondet_above(int bound){
34-
int nd = nondet_int();
34+
int nndt_above(int bound){
35+
int nd = nndt_int();
3536
if (nd > bound) return(nd);
3637
else return(bound + 1+ nd);
3738
}
@@ -59,20 +60,20 @@ int concretize_1(int abs_ind, int a1){
5960
if(abs_ind < 1) {
6061
if (a1 == 0)
6162
{
62-
assert(false);
63+
assert(0 != 0);
6364
return(-1);
6465
}
65-
else return(nondet_under(a1));
66+
else return(nndt_under(a1));
6667
}
6768
else if (abs_ind == 1) return(a1);
68-
else return(nondet_above(a1));
69+
else return(nndt_above(a1));
6970
}
7071

7172
// Add a number to an abs_ind
7273
int add_abs_to_conc_1(int abs_ind, int num, int a1){
7374
if (num == 1){
7475
if(abs_ind == 0) {
75-
if (nondet_bool()) return(abs_ind);
76+
if (nndt_bool() > 0) return(abs_ind);
7677
else return(abs_ind + 1);
7778
}
7879
//abs_ind = 1 or 2
@@ -91,7 +92,7 @@ int add_abs_to_conc_1(int abs_ind, int num, int a1){
9192
int sub_conc_from_abs_1(int abs_ind, int num, int a1, int a2){
9293
if (num == 1){
9394
if(abs_ind == 2) {
94-
if (nondet_bool()) return(abs_ind);
95+
if (nndt_bool() > 0) return(abs_ind);
9596
else return(abs_ind - 1);
9697
}
9798
//abs_ind = 1 0r 0
@@ -133,37 +134,39 @@ int concretize_2(int abs_ind, int a1, int a2) {
133134
if (a1 == 0)
134135
{
135136
//throw an exception here?
136-
assert(false);
137+
assert(0 != 0);
137138
return(-1);
138139
}
139-
else return(nondet_under(a1));
140+
else return(nndt_under(a1));
140141
}
141142
else if (abs_ind == 1) return(a1);
142143
else if (abs_ind == 2){
143144
if (a1+1 == a2 ) {
144145
//throw an exception here?
145-
assert(false);
146+
assert(0 != 0);
146147
return(-1);
147148
}
148-
else return(nondet_between(a1, a2));
149+
else return(nndt_between(a1, a2));
149150
}
150151
else if (abs_ind == 3) return(a2);
151-
else return(nondet_above(a2));
152+
else return(nndt_above(a2));
152153
}
153154

154-
bool is_precise_2(int abs_ind){
155-
return(abs_ind == 1 || abs_ind == 3);
155+
int is_precise_2(int abs_ind){
156+
if (abs_ind == 1 || abs_ind == 3) return(1);
157+
else return(0);
156158
}
157159

158-
bool is_abstract_2(int abs_ind){
159-
return(!is_precise_2(abs_ind));
160+
int is_abstract_2(int abs_ind){
161+
int pre = is_precise_2(abs_ind);
162+
return(1-pre);
160163
}
161164

162165
// Add a number to an abs_ind
163166
int add_abs_to_conc_2(int abs_ind, int num, int a1, int a2){
164167
if (num == 1){
165168
if(abs_ind == 0 || abs_ind == 2) {
166-
if (nondet_bool()) return(abs_ind);
169+
if (nndt_bool() > 0) return(abs_ind);
167170
else return(abs_ind + 1);
168171
}
169172
else if (abs_ind == 1) {
@@ -187,7 +190,7 @@ int add_abs_to_conc_2(int abs_ind, int num, int a1, int a2){
187190
int sub_conc_from_abs_2(int abs_ind, int num, int a1, int a2){
188191
if (num == 1){
189192
if(abs_ind == 4 || abs_ind == 2) {
190-
if (nondet_bool()) return(abs_ind);
193+
if (nndt_bool() > 0) return(abs_ind);
191194
else return(abs_ind - 1);
192195
}
193196
else if (abs_ind == 3) {
@@ -248,39 +251,41 @@ int concretize_4(int abs_ind, int a1, int a2, int a3, int a4) {
248251
if (a1 == 0)
249252
{
250253
//throw an exception here?
251-
assert(false);
254+
assert(0 != 0);
252255
return(-1);
253256
}
254-
else return(nondet_under(a1));
257+
else return(nndt_under(a1));
255258
}
256259
else if (abs_ind == 1) return(a1);
257260
else if (abs_ind == 2) return(a2);
258261
else if (abs_ind == 3){
259262
if (a2+1 == a3 ) {
260263
//throw an exception here?
261-
assert(false);
264+
assert(0 != 0);
262265
return(-1);
263266
}
264-
else return(nondet_between(a2, a3));
267+
else return(nndt_between(a2, a3));
265268
}
266269
else if (abs_ind == 4) return(a3);
267270
else if (abs_ind == 5) return(a4);
268-
else return(nondet_above(a4));
271+
else return(nndt_above(a4));
269272
}
270273

271-
bool is_precise_4(int abs_ind){
272-
return(abs_ind == 1 || abs_ind == 2 || abs_ind == 4 || abs_ind == 5);
274+
int is_precise_4(int abs_ind){
275+
if (abs_ind == 1 || abs_ind == 2 || abs_ind == 4 || abs_ind == 5) return(1);
276+
else return(0);
273277
}
274278

275-
bool is_abstract_4(int abs_ind){
276-
return(!is_precise_4(abs_ind));
279+
int is_abstract_4(int abs_ind){
280+
if(!is_precise_4(abs_ind)) return(1);
281+
else return(0);
277282
}
278283

279284
// Add a number to an abs_ind
280285
int add_abs_to_conc_4(int abs_ind, int num, int a1, int a2, int a3, int a4){
281286
if (num == 1){
282287
if(abs_ind == 0 || abs_ind == 3) {
283-
if (nondet_bool()) return(abs_ind);
288+
if (nndt_bool() > 0) return(abs_ind);
284289
else return(abs_ind + 1);
285290
}
286291
else if (abs_ind == 1) return(2);
@@ -306,7 +311,7 @@ int add_abs_to_conc_4(int abs_ind, int num, int a1, int a2, int a3, int a4){
306311
int sub_conc_from_abs_4(int abs_ind, int num, int a1, int a2, int a3, int a4){
307312
if (num == 1){
308313
if(abs_ind == 6 || abs_ind == 3) {
309-
if (nondet_bool()) return(abs_ind);
314+
if (nndt_bool() > 0) return(abs_ind);
310315
else return(abs_ind - 1);
311316
}
312317
else if (abs_ind == 5 || abs_ind == 2 || abs_ind == 1) return(abs_ind-1);

‎regression/abstraction/aws_byte_cursor_left_trim_pred.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@
1414
"add-abs-conc": "add_abs_to_conc",
1515
"sub-abs-conc": "sub_conc_from_abs",
1616
"precise-check": "is_precise",
17-
"abstract-index": "two_abs",
17+
"abstract-index": "one_abs",
1818
"concretize-index": "concretize",
1919
"multiply-indices": null,
2020
"mod-indices": null

‎regression/abstraction/test.sh

Lines changed: 3 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -5,12 +5,11 @@ CHECK=false
55

66
# paths to the benchmark repos
77
AWS_C_COMMON_PATH="/home/ubuntu/aws-c-common"
8-
AWS_IOT_SDK_PATH="/home/ubuntu/aws-iot-device-sdk-embedded-C-tuttle"
98

109
# executables
1110
MAKE="make"
12-
GOTO_INSTRUMENT="goto-instrument"
13-
CBMC="cbmc"
11+
GOTO_INSTRUMENT="/home/ubuntu/abstract-cbmc/cbmc/build/bin/goto-instrument"
12+
CBMC="/home/ubuntu/abstract-cbmc/cbmc/build/bin/cbmc"
1413
CBMC_FLAGS="--unwind 10
1514
--bounds-check
1615
--pointer-check
@@ -27,16 +26,8 @@ CBMC_FLAGS="--unwind 10
2726

2827
AWS_C_COMMON_TESTS=(
2928
"aws_array_eq"
30-
"aws_array_eq_c_str_ignore_case"
31-
"aws_array_eq_ignore_case"
32-
"aws_array_list_comparator_string"
33-
"aws_array_list_front"
34-
"aws_array_list_get_at"
35-
"aws_array_list_pop_back"
3629
)
3730

38-
AWS_IOT_SDK_TEST="skip_string"
39-
4031
cwd=$(pwd)
4132
for test in ${AWS_C_COMMON_TESTS[@]}; do
4233
echo "===== $test ====="
@@ -51,30 +42,11 @@ for test in ${AWS_C_COMMON_TESTS[@]}; do
5142
$AWS_C_COMMON_PATH/.cbmc-batch/jobs/$test/${test}_harness_abst.goto
5243
# print the goto-programs into txts
5344
rm $AWS_C_COMMON_PATH/.cbmc-batch/jobs/$test/${test}_harness_abst.txt
54-
$GOTO_INSTRUMENT --print-internal-representation \
45+
$GOTO_INSTRUMENT --show-goto-functions \
5546
$AWS_C_COMMON_PATH/.cbmc-batch/jobs/$test/${test}_harness_abst.goto \
5647
>> $AWS_C_COMMON_PATH/.cbmc-batch/jobs/$test/${test}_harness_abst.txt
5748
# check the program
5849
if [ $CHECK = true ]; then
5950
$CBMC $CBMC_FLAGS $AWS_C_COMMON_PATH/.cbmc-batch/jobs/$test/${test}_harness_abst.goto
6051
fi
6152
done
62-
63-
echo "===== $AWS_IOT_SDK_TEST ====="
64-
cd $AWS_IOT_SDK_PATH/cbmc/proofs/JsonParser/proofs
65-
# compile program into goto-programs
66-
$MAKE goto ENTRY=String 2&>1
67-
cd $cwd
68-
# run goto-instrument to make abstracted goto-programs
69-
$GOTO_INSTRUMENT --use-abstraction $cwd/$AWS_IOT_SDK_TEST.json \
70-
$AWS_IOT_SDK_PATH/cbmc/proofs/JsonParser/proofs/String.goto \
71-
$AWS_IOT_SDK_PATH/cbmc/proofs/JsonParser/proofs/String_abst.goto
72-
# print the goto-programs into txts
73-
rm $AWS_IOT_SDK_PATH/cbmc/proofs/JsonParser/proofs/String_abst.txt
74-
$GOTO_INSTRUMENT --print-internal-representation \
75-
$AWS_IOT_SDK_PATH/cbmc/proofs/JsonParser/proofs/String_abst.goto \
76-
>> $AWS_IOT_SDK_PATH/cbmc/proofs/JsonParser/proofs/String_abst.txt
77-
# check the program
78-
if [ $CHECK = true ]; then
79-
$CBMC $CBMC_FLAGS $AWS_IOT_SDK_PATH/cbmc/proofs/JsonParser/proofs/String_abst.goto
80-
fi

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1136,9 +1136,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
11361136

11371137
std::vector<std::string> abstfiles = abst_spec.get_abstraction_function_files();
11381138

1139-
// log.status() << "Reading in abst funcs goto-model" << messaget::eom;
1140-
// link_abst_functions(goto_model, abst_spec, ui_message_handler, options);
1141-
// log.status() << "Abst functions linked to goto-program" << messaget::eom;
1139+
log.status() << "Reading in abst funcs goto-model" << messaget::eom;
1140+
link_abst_functions(goto_model, abst_spec, ui_message_handler, options);
1141+
log.status() << "Abst functions linked to goto-program" << messaget::eom;
11421142

11431143
log.status() << "Analyzing index variables related to the entity" << messaget::eom;
11441144
abstract_goto_program(goto_model, abst_spec);

0 commit comments

Comments
 (0)