Skip to content

Commit 5cc78c4

Browse files
kroeningkroening
committed
introduce 'fatal assertions'
This introduces a variant of ASSERT instructions that are fatal when they are refuted. Execution paths through fatal assertions that are refuted are undefined. Assertions that (otherwise) pass and that are reachable from a refuted fatal assertion are now reported as UNKNOWN. The motivating use-case for fatal assertions is undefined behavior in languages such as C/C++ or Rust. Noi attempt is made to modify the outcome of ASSERT instructions that are refuted owing to a trace through a refuted fatal assertion. The computation of the trace is not robust enough.
1 parent 08b2f2f commit 5cc78c4

File tree

13 files changed

+318
-19
lines changed

13 files changed

+318
-19
lines changed

‎regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
div_by_zero.c
33
--div-by-zero-check --trace
44
\[main\.division-by-zero\.1\] line \d division by zero in x / y: FAILURE
5-
\[main\.division-by-zero\.2\] line \d+ division by zero in x / z: SUCCESS
5+
\[main\.division-by-zero\.2\] line \d+ division by zero in x / z: UNKNOWN
66
y=0
77
^VERIFICATION FAILED$
88
^EXIT=10$

‎regression/cbmc/Division3/main.c

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
_Bool nondet_bool();
2+
3+
void main()
4+
{
5+
__CPROVER_assert(0, "non-fatal assertion");
6+
7+
if(nondet_bool())
8+
{
9+
int divisor = nondet_bool() ? 2 : 0;
10+
11+
// possible division by zero
12+
int result = 10 / divisor;
13+
14+
__CPROVER_assert(divisor == 2 || divisor == 0, "divisor value");
15+
}
16+
else
17+
__CPROVER_assert(0, "independent assertion");
18+
}

‎regression/cbmc/Division3/test.desc

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1\] line 5 non-fatal assertion: FAILURE$
7+
^\[main\.division-by-zero\.1\] line 12 division by zero in 10 / divisor: FAILURE$
8+
^\[main\.assertion\.2\] line 14 divisor value: UNKNOWN$
9+
^\[main\.assertion\.3\] line 17 independent assertion: FAILURE$
10+
^\*\* 3 of 4 failed
11+
^VERIFICATION FAILED$
12+
--
13+
^warning: ignoring

‎regression/cbmc/pragma_cprover_enable_all/test.desc

+13-13
Original file line numberDiff line numberDiff line change
@@ -8,22 +8,22 @@ main.c
88
^\[main\.float-division-by-zero\.\d+\] line 87 floating-point division by zero in x / den: FAILURE
99
^\[main\.overflow\.\d+\] line 87 arithmetic overflow on floating-point division in x / den: FAILURE
1010
^\[main\.division-by-zero\.\d+\] line 88 division by zero in 10 / 0: FAILURE$
11-
^\[main\.enum-range-check\.\d+\] line 89 enum range check in \(ABC\)10: FAILURE
12-
^\[main\.overflow\.\d+\] line 90 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
13-
^\[main\.overflow\.\d+\] line 91 arithmetic overflow on signed \+ in k \+ 1: FAILURE
11+
^\[main\.enum-range-check\.\d+\] line 89 enum range check in \(ABC\)10: UNKNOWN$
12+
^\[main\.overflow\.\d+\] line 90 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): UNKNOWN$
13+
^\[main\.overflow\.\d+\] line 91 arithmetic overflow on signed \+ in k \+ 1: UNKNOWN$
1414
^VERIFICATION FAILED$
1515
^EXIT=10$
1616
^SIGNAL=0$
1717
--
18-
^\[main\.pointer_primitives\.\d+\] line 41 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
19-
^\[main\.pointer_primitives\.\d+\] line 41 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
20-
^\[main\.pointer_arithmetic\.\d+\] line 42 pointer arithmetic: pointer outside object bounds in p \+ .*2000000000000(l|ll): FAILURE
21-
^\[main\.NaN\.\d+\] line 48 NaN on / in x / den: FAILURE
22-
^\[main\.float-division-by-zero\.\d+\] line 49 floating-point division by zero in x / den: FAILURE
23-
^\[main\.overflow\.\d+\] line 48 arithmetic overflow on floating-point division in x / den: FAILURE
24-
^\[main\.division-by-zero\.\d+\] line 48 division by zero in 10 / 0: FAILURE$
25-
^\[main\.enum-range-check\.\d+\] line 49 enum range check in \(ABC\)10: FAILURE
26-
^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE
27-
^\[main\.overflow\.\d+\] line 51 arithmetic overflow on signed \+ in k \+ 1: FAILURE
18+
^\[main\.pointer_primitives\.\d+\] line 41 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\):
19+
^\[main\.pointer_primitives\.\d+\] line 41 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\):
20+
^\[main\.pointer_arithmetic\.\d+\] line 42 pointer arithmetic: pointer outside object bounds in p \+ .*2000000000000(l|ll):
21+
^\[main\.NaN\.\d+\] line 48 NaN on / in x / den:
22+
^\[main\.float-division-by-zero\.\d+\] line 49 floating-point division by zero in x / den:
23+
^\[main\.overflow\.\d+\] line 48 arithmetic overflow on floating-point division in x / den:
24+
^\[main\.division-by-zero\.\d+\] line 48 division by zero in 10 / 0:
25+
^\[main\.enum-range-check\.\d+\] line 49 enum range check in \(ABC\)10:
26+
^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\):
27+
^\[main\.overflow\.\d+\] line 51 arithmetic overflow on signed \+ in k \+ 1:
2828
--
2929
This test uses all possible named-checks to maximize coverage.

