Skip to content

Commit 1fad927

Browse files
Long PhamAalok Thakkar
Long Pham
authored and
Aalok Thakkar
committed
Implemented parsing and type checking for loop variants
1 parent 86bf65c commit 1fad927

File tree

21 files changed

+167
-26
lines changed

21 files changed

+167
-26
lines changed

‎regression/contracts/invar_check_break_pass/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,10 @@ int main()
66
__CPROVER_assume(r >= 0);
77

88
while(r > 0)
9+
// clang-format off
910
__CPROVER_loop_invariant(r >= 0)
11+
__CPROVER_decreases(r)
12+
// clang-format on
1013
{
1114
--r;
1215
if(r <= 1)

‎regression/contracts/invar_check_continue/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,10 @@ int main()
66
__CPROVER_assume(r >= 0);
77

88
while(r > 0)
9+
// clang-format off
910
__CPROVER_loop_invariant(r >= 0)
11+
__CPROVER_decreases(r)
12+
// clang-format on
1013
{
1114
--r;
1215
if(r < 5)

‎regression/contracts/invar_check_large/main.c

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,9 @@ int main()
2222
int l = 0;
2323
int r = 1;
2424
while(h > l)
25+
// clang-format off
2526
__CPROVER_loop_invariant(
2627
// Turn off `clang-format` because it breaks the `==>` operator.
27-
/* clang-format off */
2828
h >= l &&
2929
0 <= l && l < 5 &&
3030
0 <= h && h < 5 &&
@@ -44,8 +44,9 @@ int main()
4444
(2 > h ==> arr2 >= pivot) &&
4545
(3 > h ==> arr3 >= pivot) &&
4646
(4 > h ==> arr4 >= pivot)
47-
/* clang-format on */
4847
)
48+
__CPROVER_decreases(h - l)
49+
// clang-format on
4950
{
5051
if(*(arr[h]) <= pivot && *(arr[l]) >= pivot)
5152
{

‎regression/contracts/invar_check_multiple_loops/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,18 @@ int main()
66
__CPROVER_assume(n > 0 && x == y);
77

88
for(r = 0; r < n; ++r)
9+
// clang-format off
910
__CPROVER_loop_invariant(0 <= r && r <= n && x == y + r)
11+
__CPROVER_decreases(n - r)
12+
// clang-format on
1013
{
1114
x++;
1215
}
1316
while(r > 0)
17+
// clang-format off
1418
__CPROVER_loop_invariant(r >= 0 && x == y + n + (n - r))
19+
__CPROVER_decreases(r)
20+
// clang-format on
1521
{
1622
y--;
1723
r--;

‎regression/contracts/invar_check_nested_loops/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,19 @@ int main()
66
__CPROVER_assume(n >= 0);
77

88
for(int i = 0; i < n; ++i)
9+
// clang-format off
910
__CPROVER_loop_invariant(i <= n && s == i)
11+
__CPROVER_decreases(n - i)
12+
// clang-format on
1013
{
1114
int a, b;
1215
__CPROVER_assume(b >= 0 && a == b);
1316

1417
while(a > 0)
18+
// clang-format off
1519
__CPROVER_loop_invariant(a >= 0 && s == i + (b - a))
20+
__CPROVER_decreases(a)
21+
// clang-format on
1622
{
1723
s++;
1824
a--;

‎regression/contracts/invar_check_pointer_modifies-01/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,10 @@ void main()
88

99
unsigned i;
1010
while(i > 0)
11+
// clang-format off
1112
__CPROVER_loop_invariant(*data == 42)
13+
__CPROVER_decreases(i)
14+
// clang-format on
1215
{
1316
*data = 42;
1417
i--;

‎regression/contracts/invar_check_pointer_modifies-02/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,10 @@ void main()
1010

1111
unsigned i;
1212
while(i > 0)
13+
// clang-format off
1314
__CPROVER_loop_invariant(*data == 42)
15+
__CPROVER_decreases(i)
16+
// clang-format on
1417
{
1518
*data = 42;
1619
i--;

‎regression/contracts/invar_check_sufficiency/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,10 @@ int main()
66
__CPROVER_assume(r >= 0);
77

88
while(r > 0)
9+
// clang-format off
910
__CPROVER_loop_invariant(r >= 0)
11+
__CPROVER_decreases(r)
12+
// clang-format on
1013
{
1114
--r;
1215
}

‎regression/contracts/invar_loop_constant_no_modify/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,10 @@ int main()
66
int s = 1;
77
__CPROVER_assume(r >= 0);
88
while(r > 0)
9+
// clang-format off
910
__CPROVER_loop_invariant(r >= 0)
11+
__CPROVER_decreases(r)
12+
// clang-format on
1013
{
1114
r--;
1215
}

‎regression/contracts/invar_loop_constant_pass/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,10 @@ int main()
55
int r, s = 1;
66
__CPROVER_assume(r >= 0);
77
while(r > 0)
8+
// clang-format off
89
__CPROVER_loop_invariant(r >= 0 && s == 1)
10+
__CPROVER_decreases(r)
11+
// clang-format on
912
{
1013
s = 1;
1114
r--;

‎regression/contracts/invariant_side_effects/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,10 @@ int main()
77

88
*a = 0;
99
while(*a < N)
10+
// clang-format off
1011
__CPROVER_loop_invariant((0 <= *a) && (*a <= N))
12+
__CPROVER_decreases(N - *a)
13+
// clang-format on
1114
{
1215
++(*a);
1316
}

‎regression/contracts/variant_parsing_statement_fail/main.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
2+
int main()
3+
{
4+
int i = 0;
5+
int N = 10;
6+
while(i != N)
7+
// clang-format off
8+
__CPROVER_loop_invariant(0 <= i && i <= N)
9+
__CPROVER_decreases(int x = 0)
10+
// clang-format on
11+
{
12+
i++;
13+
}
14+
15+
return 0;
16+
}

‎regression/contracts/variant_parsing_statement_fail/test.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
activate-multi-line-match
5+
^main.c.*error: syntax error before 'int'\n.*__CPROVER_decreases\(int x = 0\)$
6+
^PARSING ERROR$
7+
^EXIT=(1|64)$
8+
^SIGNAL=0$
9+
--
10+
--
11+
This test fails because the loop variant is a statement (more precisely,
12+
an assignment) rather than an expression (more precisely, an ACSL binding
13+
expression).

‎regression/contracts/variant_parsing_tuple_fail/main.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
int main()
2+
{
3+
int i = 0;
4+
int N = 10;
5+
while(i != N)
6+
// clang-format off
7+
__CPROVER_loop_invariant(0 <= i && i <= N)
8+
__CPROVER_decreases(N - i, 42)
9+
// clang-format on
10+
{
11+
i++;
12+
}
13+
14+
return 0;
15+
}

‎regression/contracts/variant_parsing_tuple_fail/test.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
activate-multi-line-match
5+
^main.c.*error: syntax error before ','\n.*__CPROVER_decreases\(N - i, 42\)$
6+
^PARSING ERROR$
7+
^EXIT=(1|64)$
8+
^SIGNAL=0$
9+
--
10+
--
11+
This test fails because the loop variant has two arguments instead of just one.
12+
Currently, we only support loop variants of single arguments - we do not
13+
support loop variants of tuples (yet).

‎src/ansi-c/c_typecheck_base.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,8 @@ class c_typecheck_baset:
144144
virtual void typecheck_while(code_whilet &code);
145145
virtual void typecheck_dowhile(code_dowhilet &code);
146146
virtual void typecheck_start_thread(codet &code);
147-
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec);
147+
virtual void typecheck_spec_loop_invariant(codet &code);
148+
virtual void typecheck_spec_decreases(codet &code);
148149

149150
bool break_is_allowed;
150151
bool continue_is_allowed;

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 22 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -484,7 +484,8 @@ void c_typecheck_baset::typecheck_for(codet &code)
484484
typecheck_code(code); // recursive call
485485
}
486486

487-
typecheck_spec_expr(code, ID_C_spec_loop_invariant);
487+
typecheck_spec_loop_invariant(code);
488+
typecheck_spec_decreases(code);
488489
}
489490

490491
void c_typecheck_baset::typecheck_label(code_labelt &code)
@@ -772,7 +773,8 @@ void c_typecheck_baset::typecheck_while(code_whilet &code)
772773
break_is_allowed=old_break_is_allowed;
773774
continue_is_allowed=old_continue_is_allowed;
774775

775-
typecheck_spec_expr(code, ID_C_spec_loop_invariant);
776+
typecheck_spec_loop_invariant(code);
777+
typecheck_spec_decreases(code);
776778
}
777779

778780
void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
@@ -805,16 +807,28 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
805807
break_is_allowed=old_break_is_allowed;
806808
continue_is_allowed=old_continue_is_allowed;
807809

808-
typecheck_spec_expr(code, ID_C_spec_loop_invariant);
810+
typecheck_spec_loop_invariant(code);
811+
typecheck_spec_decreases(code);
809812
}
810813

811-
void c_typecheck_baset::typecheck_spec_expr(codet &code, const irep_idt &spec)
814+
void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
812815
{
813-
if(code.find(spec).is_not_nil())
816+
if(code.find(ID_C_spec_loop_invariant).is_not_nil())
814817
{
815-
exprt &constraint = static_cast<exprt &>(code.add(spec));
818+
exprt &invariant = static_cast<exprt &>(code.add(ID_C_spec_loop_invariant));
816819

817-
typecheck_expr(constraint);
818-
implicit_typecast_bool(constraint);
820+
typecheck_expr(invariant);
821+
implicit_typecast_bool(invariant);
822+
}
823+
}
824+
825+
void c_typecheck_baset::typecheck_spec_decreases(codet &code)
826+
{
827+
if(code.find(ID_C_spec_decreases).is_not_nil())
828+
{
829+
exprt &variant = static_cast<exprt &>(code.add(ID_C_spec_decreases));
830+
831+
typecheck_expr(variant);
832+
implicit_typecast_arithmetic(variant);
819833
}
820834
}

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ void c_typecheck_baset::typecheck_expr(exprt &expr)
5151
return;
5252
}
5353

54-
// fist do sub-nodes
54+
// first do sub-nodes
5555
typecheck_expr_operands(expr);
5656

5757
// now do case-split

0 commit comments

Comments
 (0)