Skip to content

Disable unnecessary pointer checks, enable necessary pointer checks i… #6459

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
Dec 3, 2021
Merged

Disable unnecessary pointer checks, enable necessary pointer checks i… #6459

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
850578b
Adding readable names for CAR instrumentation variables.
Dec 3, 2021
26dc976
Disabling pointer checks on CAR inclusion instructions. Enabling poin…
Dec 3, 2021
e2f4fec
Fixed test that triggers the newly added pointer overflow checks
Dec 3, 2021
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
50 changes: 33 additions & 17 deletions src/goto-instrument/contracts/assigns.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Date: July 2021
/// Specify write set in code contracts

#include "assigns.h"
#include "utils.h"

#include <analyses/call_graph.h>

Expand Down Expand Up @@ -87,41 +88,54 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
const
{
goto_programt instructions;

instructions.add(goto_programt::make_decl(validity_condition_var, location));
instructions.add(goto_programt::make_decl(lower_bound_address_var, location));
instructions.add(goto_programt::make_decl(upper_bound_address_var, location));
// adding pragmas to the location to selectively disable checks
// where it is sound to do so
Comment on lines +91 to +92
Copy link
Collaborator

Choose a reason for hiding this comment

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

I think a brief explanation of "why" is sound to disable checks here would be more helpful, since one can easily infer this comment from the code.

source_locationt location_no_checks = location;
disable_pointer_checks(location_no_checks);

instructions.add(
goto_programt::make_decl(validity_condition_var, location_no_checks));
instructions.add(
goto_programt::make_decl(lower_bound_address_var, location_no_checks));
instructions.add(
goto_programt::make_decl(upper_bound_address_var, location_no_checks));

instructions.add(goto_programt::make_assignment(
lower_bound_address_var,
null_pointer_exprt{to_pointer_type(slice.first.type())},
location));
location_no_checks));
instructions.add(goto_programt::make_assignment(
upper_bound_address_var,
null_pointer_exprt{to_pointer_type(slice.first.type())},
location));
location_no_checks));

goto_programt skip_program;
const auto skip_target = skip_program.add(goto_programt::make_skip(location));
const auto skip_target =
skip_program.add(goto_programt::make_skip(location_no_checks));

const auto validity_check_expr =
and_exprt{all_dereferences_are_valid(source_expr, parent.ns),
w_ok_exprt{slice.first, slice.second}};
instructions.add(goto_programt::make_assignment(
validity_condition_var, validity_check_expr, location));
validity_condition_var, validity_check_expr, location_no_checks));

instructions.add(goto_programt::make_goto(
skip_target, not_exprt{validity_condition_var}, location));
skip_target, not_exprt{validity_condition_var}, location_no_checks));

instructions.add(goto_programt::make_assignment(
lower_bound_address_var, slice.first, location));
lower_bound_address_var, slice.first, location_no_checks));

// the computation of the CAR upper bound can overflow into the object ID bits
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
// the computation of the CAR upper bound can overflow into the object ID bits
// The computation of the CAR upper bound can overflow into the object ID bits

// of the pointer with very large allocation sizes.
// We enable pointer overflow checks to detect such cases.
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
// We enable pointer overflow checks to detect such cases.
// We always enable pointer overflow checks to detect such cases.

source_locationt location_overflow_check = location;
location_overflow_check.add_pragma("enable:pointer-overflow-check");

instructions.add(goto_programt::make_assignment(
upper_bound_address_var,
minus_exprt{plus_exprt{slice.first, slice.second},
from_integer(1, slice.second.type())},
location));

location_overflow_check));
instructions.destructive_append(skip_program);

// The assignments above are only performed on locally defined temporaries
Expand All @@ -134,14 +148,16 @@ const exprt
assigns_clauset::conditional_address_ranget::generate_unsafe_inclusion_check(
const conditional_address_ranget &lhs) const
{
// remark: both lb and ub are derived from the same object so checking
// same_object(upper_bound_address_var, lhs.upper_bound_address_var)
// is redundant
Comment on lines +151 to +153
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nice!

Suggested change
// remark: both lb and ub are derived from the same object so checking
// same_object(upper_bound_address_var, lhs.upper_bound_address_var)
// is redundant
// Both lb and ub are derived from the same object so checking
// same_object(upper_bound_address_var, lhs.upper_bound_address_var)
// is redundant

return conjunction(
{validity_condition_var,
same_object(lower_bound_address_var, lhs.lower_bound_address_var),
same_object(lhs.upper_bound_address_var, upper_bound_address_var),
less_than_or_equal_exprt{lower_bound_address_var,
lhs.lower_bound_address_var},
less_than_or_equal_exprt{lhs.upper_bound_address_var,
upper_bound_address_var}});
less_than_or_equal_exprt{pointer_offset(lower_bound_address_var),
pointer_offset(lhs.lower_bound_address_var)},
less_than_or_equal_exprt{pointer_offset(lhs.upper_bound_address_var),
pointer_offset(upper_bound_address_var)}});
}