‎regression/symtab2gb/multiple_symtabs/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -7,4 +7,3 @@ user.json_symtab library.json_symtab
77
^\[2\] file library.adb line \d+ assertion: FAILURE$
88
^VERIFICATION FAILED$
99
--
10-
error

‎regression/symtab2gb/single_symtab/test.desc

-1
Original file line numberDiff line numberDiff line change
@@ -7,4 +7,3 @@ entry_point.json_symtab
77
^\[2\] file entry_point.adb line \d+ assertion: SUCCESS$
88
^VERIFICATION FAILED$
99
--
10-
error

‎src/ansi-c/goto_check_c.cpp

+3
Original file line numberDiff line numberDiff line change
@@ -1752,6 +1752,9 @@ void goto_check_ct::add_guarded_property(
17521752
}
17531753
else
17541754
{
1755+
if(property_class == "division-by-zero")
1756+
annotated_location.property_fatal(true);
1757+
17551758
new_code.add(goto_programt::make_assertion(
17561759
std::move(guarded_expr), annotated_location));
17571760
}

‎src/goto-checker/Makefile

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,12 @@
11
SRC = bmc_util.cpp \
22
counterexample_beautification.cpp \
33
cover_goals_report_util.cpp \
4-
incremental_goto_checker.cpp \
4+
fatal_assertions.cpp \
55
goto_symex_fault_localizer.cpp \
66
goto_symex_property_decider.cpp \
77
goto_trace_storage.cpp \
88
goto_verifier.cpp \
9+
incremental_goto_checker.cpp \
910
multi_path_symex_checker.cpp \
1011
multi_path_symex_only_checker.cpp \
1112
properties.cpp \

‎src/goto-checker/all_properties_verifier_with_trace_storage.h

+5-2
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,10 @@ Author: Daniel Kroening, Peter Schrammel
1212
#ifndef CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_TRACE_STORAGE_H
1313
#define CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_WITH_TRACE_STORAGE_H
1414

15-
#include "goto_verifier.h"
16-
1715
#include "bmc_util.h"
16+
#include "fatal_assertions.h"
1817
#include "goto_trace_storage.h"
18+
#include "goto_verifier.h"
1919
#include "incremental_goto_checker.h"
2020
#include "properties.h"
2121
#include "report_util.h"
@@ -62,6 +62,9 @@ class all_properties_verifier_with_trace_storaget : public goto_verifiert
6262
++iterations;
6363
}
6464

