Skip to content

Commit 65d06a0

Browse files
smowtonsmowton
committed
Add local-safe-pointers analysis
This approaches the safe-pointers problem from the opposite direction compared to local- bitvector-analysis -- local-bitvector tries to establish a pointer is safe because it definitely points to known object, whereas local-safe-pointers tries to establish a particular usage is certainly safe because it is trivially dominated by a not-null test, which at present means a conditional GOTO or an ASSUME.
1 parent f3a3e79 commit 65d06a0

File tree

7 files changed

+415
-1
lines changed

7 files changed

+415
-1
lines changed

‎regression/goto-instrument/safe-dereferences/main.c

+71
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
static void noop() { }
2+
3+
int main(int argc, char **argv) {
4+
5+
int x;
6+
7+
// Should work (guarded by assume):
8+
int *ptr1 = &x;
9+
__CPROVER_assume(ptr1 != 0);
10+
int deref1 = *ptr1;
11+
12+
// Should work (guarded by else):
13+
int *ptr2 = &x;
14+
if(ptr2 == 0)
15+
{
16+
}
17+
else
18+
{
19+
int deref2 = *ptr2;
20+
}
21+
22+
// Should work (guarded by if):
23+
int *ptr3 = &x;
24+
if(ptr3 != 0)
25+
{
26+
int deref3 = *ptr3;
27+
}
28+
29+
// Shouldn't work yet despite being safe (guarded by backward goto):
30+
int *ptr4 = &x;
31+
goto check;
32+
33+
deref:
34+
int deref4 = *ptr4;
35+
goto end_test4;
36+
37+
check:
38+
__CPROVER_assume(ptr4 != 0);
39+
goto deref;
40+
41+
end_test4:
42+
43+
// Shouldn't work yet despite being safe (guarded by confluence):
44+
int *ptr5 = &x;
45+
if(argc == 5)
46+
__CPROVER_assume(ptr5 != 0);
47+
else
48+
__CPROVER_assume(ptr5 != 0);
49+
int deref5 = *ptr5;
50+
51+
// Shouldn't work (unsafe as only guarded on one branch):
52+
int *ptr6 = &x;
53+
if(argc == 6)
54+
__CPROVER_assume(ptr6 != 0);
55+
else
56+
{
57+
}
58+
int deref6 = *ptr6;
59+
60+
// Shouldn't work due to suspicion *ptr6 might alter ptr7:
61+
int *ptr7 = &x;
62+
__CPROVER_assume(ptr7 != 0);
63+
ptr6 = 0;
64+
int deref7 = *ptr7;
65+
66+
// Shouldn't work due to suspicion noop() call might alter ptr8:
67+
int *ptr8 = &x;
68+
__CPROVER_assume(ptr8 != 0);
69+
noop();
70+
int deref8 = *ptr8;
71+
}

‎regression/goto-instrument/safe-dereferences/test.desc

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--show-safe-dereferences
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
Safe \(known-not-null\) dereferences: \{main::[0-9]+::ptr1\}
7+
Safe \(known-not-null\) dereferences: \{main::[0-9]+::ptr2\}
8+
Safe \(known-not-null\) dereferences: \{main::[0-9]+::ptr3\}
9+
--
10+
Safe \(known-not-null\) dereferences: \{main::[0-9]+::ptr[4-8]\}
11+
^warning: ignoring
12+
--
13+
See comments in main.c for details about what each ptr variable is testing, and why they
14+
should or shouldn't be seen as safe accesses.

‎src/analyses/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ SRC = ai.cpp \
2020
local_bitvector_analysis.cpp \
2121
local_cfg.cpp \
2222
local_may_alias.cpp \
23+
local_safe_pointers.cpp \
2324
locals.cpp \
2425
natural_loops.cpp \
2526
reaching_definitions.cpp \

‎src/analyses/local_safe_pointers.cpp

