Skip to content

Always check Java pointers for null before deref #737

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Apr 4, 2017
Merged

Always check Java pointers for null before deref #737

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ee3c39a
Always check Java pointers for null before deref
smowton Mar 30, 2017
eb20cdf
Amend tests perturbed by adding null pointer checks
smowton Mar 31, 2017
f9cd371
Document change to pointer-check option
smowton Mar 31, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion regression/cbmc-java/exceptions1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ test.class
^EXIT=10$
^SIGNAL=0$
^.*assertion at file test.java line 26 function.*: FAILURE$
\*\* 1 of 9 failed \(2 iterations\)$
\*\* 1 of [0-9]* failed \(2 iterations\)$
^VERIFICATION FAILED$
--
^warning: ignoring
2 changes: 1 addition & 1 deletion regression/cbmc-java/exceptions2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ test.class
^EXIT=10$
^SIGNAL=0$
^.*assertion at file test.java line 15 function.*: FAILURE$
^\*\* 1 of 5 failed \(2 iterations\)$
^\*\* 1 of [0-9]* failed \(2 iterations\)$
^VERIFICATION FAILED$
--
^warning: ignoring
Binary file modified regression/cbmc-java/lazyloading3/A.class
View file
Open in desktop
Binary file not shown.
Binary file modified regression/cbmc-java/lazyloading3/B.class
View file
Open in desktop
Binary file not shown.
Binary file modified regression/cbmc-java/lazyloading3/C.class
View file
Open in desktop
Binary file not shown.
Binary file modified regression/cbmc-java/lazyloading3/D.class
View file
Open in desktop
Binary file not shown.
Binary file modified regression/cbmc-java/lazyloading3/test.class
View file
Open in desktop
Binary file not shown.
2 changes: 2 additions & 0 deletions regression/cbmc-java/lazyloading3/test.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@ public class test
{
public static void main(C c)
{
if(c==null)
return;
c.a.f();
}
}
Expand Down
92 changes: 45 additions & 47 deletions src/analyses/goto_check.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,17 +62,19 @@ class goto_checkt

typedef goto_functionst::goto_functiont goto_functiont;

void goto_check(goto_functiont &goto_function);

irep_idt mode;
void goto_check(goto_functiont &goto_function, const irep_idt &mode);

protected:
const namespacet &ns;
local_bitvector_analysist *local_bitvector_analysis;
goto_programt::const_targett t;

void check_rec(const exprt &expr, guardt &guard, bool address);
void check(const exprt &expr);
void check_rec(
const exprt &expr,
guardt &guard,
bool address,
const irep_idt &mode);
void check(const exprt &expr, const irep_idt &mode);