65+
propagate_fatal_assertions(
66+
properties, traces, goto_model.get_goto_functions());
67+
6568
return determine_result(properties);
6669
}
6770

‎src/goto-checker/fatal_assertions.cpp

+219
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,219 @@
1+
/*******************************************************************\
2+
3+
Module: Fatal Assertions
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Fatal Assertions
11+
12+
#include "fatal_assertions.h"
13+
14+
#include <util/irep_hash.h>
15+
16+
#include <goto-programs/goto_functions.h>
17+
18+
#include "goto_trace_storage.h"
19+
20+
#include <stack>
21+
#include <unordered_set>
22+
23+
struct function_loc_pairt
24+
{
25+
using function_itt = goto_functionst::function_mapt::const_iterator;
26+
function_loc_pairt(
27+
function_itt __function_it,
28+
goto_programt::const_targett __target)
29+
: function_it(__function_it), target(__target)
30+
{
31+
}
32+
function_itt function_it;
33+
goto_programt::const_targett target;
34+
bool operator==(const function_loc_pairt &other) const
35+
{
36+
return function_it->first == other.function_it->first &&
37+
target == other.target;
38+
}
39+
};
40+
41+
struct function_itt_hasht
42+
{
43+
using function_itt = goto_functionst::function_mapt::const_iterator;
44+
std::size_t operator()(const function_itt &function_it) const
45+
{
46+
return function_it->first.hash();
47+
}
48+
};
49+
50+
struct function_loc_pair_hasht
51+
{
52+
std::size_t operator()(const function_loc_pairt &p) const
53+
{
54+
auto h1 = p.function_it->first.hash();
55+
auto h2 = const_target_hash{}(p.target);
56+
return hash_combine(h1, h2);
57+
}
58+
};
59+
60+
using loc_sett =
61+
std::unordered_set<function_loc_pairt, function_loc_pair_hasht>;
62+
63+
static loc_sett
64+
reachable_fixpoint(const loc_sett &locs, const goto_functionst &goto_functions)
65+
{
66+
// frontier set
67+
std::stack<function_loc_pairt> working;
68+
69+
for(auto loc : locs)
70+
working.push(loc);
71+
72+
loc_sett fixpoint;
73+
74+
while(!working.empty())
75+
{
76+
auto loc = working.top();
77+
working.pop();
78+
79+
auto insertion_result = fixpoint.insert(loc);
80+
if(!insertion_result.second)
81+
continue; // seen already
82+
83+
if(loc.target->is_function_call())
84+
{
85+
// get the callee
86+
auto &function = loc.target->call_function();
87+
if(function.id() == ID_symbol)
88+
{
89+
// add the callee to the working set
90+
auto &function_identifier = to_symbol_expr(function).get_identifier();
91+
auto function_iterator =
92+
goto_functions.function_map.find(function_identifier);
93+
CHECK_RETURN(function_iterator != goto_functions.function_map.end());
94+
working.emplace(
95+
function_iterator,
96+
function_iterator->second.body.instructions.begin());
97+
}
98+
99+
// add the next location to the working set
100+
working.emplace(loc.function_it, std::next(loc.target));
101+
}
102+
else
103+
{
104+
auto &body = loc.function_it->second.body;
105+
106+
for(auto successor : body.get_successors(loc.target))
107+
working.emplace(loc.function_it, successor);
108+
}
109+
}
110+
111+
return fixpoint;
112+
}
113+
114+
/// Proven assertions after refuted fatal assertions
115+
/// are marked as UNKNOWN.
116+
void propagate_fatal_to_proven(
117+
propertiest &properties,
118+
const goto_functionst &goto_functions)
119+
{
120+
// Iterate to find refuted fatal assertions. Anything reachalble
121+
// from there is a 'fatal loc'.
122+
loc_sett fatal_locs;
123+
124+
for(auto function_it = goto_functions.function_map.begin();
125+
function_it != goto_functions.function_map.end();
126+
function_it++)
127+
{
128+
auto &body = function_it->second.body;
129+
for(auto target = body.instructions.begin();
130+
target != body.instructions.end();
131+
target++)
132+
{
133+
if(target->is_assert() && target->source_location().property_fatal())
134+
{
135+
auto id = target->source_location().get_property_id();
136+
auto property = properties.find(id);
137+
CHECK_RETURN(property != properties.end());
138+
139+
// Status?
140+
if(property->second.status == property_statust::FAIL)
141+
{
142+
fatal_locs.emplace(function_it, target);
143+
}
144+
}
145+
}
146+
}
147+
148+
// Saturate fixpoint.
149+
auto fixpoint = reachable_fixpoint(fatal_locs, goto_functions);
150+
151+
// Now mark PASS assertions as UNKNOWN.
152+
for(auto &loc : fixpoint)
153+
{
154+
if(loc.target->is_assert())
155+
{
156+
auto id = loc.target->source_location().get_property_id();
157+
auto property = properties.find(id);
158+
CHECK_RETURN(property != properties.end());
159+
160+
// Status?
161+
if(property->second.status == property_statust::PASS)
162+
{
163+
property->second.status = property_statust::UNKNOWN;
164+
}
165+
}
166+
}
167+
}
168+
169+
bool passes_through_refuted_fatal(
170+
goto_programt::const_targett assertion,
171+
const goto_tracet &trace,
172+
const propertiest &properties)
173+
{
174+
for(auto &step : trace.steps)
175+
{
176+
// Ignore the assertion itself.
177+
if(step.pc->location_number == assertion->location_number)
178+
continue;
179+
180+
if(
181+
step.is_assert() && step.pc->source_location().property_fatal() &&
182+
step.cond_value == false)
183+
{
184+
return true;
185+
}
186+
}
187+
188+
return false;
189+
}
190+
191+
/// Refuted assertions are marked as UNKNOWN iff their
192+
/// counterexample passes through a non-proven fatal assertion.
193+
void propagate_fatal_to_refuted(
194+
propertiest &properties,
195+
const goto_trace_storaget &goto_trace_storage)
196+
{
197+
for(auto &property : properties)
198+
{
199+
// Status?
200+
if(property.second.status == property_statust::FAIL)
201+
{
202+
auto &trace = goto_trace_storage[property.first];
203+
if(passes_through_refuted_fatal(property.second.pc, trace, properties))
204+
{
205+
// mark as 'UNKNOWN'
206+
property.second.status = property_statust::UNKNOWN;
207+
}
208+
}
209+
}
210+
}
211+
212+
void propagate_fatal_assertions(
213+
propertiest &properties,
214+
const goto_trace_storaget &goto_trace_storage,
215+
const goto_functionst &goto_functions)
216+
{
217+
propagate_fatal_to_proven(properties, goto_functions);
218+
propagate_fatal_to_refuted(properties, goto_trace_storage);
219+
}

‎src/goto-checker/fatal_assertions.h

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
/*******************************************************************\
2+
3+
Module: Fatal Assertions
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Fatal Assertions
11+
12+
#ifndef CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H
13+
#define CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H
14+
15+
#include "properties.h"
16+
17+
class goto_functionst;
18+
class goto_trace_storaget;
19+
20+
/// This has two effects.
21+
/// 1. Proven assertions after refuted fatal assertions
22+
/// are marked as UNKNOWN.
23+
/// 2. Refuted assertions are marked as UNKNOWN iff their
24+
/// counterexample trace passes through a non-proven fatal assertion.
25+
void propagate_fatal_assertions(
26+
propertiest &,
27+
const goto_trace_storaget &,
28+
const goto_functionst &);
29+
30+
#endif // CPROVER_GOTO_CHECKER_FATAL_ASSERTIONS_H

‎src/util/irep_ids.def

+1
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ IREP_ID_ONE(line)
2626
IREP_ID_ONE(column)
2727
IREP_ID_ONE(comment)
2828
IREP_ID_ONE(property_class)
29+
IREP_ID_ONE(property_fatal)
2930
IREP_ID_ONE(property_id)
3031
IREP_ID_ONE(function)
3132
IREP_ID_ONE(mathematical_function)

0 commit comments

Comments
 (0)