+238
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,238 @@
1+
/*******************************************************************\
2+
3+
Module: Local safe pointer analysis
4+
5+
Author: Diffblue Ltd
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Local safe pointer analysis
11+
12+
#include "local_safe_pointers.h"
13+
14+
#include <util/expr_iterator.h>
15+
#include <util/format_expr.h>
16+
17+
/// If `expr` is of the form `x != nullptr`, return x. Otherwise return null
18+
static const exprt *get_null_checked_expr(const exprt &expr)
19+
{
20+
if(expr.id() == ID_notequal)
21+
{
22+
const exprt *op0 = &expr.op0(), *op1 = &expr.op1();
23+
if(op0->type().id() == ID_pointer &&
24+
*op0 == null_pointer_exprt(to_pointer_type(op0->type())))
25+
{
26+
std::swap(op0, op1);
27+
}
28+
29+
if(op1->type().id() == ID_pointer &&
30+
*op1 == null_pointer_exprt(to_pointer_type(op1->type())))
31+
{
32+
while(op0->id() == ID_typecast)
33+
op0 = &op0->op0();
34+
return op0;
35+
}
36+
}
37+
38+
return nullptr;
39+
}
40+
41+
/// Return structure for `get_conditional_checked_expr`
42+
struct goto_null_checkt
43+
{
44+
/// If true, the given GOTO tests that a pointer expression is non-null on the
45+
/// taken branch; otherwise, on the not-taken branch.
46+
bool checked_when_taken;
47+
48+
/// Null-tested pointer expression
49+
exprt checked_expr;
50+
};
51+
52+
/// Check if a GOTO guard expression tests if a pointer is null
53+
/// \param goto_guard: expression to check
54+
/// \return a `goto_null_checkt` indicating what expression is tested and
55+
/// whether the check applies on the taken or not-taken branch, or an empty
56+
/// optionalt if this isn't a null check.
57+
static optionalt<goto_null_checkt>
58+
get_conditional_checked_expr(const exprt &goto_guard)
59+
{
60+
exprt normalized_guard = goto_guard;
61+
bool checked_when_taken = true;
62+
while(normalized_guard.id() == ID_not || normalized_guard.id() == ID_equal)
63+
{
64+
if(normalized_guard.id() == ID_not)
65+
normalized_guard = normalized_guard.op0();
66+
else
67+
normalized_guard.id(ID_notequal);
68+
checked_when_taken = !checked_when_taken;
69+
}
70+
71+
const exprt *checked_expr = get_null_checked_expr(normalized_guard);
72+
if(!checked_expr)
73+
return {};
74+
else
75+
return goto_null_checkt { checked_when_taken, *checked_expr };
76+
}
77+
78+
/// Compute safe dereference expressions for a given GOTO program. This
79+
/// populates `non_null_expressions` mapping instruction location numbers
80+
/// onto a set of expressions that are known to be non-null BEFORE that
81+
/// instruction is executed.
82+
/// \param goto_program: program to analyse
83+
void local_safe_pointerst::operator()(const goto_programt &goto_program)
84+
{
85+
std::set<exprt> checked_expressions;
86+
87+
for(const auto &instruction : goto_program.instructions)
88+
{
89+
// Handle control-flow convergence pessimistically:
90+
if(instruction.incoming_edges.size() > 1)
91+
checked_expressions.clear();
92+
// Retrieve working set for forward GOTOs:
93+
else if(instruction.is_target())
94+
checked_expressions = non_null_expressions[instruction.location_number];
95+
96+
// Save the working set at this program point:
97+
if(!checked_expressions.empty())
98+
non_null_expressions[instruction.location_number] = checked_expressions;
99+
100+
switch(instruction.type)
101+
{
102+
// Instruction types that definitely don't write anything, and therefore
103+
// can't store a null pointer:
104+
case DECL:
105+
case DEAD:
106+
case ASSERT:
107+
case SKIP:
108+
case LOCATION:
109+
case RETURN:
110+
case THROW:
111+
case CATCH:
112+
break;
113+
114+
// Possible checks:
115+
case ASSUME:
116+
{
117+
const exprt *checked_expr;
118+
if((checked_expr = get_null_checked_expr(instruction.guard)) != nullptr)
119+
{
120+
checked_expressions.insert(*checked_expr);
121+
}
122+
break;
123+
}
124+
125+
case GOTO:
126+
if(!instruction.is_backwards_goto())
127+
{
128+
if(auto conditional_check =
129+
get_conditional_checked_expr(instruction.guard))
130+
{
131+
auto &taken_checked_expressions =
132+
non_null_expressions[instruction.get_target()->location_number];
133+
taken_checked_expressions = checked_expressions;
134+
135+
if(conditional_check->checked_when_taken)
136+
taken_checked_expressions.insert(conditional_check->checked_expr);
137+
else
138+
checked_expressions.insert(conditional_check->checked_expr);
139+
140+
break;
141+
}
142+
// Otherwise fall through to...
143+
}
144+
145+
default:
146+
// Pessimistically assume all other instructions might overwrite any
147+
// pointer with a possibly-null value.
148+
checked_expressions.clear();
149+
break;
150+
}
151+
}
152+
}
153+
154+
/// Output non-null expressions per instruction in human-readable format
155+
/// \param out: stream to write output to
156+
/// \param goto_program: GOTO program analysed (the same one passed to
157+
/// operator())
158+
/// \param ns: global namespace
159+
void local_safe_pointerst::output(
160+
std::ostream &out, const goto_programt &goto_program, const namespacet &ns)
161+
{
162+
forall_goto_program_instructions(i_it, goto_program)
163+
{
164+
out << "**** " << i_it->location_number << " "
165+
<< i_it->source_location << "\n";
166+
167+
out << "Non-null expressions: ";
168+
169+
auto findit = non_null_expressions.find(i_it->location_number);
170+
if(findit == non_null_expressions.end())
171+
out << "{}";
172+
else
173+
{
174+
out << "{";
175+
bool first = true;
176+
for(const exprt &expr : findit->second)
177+
{
178+
if(!first)
179+
out << ", ";
180+
first = true;
181+
format_rec(out, expr);
182+
}
183+
out << "}";
184+
}
185+
186+
out << '\n';
187+
goto_program.output_instruction(ns, "", out, *i_it);
188+
out << '\n';
189+
}
190+
}
191+
192+
/// Output safely dereferenced expressions per instruction in human-readable
193+
/// format. For example, if we have an instruction `ASSUME x->y->z == a->b`
194+
/// and we know expressions `x->y`, `a` and `other` are not null prior to it,
195+
/// this will print `{x->y, a}`, the intersection of the `dereference_exprt`s
196+
/// used here and the known-not-null expressions.
197+
/// \param out: stream to write output to
198+
/// \param goto_program: GOTO program analysed (the same one passed to
199+
/// operator())
200+
/// \param ns: global namespace
201+
void local_safe_pointerst::output_safe_dereferences(
202+
std::ostream &out, const goto_programt &goto_program, const namespacet &ns)
203+
{
204+
forall_goto_program_instructions(i_it, goto_program)
205+
{
206+
out << "**** " << i_it->location_number << " "
207+
<< i_it->source_location << "\n";
208+
209+
out << "Safe (known-not-null) dereferences: ";
210+
211+
auto findit = non_null_expressions.find(i_it->location_number);
212+
if(findit == non_null_expressions.end())
213+
out << "{}";
214+
else
215+
{
216+
out << "{";
217+
bool first = true;
218+
for(auto subexpr_it = i_it->code.depth_begin(),
219+
subexpr_end = i_it->code.depth_end();
220+
subexpr_it != subexpr_end;
221+
++subexpr_it)
222+
{
223+
if(subexpr_it->id() == ID_dereference)
224+
{
225+
if(!first)
226+
out << ", ";
227+
first = true;
228+
format_rec(out, subexpr_it->op0());
229+
}
230+
}
231+
out << "}";
232+
}
233+
234+
out << '\n';
235+
goto_program.output_instruction(ns, "", out, *i_it);
236+
out << '\n';
237+
}
238+
}

‎src/analyses/local_safe_pointers.h

+57
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
/*******************************************************************\
2+
3+
Module: Local safe pointer analysis
4+
5+
Author: Diffblue Ltd
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Local safe pointer analysis
11+
12+
#ifndef CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H
13+
#define CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H
14+
15+
#include <goto-programs/goto_program.h>
16+
#include <util/std_expr.h>
17+
18+
/// A very simple, cheap analysis to determine when dereference operations are
19+
/// trivially guarded by a check against a null pointer access.
20+
/// In the interests of a very cheap analysis we only search for very local
21+
/// guards -- at the moment only `if(x != null) { *x }`
22+
/// and `assume(x != null); *x` are handled. Control-flow convergence and
23+
/// possibly-alising operations are handled pessimistically.
24+
class local_safe_pointerst
25+
{
26+
std::map<unsigned, std::set<exprt>> non_null_expressions;
27+
28+
public:
29+
void operator()(const goto_programt &goto_program);
30+
31+
bool is_non_null_at_program_point(
32+
const exprt &expr, goto_programt::const_targett program_point)
33+
{
34+
auto findit = non_null_expressions.find(program_point->location_number);
35+
if(findit == non_null_expressions.end())
36+
return false;
37+
const exprt *tocheck = &expr;
38+
while(tocheck->id() == ID_typecast)
39+
tocheck = &tocheck->op0();
40+
return findit->second.count(*tocheck) != 0;
41+
}
42+
43+
bool is_safe_dereference(
44+
const dereference_exprt &deref,
45+
goto_programt::const_targett program_point)
46+
{
47+
return is_non_null_at_program_point(deref.op0(), program_point);
48+
}
49+
50+
void output(
51+
std::ostream &stream, const goto_programt &program, const namespacet &ns);
52+
53+
void output_safe_dereferences(
54+
std::ostream &stream, const goto_programt &program, const namespacet &ns);
55+
};
56+
57+
#endif // CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H

0 commit comments

Comments
 (0)