void bounds_check(const index_exprt &expr, const guardt &guard);
void div_by_zero_check(const div_exprt &expr, const guardt &guard);
Expand All @@ -84,7 +86,8 @@ class goto_checkt
const dereference_exprt &expr,
const guardt &guard,
const exprt &access_lb,
const exprt &access_ub);
const exprt &access_ub,
const irep_idt &mode);
void integer_overflow_check(const exprt &expr, const guardt &guard);
void conversion_check(const exprt &expr, const guardt &guard);
void float_overflow_check(const exprt &expr, const guardt &guard);
Expand Down Expand Up @@ -993,9 +996,10 @@ void goto_checkt::pointer_validity_check(
const dereference_exprt &expr,
const guardt &guard,
const exprt &access_lb,
const exprt &access_ub)
const exprt &access_ub,
const irep_idt &mode)
{
if(!enable_pointer_check)
if(mode!=ID_java && !enable_pointer_check)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So we would always be doing this for mode==ID_java, whether it's enabled or not!?

Copy link
Contributor Author

@smowton smowton Mar 30, 2017 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes. Check-deref'd-pointer-not-null is mandatory for Java. Explicit enable is only then meaningful for C/C++/etc.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But we should then be generating an exception, not an assertion, shouldn't we?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ideally yes. However this matches current Java front-end behaviour for out of bounds array access and similar. I think we should support this simple model and then perhaps in the future add support for a "full fidelity" model where we support catching NPE, AOOBE and so on.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok; I'd thus suggestion that the help output for --pointer-check be amended to say "C/C++ only".

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done

return;

const exprt &pointer=expr.op0();
Expand Down Expand Up @@ -1373,7 +1377,8 @@ Function: goto_checkt::check_rec
void goto_checkt::check_rec(
const exprt &expr,
guardt &guard,
bool address)
bool address,
const irep_idt &mode)
{
// we don't look into quantifiers
if(expr.id()==ID_exists || expr.id()==ID_forall)
Expand All @@ -1384,26 +1389,26 @@ void goto_checkt::check_rec(
if(expr.id()==ID_dereference)
{
assert(expr.operands().size()==1);
check_rec(expr.op0(), guard, false);
check_rec(expr.op0(), guard, false, mode);
}
else if(expr.id()==ID_index)
{
assert(expr.operands().size()==2);
check_rec(expr.op0(), guard, true);
check_rec(expr.op1(), guard, false);
check_rec(expr.op0(), guard, true, mode);
check_rec(expr.op1(), guard, false, mode);
}
else
{
forall_operands(it, expr)
check_rec(*it, guard, true);
check_rec(*it, guard, true, mode);
}
return;
}

if(expr.id()==ID_address_of)
{
assert(expr.operands().size()==1);
check_rec(expr.op0(), guard, true);
check_rec(expr.op0(), guard, true, mode);
return;
}
else if(expr.id()==ID_and || expr.id()==ID_or)
Expand All @@ -1420,7 +1425,7 @@ void goto_checkt::check_rec(
throw "`"+expr.id_string()+"' takes Boolean operands only, but got "+
op.pretty();

check_rec(op, guard, false);
check_rec(op, guard, false, mode);

if(expr.id()==ID_or)
guard.add(not_exprt(op));
Expand All @@ -1445,19 +1450,19 @@ void goto_checkt::check_rec(
throw msg;
}

check_rec(expr.op0(), guard, false);
check_rec(expr.op0(), guard, false, mode);

{
guardt old_guard=guard;
guard.add(expr.op0());
check_rec(expr.op1(), guard, false);
check_rec(expr.op1(), guard, false, mode);
guard.swap(old_guard);
}

{
guardt old_guard=guard;
guard.add(not_exprt(expr.op0()));
check_rec(expr.op2(), guard, false);
check_rec(expr.op2(), guard, false, mode);
guard.swap(old_guard);
}

Expand All @@ -1470,7 +1475,7 @@ void goto_checkt::check_rec(
const dereference_exprt &deref=
to_dereference_expr(member.struct_op());

check_rec(deref.op0(), guard, false);
check_rec(deref.op0(), guard, false, mode);

exprt access_ub=nil_exprt();

Expand All @@ -1480,13 +1485,13 @@ void goto_checkt::check_rec(
if(member_offset.is_not_nil() && size.is_not_nil())
access_ub=plus_exprt(member_offset, size);

pointer_validity_check(deref, guard, member_offset, access_ub);
pointer_validity_check(deref, guard, member_offset, access_ub, mode);

return;
}

forall_operands(it, expr)
check_rec(*it, guard, false);
check_rec(*it, guard, false, mode);

if(expr.id()==ID_index)
{
Expand Down Expand Up @@ -1545,7 +1550,8 @@ void goto_checkt::check_rec(
to_dereference_expr(expr),
guard,
nil_exprt(),
size_of_expr(expr.type(), ns));
size_of_expr(expr.type(), ns),
mode);
}

/*******************************************************************\
Expand All @@ -1560,10 +1566,10 @@ Function: goto_checkt::check

\*******************************************************************/

void goto_checkt::check(const exprt &expr)
void goto_checkt::check(const exprt &expr, const irep_idt &mode)
{
guardt guard;
check_rec(expr, guard, false);
check_rec(expr, guard, false, mode);
}

/*******************************************************************\
Expand All @@ -1574,18 +1580,14 @@ Function: goto_checkt::goto_check

Outputs:

Purpose:[B
Purpose:

\*******************************************************************/

void goto_checkt::goto_check(goto_functiont &goto_function)
void goto_checkt::goto_check(
goto_functiont &goto_function,
const irep_idt &mode)
{
{
const symbolt *init_symbol;
if(!ns.lookup(CPROVER_PREFIX "initialize", init_symbol))
mode=init_symbol->mode;
}

assertions.clear();

local_bitvector_analysist local_bitvector_analysis_obj(goto_function);
Expand All @@ -1607,7 +1609,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
i.is_target())
assertions.clear();

check(i.guard);
check(i.guard, mode);

// magic ERROR label?
for(const auto &label : error_labels)
Expand All @@ -1633,20 +1635,20 @@ void goto_checkt::goto_check(goto_functiont &goto_function)

if(statement==ID_expression)
{
check(i.code);
check(i.code, mode);
}
else if(statement==ID_printf)
{
forall_operands(it, i.code)
check(*it);
check(*it, mode);
}
}
else if(i.is_assign())
{
const code_assignt &code_assign=to_code_assign(i.code);

check(code_assign.lhs());
check(code_assign.rhs());
check(code_assign.lhs(), mode);
check(code_assign.rhs(), mode);

// the LHS might invalidate any assertion
invalidate(code_assign.lhs());
Expand Down Expand Up @@ -1686,7 +1688,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
}

forall_operands(it, code_function_call)
check(*it);
check(*it, mode);

// the call might invalidate any assertion
assertions.clear();
Expand All @@ -1695,7 +1697,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
{
if(i.code.operands().size()==1)
{
check(i.code.op0());
check(i.code.op0(), mode);
// the return value invalidate any assertion
invalidate(i.code.op0());
}
Expand Down Expand Up @@ -1853,7 +1855,7 @@ void goto_check(
goto_functionst::goto_functiont &goto_function)
{
goto_checkt goto_check(ns, options);
goto_check.goto_check(goto_function);
goto_check.goto_check(goto_function, irep_idt());
}

/*******************************************************************\
Expand All @@ -1877,7 +1879,8 @@ void goto_check(

Forall_goto_functions(it, goto_functions)
{
goto_check.goto_check(it->second);
irep_idt mode=ns.lookup(it->first).mode;
goto_check.goto_check(it->second, mode);
}
}

Expand All @@ -1898,10 +1901,5 @@ void goto_check(
goto_modelt &goto_model)
{
const namespacet ns(goto_model.symbol_table);
goto_checkt goto_check(ns, options);

Forall_goto_functions(it, goto_model.goto_functions)
{
goto_check.goto_check(it->second);
}
goto_check(ns, options, goto_model.goto_functions);
}
2 changes: 1 addition & 1 deletion src/analyses/goto_check.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ void goto_check(

#define HELP_GOTO_CHECK \
" --bounds-check enable array bounds checks\n" \
" --pointer-check enable pointer checks\n" \
" --pointer-check enable pointer checks (always enabled for Java)\n" /* NOLINT(whitespace/line_length) */ \
" --memory-leak-check enable memory leak checks\n" \
" --div-by-zero-check enable division by zero checks\n" \
" --signed-overflow-check enable signed arithmetic over- and underflow checks\n" /* NOLINT(whitespace/line_length) */ \
Expand Down