assigns_clauset::assigns_clauset(
Expand Down
37 changes: 21 additions & 16 deletions src/goto-instrument/contracts/contracts.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -911,6 +911,8 @@ void code_contractst::instrument_call_statement(
}
else if(callee_name == "free")
{
source_locationt location_no_checks = instruction_it->source_location();
disable_pointer_checks(location_no_checks);
Copy link
Collaborator

Choose a reason for hiding this comment

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

We could add a comment here again explaining "why" is safe to always remove pointer checks in this location.

const auto free_car = add_inclusion_check(
body,
assigns,
Expand All @@ -920,10 +922,9 @@ void code_contractst::instrument_call_statement(
// skip all invalidation business if we're freeing invalid memory
goto_programt alias_checking_instructions, skip_program;
alias_checking_instructions.add(goto_programt::make_goto(
skip_program.add(
goto_programt::make_skip(instruction_it->source_location())),
skip_program.add(goto_programt::make_skip(location_no_checks)),
not_exprt{free_car.validity_condition_var},
instruction_it->source_location()));
location_no_checks));

// Since the argument to free may be an "alias" (but not identical)
// to existing CARs' source_expr, structural equality wouldn't work.
Expand All @@ -943,8 +944,8 @@ void code_contractst::instrument_call_statement(
.symbol_expr();
write_set_validity_addrs.insert(object_validity_var_addr);

alias_checking_instructions.add(goto_programt::make_decl(
object_validity_var_addr, instruction_it->source_location()));
alias_checking_instructions.add(
goto_programt::make_decl(object_validity_var_addr, location_no_checks));
// if the CAR was defined on the same_object as the one being `free`d,
// record its validity variable's address, otherwise record NULL
alias_checking_instructions.add(goto_programt::make_assignment(
Expand All @@ -956,7 +957,7 @@ void code_contractst::instrument_call_statement(
free_car.lower_bound_address_var, w_car.lower_bound_address_var)},
address_of_exprt{w_car.validity_condition_var},
null_pointer_exprt{to_pointer_type(object_validity_var_addr.type())}},
instruction_it->source_location()));
location_no_checks));
}

alias_checking_instructions.destructive_append(skip_program);
Expand All @@ -972,24 +973,22 @@ void code_contractst::instrument_call_statement(
goto_programt invalidation_instructions;
skip_program.clear();
invalidation_instructions.add(goto_programt::make_goto(
skip_program.add(
goto_programt::make_skip(instruction_it->source_location())),
skip_program.add(goto_programt::make_skip(location_no_checks)),
not_exprt{free_car.validity_condition_var},
instruction_it->source_location()));
location_no_checks));

// invalidate all recorded CAR validity variables
for(const auto &w_car_validity_addr : write_set_validity_addrs)
{
goto_programt w_car_skip_program;
invalidation_instructions.add(goto_programt::make_goto(
w_car_skip_program.add(
goto_programt::make_skip(instruction_it->source_location())),
w_car_skip_program.add(goto_programt::make_skip(location_no_checks)),
null_pointer(w_car_validity_addr),
instruction_it->source_location()));
location_no_checks));
invalidation_instructions.add(goto_programt::make_assignment(
dereference_exprt{w_car_validity_addr},
false_exprt{},
instruction_it->source_location()));
location_no_checks));
invalidation_instructions.destructive_append(w_car_skip_program);
}

Expand Down Expand Up @@ -1175,6 +1174,9 @@ void code_contractst::check_frame_conditions(
else if(instruction_it->is_dead())
{
const auto &symbol = instruction_it->dead_symbol();
source_locationt location_no_checks = instruction_it->source_location();
disable_pointer_checks(location_no_checks);
Copy link
Collaborator

Choose a reason for hiding this comment

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

As above: is the reference intentional?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

fixed

Copy link
Collaborator

Choose a reason for hiding this comment

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

We could add a comment here again explaining "why" is safe to always remove pointer checks in this location.


// CAR equality and hash are defined on source_expr alone,
// therefore this temporary CAR should be "found"
const auto &symbol_car = assigns.get_write_set().find(
Expand Down Expand Up @@ -1228,10 +1230,13 @@ code_contractst::add_inclusion_check(
program, instruction_it, snapshot_instructions);

goto_programt assertion;
assertion.add(goto_programt::make_assertion(
assigns.generate_inclusion_check(car), instruction_it->source_location()));
assertion.instructions.back().source_location_nonconst().set_comment(
source_locationt location_no_checks =
instruction_it->source_location_nonconst();
Copy link
Collaborator

Choose a reason for hiding this comment

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

Certainly source_location() instead of source_location_nonconst().

disable_pointer_checks(location_no_checks);
Copy link
Collaborator

Choose a reason for hiding this comment

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

We could add a comment here again explaining "why" is safe to always remove pointer checks in this location.

location_no_checks.set_comment(
"Check that " + from_expr(ns, expr.id(), expr) + " is assignable");
assertion.add(goto_programt::make_assertion(
assigns.generate_inclusion_check(car), location_no_checks));
insert_before_swap_and_advance(program, instruction_it, assertion);

return car;
Expand Down
10 changes: 8 additions & 2 deletions src/goto-instrument/contracts/utils.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,7 +153,13 @@ const symbolt &new_tmp_symbol(
location,
mode,
symtab);
new_symbol.is_auxiliary = is_auxiliary;
return new_symbol;
new_symbol.is_auxiliary = is_auxiliary;
return new_symbol;
}

void disable_pointer_checks(source_locationt &source_location)
{
source_location.add_pragma("disable:pointer-check");
source_location.add_pragma("disable:pointer-primitive-check");
source_location.add_pragma("disable:pointer-overflow-check");
}
5 changes: 4 additions & 1 deletion src/goto-instrument/contracts/utils.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ void insert_before_swap_and_advance(
/// \param mode: The mode for the new symbol, e.g. ID_C, ID_java.
/// \param symtab: The symbol table to which the new symbol is to be added.
/// \param suffix: Suffix to use to generate the unique name
/// \param is_auxiliary: Do not print symbol in traces if true (default = false)
/// \param is_auxiliary: Do not print symbol in traces if true (default = false)
/// \return The new symbolt object.
const symbolt &new_tmp_symbol(
const typet &type,
Expand All @@ -122,4 +122,7 @@ const symbolt &new_tmp_symbol(
std::string suffix = "tmp_cc",
bool is_auxiliary = false);

/// Add disable pragmas for all pointer checks on the given location
void disable_pointer_checks(source_locationt &source_location);

#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H