Skip to content

Commit 8ea516a

Browse files
committed
Refactor code contracts utility functions
In this change, we move two of the "static" functions within contracts.cpp to utils.cpp (a new file in contracts module). We also fix the #include dependence -- assigns should not #include contracts.h, it should be the other way round.
1 parent c3d7235 commit 8ea516a

File tree

6 files changed

+111
-61
lines changed

6 files changed

+111
-61
lines changed

src/goto-instrument/contracts/assigns.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,11 @@ Date: July 2021
1515

1616
#include <goto-instrument/havoc_utils.h>
1717

18+
#include <langapi/language_util.h>
19+
1820
#include <util/arith_tools.h>
1921
#include <util/c_types.h>
22+
#include <util/pointer_offset_size.h>
2023
#include <util/pointer_predicates.h>
2124

2225
assigns_clauset::targett::targett(

src/goto-instrument/contracts/assigns.h

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,12 @@ Date: July 2021
1414
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
1515
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
1616

17-
#include "contracts.h"
17+
#include <unordered_set>
1818

19-
#include <util/pointer_offset_size.h>
19+
#include <goto-programs/goto_model.h>
20+
21+
#include <util/message.h>
22+
#include <util/pointer_expr.h>
2023

2124
/// \brief A class for representing assigns clauses in code contracts
2225
class assigns_clauset

src/goto-instrument/contracts/contracts.cpp

Lines changed: 5 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ Date: February 2016
2424

2525
#include <goto-programs/remove_skip.h>
2626

27+
#include <langapi/language_util.h>
28+
2729
#include <util/c_types.h>
2830
#include <util/expr_util.h>
2931
#include <util/fresh_symbol.h>
@@ -35,62 +37,7 @@ Date: February 2016
3537

3638
#include "assigns.h"
3739
#include "memory_predicates.h"
38-
39-
// Create a lexicographic less-than relation between two tuples of variables.
40-
// This is used in the implementation of multidimensional decreases clauses.
41-
static exprt create_lexicographic_less_than(
42-
const std::vector<symbol_exprt> &lhs,
43-
const std::vector<symbol_exprt> &rhs)
44-
{
45-
PRECONDITION(lhs.size() == rhs.size());
46-
47-
if(lhs.empty())
48-
{
49-
return false_exprt();
50-
}
51-
52-
// Store conjunctions of equalities.
53-
// For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
54-
// l2, l3>.
55-
// Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
56-
// s1 == l1 && s2 == l2 && s3 == l3>.
57-
// In fact, the last element is unnecessary, so we do not create it.
58-
exprt::operandst equality_conjunctions(lhs.size());
59-
equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
60-
for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
61-
{
62-
binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
63-
equality_conjunctions[i] =
64-
and_exprt(equality_conjunctions[i - 1], component_i_equality);
65-
}
66-
67-
// Store inequalities between the i-th components of the input vectors
68-
// (i.e. lhs and rhs).
69-
// For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
70-
// l2, l3>.
71-
// Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
72-
// s2 == l2 && s3 < l3>.
73-
exprt::operandst lexicographic_individual_comparisons(lhs.size());
74-
lexicographic_individual_comparisons[0] =
75-
binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
76-
for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
77-
{
78-
binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
79-
lexicographic_individual_comparisons[i] =
80-
and_exprt(equality_conjunctions[i - 1], component_i_less_than);
81-
}
82-
return disjunction(lexicographic_individual_comparisons);
83-
}
84-
85-
static void insert_before_swap_and_advance(
86-
goto_programt &program,
87-
goto_programt::targett &target,
88-
goto_programt &payload)
89-
{
90-
const auto offset = payload.instructions.size();
91-
program.insert_before_swap(target, payload);
92-
std::advance(target, offset);
93-
}
40+
#include "utils.h"
9441

9542
void code_contractst::check_apply_loop_contracts(
9643
goto_functionst::goto_functiont &goto_function,
@@ -289,7 +236,8 @@ void code_contractst::check_apply_loop_contracts(
289236
// after the loop is smaller than the value before the loop.
290237
// Here, we use the lexicographic order.
291238
code_assertt monotonic_decreasing_assertion{
292-
create_lexicographic_less_than(new_decreases_vars, old_decreases_vars)};
239+
generate_lexicographic_less_than_check(
240+
new_decreases_vars, old_decreases_vars)};
293241
monotonic_decreasing_assertion.add_source_location() =
294242
loop_head->source_location;
295243
converter.goto_convert(monotonic_decreasing_assertion, havoc_code, mode);

src/goto-instrument/contracts/contracts.h

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,6 @@ Date: February 2016
2525
#include <goto-programs/goto_functions.h>
2626
#include <goto-programs/goto_model.h>
2727

28-
#include <langapi/language_util.h>
29-
3028
#include <util/message.h>
3129
#include <util/namespace.h>
3230
#include <util/pointer_expr.h>
Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
/*******************************************************************\
2+
3+
Module: Utility functions for code contracts.
4+
5+
Author: Saswat Padhi, [email protected]
6+
7+
Date: September 2021
8+
9+
\*******************************************************************/
10+
11+
#include "utils.h"
12+
13+
// Create a lexicographic less-than relation between two tuples of variables.
14+
// This is used in the implementation of multidimensional decreases clauses.
15+
exprt generate_lexicographic_less_than_check(
16+
const std::vector<symbol_exprt> &lhs,
17+
const std::vector<symbol_exprt> &rhs)
18+
{
19+
PRECONDITION(lhs.size() == rhs.size());
20+
21+
if(lhs.empty())
22+
{
23+
return false_exprt();
24+
}
25+
26+
// Store conjunctions of equalities.
27+
// For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
28+
// l2, l3>.
29+
// Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
30+
// s1 == l1 && s2 == l2 && s3 == l3>.
31+
// In fact, the last element is unnecessary, so we do not create it.
32+
exprt::operandst equality_conjunctions(lhs.size());
33+
equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
34+
for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
35+
{
36+
binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
37+
equality_conjunctions[i] =
38+
and_exprt(equality_conjunctions[i - 1], component_i_equality);
39+
}
40+
41+
// Store inequalities between the i-th components of the input vectors
42+
// (i.e. lhs and rhs).
43+
// For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
44+
// l2, l3>.
45+
// Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
46+
// s2 == l2 && s3 < l3>.
47+
exprt::operandst lexicographic_individual_comparisons(lhs.size());
48+
lexicographic_individual_comparisons[0] =
49+
binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
50+
for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
51+
{
52+
binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
53+
lexicographic_individual_comparisons[i] =
54+
and_exprt(equality_conjunctions[i - 1], component_i_less_than);
55+
}
56+
return disjunction(lexicographic_individual_comparisons);
57+
}
58+
59+
void insert_before_swap_and_advance(
60+
goto_programt &program,
61+
goto_programt::targett &target,
62+
goto_programt &payload)
63+
{
64+
const auto offset = payload.instructions.size();
65+
program.insert_before_swap(target, payload);
66+
std::advance(target, offset);
67+
}

src/goto-instrument/contracts/utils.h

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
/*******************************************************************\
2+
3+
Module: Utility functions for code contracts.
4+
5+
Author: Saswat Padhi, [email protected]
6+
7+
Date: September 2021
8+
9+
\*******************************************************************/
10+
11+
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
12+
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
13+
14+
#include <vector>
15+
16+
#include <goto-programs/goto_model.h>
17+
18+
/// \brief
19+
/// Create an expression that represents a lexicographic less-than
20+
/// comparison between two tuples of variables.
21+
/// This is used in instrumentation of decreases clauses.
22+
exprt generate_lexicographic_less_than_check(
23+
const std::vector<symbol_exprt> &lhs,
24+
const std::vector<symbol_exprt> &rhs);
25+
26+
void insert_before_swap_and_advance(
27+
goto_programt &program,
28+
goto_programt::targett &target,
29+
goto_programt &payload);
30+
31+
#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H

0 commit comments

Comments
 (0)