Skip to content

Commit f0f7dbf

Browse files
author
martin
committed
Refactor goto-analyzer --verify with multiple histories
1 parent 8acd199 commit f0f7dbf

File tree

1 file changed

+131
-124
lines changed

1 file changed

+131
-124
lines changed

‎src/goto-analyzer/static_verifier.cpp

Lines changed: 131 additions & 124 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,122 @@ check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
5252
UNREACHABLE;
5353
}
5454

55+
static static_verifier_resultt check_assertion(
56+
const ai_baset &ai,
57+
goto_programt::const_targett assert_location,
58+
irep_idt function_id,
59+
const namespacet &ns)
60+
{
61+
static_verifier_resultt result;
62+
63+
PRECONDITION(assert_location->is_assert());
64+
exprt e(assert_location->get_condition());
65+
66+
// If there are multiple, distinct histories that reach the same location
67+
// we can get better results by checking with each individually rather
68+
// than merging all of them and doing one check.
69+
const auto trace_set_pointer = ai.abstract_traces_before(
70+
assert_location); // Keep a pointer so refcount > 0
71+
const auto &trace_set = *trace_set_pointer;
72+
73+
if(trace_set.size() == 0) // i.e. unreachable
74+
{
75+
result.status = static_verifier_resultt::BOTTOM;
76+
}
77+
else if(trace_set.size() == 1)
78+
{
79+
auto dp = ai.abstract_state_before(assert_location);
80+
81+
result.status = check_assertion(*dp, e, ns);
82+
}
83+
else
84+
{
85+
// Multiple traces, verify against each one
86+
std::size_t unreachable_traces = 0;
87+
std::size_t true_traces = 0;
88+
std::size_t false_traces = 0;
89+
std::size_t unknown_traces = 0;
90+
91+
for(const auto &trace_ptr : trace_set)
92+
{
93+
auto dp = ai.abstract_state_before(trace_ptr);
94+
95+
result.status = check_assertion(*dp, e, ns);
96+
switch(result.status)
97+
{
98+
case static_verifier_resultt::BOTTOM:
99+
++unreachable_traces;
100+
break;
101+
case static_verifier_resultt::TRUE:
102+
++true_traces;
103+
break;
104+
case static_verifier_resultt::FALSE:
105+
++false_traces;
106+
break;
107+
case static_verifier_resultt::UNKNOWN:
108+
++unknown_traces;
109+
break;
110+
default:
111+
UNREACHABLE;
112+
}
113+
}
114+
115+
// Join the results
116+
if(unknown_traces != 0)
117+
{
118+
// If any trace is unknown, the final result must be unknown
119+
result.status = static_verifier_resultt::UNKNOWN;
120+
}
121+
else
122+
{
123+
if(false_traces == 0)
124+
{
125+
// Definitely true; the only question is how
126+
if(true_traces == 0)
127+
{
128+
// Definitely not reachable
129+
INVARIANT(
130+
unreachable_traces == trace_set.size(),
131+
"All traces must not reach the assertion");
132+
result.status = static_verifier_resultt::BOTTOM;
133+
}
134+
else
135+
{
136+
// At least one trace (may) reach it.
137+
// All traces that reach it are safe.
138+
result.status = static_verifier_resultt::TRUE;
139+
}
140+
}
141+
else
142+
{
143+
// At lease one trace (may) reach it and it is false on that trace
144+
if(true_traces == 0)
145+
{
146+
// All traces that (may) reach it are false
147+
result.status = static_verifier_resultt::FALSE;
148+
}
149+
else
150+
{
151+
// The awkward case, there are traces that (may) reach it and
152+
// some are true, some are false. It is not entirely fair to say
153+
// "FAILURE (if reachable)" because it's a bit more complex than
154+
// that, "FAILURE (if reachable via a particular trace)" would be
155+
// more accurate summary of what we know at this point.
156+
// Given that all results of FAILURE from this analysis are
157+
// caveated with some reachability questions, the following is not
158+
// entirely unreasonable.
159+
result.status = static_verifier_resultt::FALSE;
160+
}
161+
}
162+
}
163+
}
164+
165+
result.source_location = assert_location->source_location;
166+
result.function_id = function_id;
167+
168+
return result;
169+
}
170+
55171
void static_verifier(
56172
const abstract_goto_modelt &abstract_goto_model,
57173
const ai_baset &ai,
@@ -286,134 +402,25 @@ bool static_verifier(
286402
if(!i_it->is_assert())
287403
continue;
288404

289-
exprt e(i_it->get_condition());
290-
291-
results.push_back(static_verifier_resultt());
292-
auto &result = results.back();
405+
results.push_back(check_assertion(ai, i_it, f.first, ns));
293406

294-
// If there are multiple, distinct histories that reach the same location
295-
// we can get better results by checking with each individually rather
296-
// than merging all of them and doing one check.
297-
const auto trace_set_pointer =
298-
ai.abstract_traces_before(i_it); // Keep a pointer so refcount > 0
299-
const auto &trace_set = *trace_set_pointer;
300-
301-
if(trace_set.size() == 0) // i.e. unreachable
407+
switch(results.back().status)
302408
{
303-
result.status = static_verifier_resultt::BOTTOM;
409+
case static_verifier_resultt::BOTTOM:
304410
++pass;
411+
break;
412+
case static_verifier_resultt::TRUE:
413+
++pass;
414+
break;
415+
case static_verifier_resultt::FALSE:
416+
++fail;
417+
break;
418+
case static_verifier_resultt::UNKNOWN:
419+
++unknown;
420+
break;
421+
default:
422+
UNREACHABLE;
305423
}
306-
else if(trace_set.size() == 1)
307-
{
308-
auto dp = ai.abstract_state_before(i_it);
309-
310-
result.status = check_assertion(*dp, e, ns);
311-
switch(result.status)
312-
{
313-
case static_verifier_resultt::BOTTOM:
314-
++pass;
315-
break;
316-
case static_verifier_resultt::TRUE:
317-
++pass;
318-
break;
319-
case static_verifier_resultt::FALSE:
320-
++fail;
321-
break;
322-
case static_verifier_resultt::UNKNOWN:
323-
++unknown;
324-
break;
325-
default:
326-
UNREACHABLE;
327-
}
328-
}
329-
else
330-
{
331-
// Multiple traces, verify against each one
332-
std::size_t unreachable_traces = 0;
333-
std::size_t true_traces = 0;
334-
std::size_t false_traces = 0;
335-
std::size_t unknown_traces = 0;
336-
337-
for(const auto &trace_ptr : trace_set)
338-
{
339-
auto dp = ai.abstract_state_before(trace_ptr);
340-
341-
result.status = check_assertion(*dp, e, ns);
342-
switch(result.status)
343-
{
344-
case static_verifier_resultt::BOTTOM:
345-
++unreachable_traces;
346-
break;
347-
case static_verifier_resultt::TRUE:
348-
++true_traces;
349-
break;
350-
case static_verifier_resultt::FALSE:
351-
++false_traces;
352-
break;
353-
case static_verifier_resultt::UNKNOWN:
354-
++unknown_traces;
355-
break;
356-
default:
357-
UNREACHABLE;
358-
}
359-
}
360-
361-
// Join the results
362-
if(unknown_traces != 0)
363-
{
364-
// If any trace is unknown, the final result must be unknown
365-
result.status = static_verifier_resultt::UNKNOWN;
366-
++unknown;
367-
}
368-
else
369-
{
370-
if(false_traces == 0)
371-
{
372-
// Definitely true; the only question is how
373-
++pass;
374-
if(true_traces == 0)
375-
{
376-
// Definitely not reachable
377-
INVARIANT(
378-
unreachable_traces == trace_set.size(),
379-
"All traces must not reach the assertion");
380-
result.status = static_verifier_resultt::BOTTOM;
381-
}
382-
else
383-
{
384-
// At least one trace (may) reach it.
385-
// All traces that reach it are safe.
386-
result.status = static_verifier_resultt::TRUE;
387-
}
388-
}
389-
else
390-
{
391-
// At lease one trace (may) reach it and it is false on that trace
392-
if(true_traces == 0)
393-
{
394-
// All traces that (may) reach it are false
395-
++fail;
396-
result.status = static_verifier_resultt::FALSE;
397-
}
398-
else
399-
{
400-
// The awkward case, there are traces that (may) reach it and
401-
// some are true, some are false. It is not entirely fair to say
402-
// "FAILURE (if reachable)" because it's a bit more complex than
403-
// that, "FAILURE (if reachable via a particular trace)" would be
404-
// more accurate summary of what we know at this point.
405-
// Given that all results of FAILURE from this analysis are
406-
// caveated with some reachability questions, the following is not
407-
// entirely unreasonable.
408-
++fail;
409-
result.status = static_verifier_resultt::FALSE;
410-
}
411-
}
412-
}
413-
}
414-
415-
result.source_location = i_it->source_location;
416-
result.function_id = f.first;
417424
}
418425
}
419426

0 commit comments

Comments
 (0)