Skip to content

writeable_object and live_object #7125

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 2 commits into from
Sep 13, 2022
Merged

writeable_object and live_object #7125

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f4a3076
add three doubly-linked list predicates
kroening Apr 26, 2021
b14cd4f
introduce __CPROVER_WRITEABLE_OBJECT and __CPROVER_LIVE_OBJECT
kroening May 16, 2022
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
116 changes: 116 additions & 0 deletions src/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2316,6 +2316,90 @@ exprt c_typecheck_baset::do_special_functions(

return std::move(is_list_expr);
}
else if(identifier == CPROVER_PREFIX "is_dll")
{
if(expr.arguments().size() != 1)
{
error().source_location = f_op.source_location();
error() << "is_dll expects one operand" << eom;
throw 0;
}

typecheck_function_call_arguments(expr);

if(
expr.arguments()[0].type().id() != ID_pointer ||
to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
ID_struct_tag)
{
error().source_location = expr.arguments()[0].source_location();
error() << "is_dll expects a struct-pointer operand" << eom;
throw 0;
}

predicate_exprt is_dll_expr("is_dll");
is_dll_expr.operands() = expr.arguments();
is_dll_expr.add_source_location() = source_location;

return std::move(is_dll_expr);
}
else if(identifier == CPROVER_PREFIX "is_cyclic_dll")
{
if(expr.arguments().size() != 1)
{
error().source_location = f_op.source_location();
error() << "is_cyclic_dll expects one operand" << eom;
throw 0;
}

typecheck_function_call_arguments(expr);

if(
expr.arguments()[0].type().id() != ID_pointer ||
to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
ID_struct_tag)
{
error().source_location = expr.arguments()[0].source_location();
error() << "is_cyclic_dll expects a struct-pointer operand" << eom;
throw 0;
}

predicate_exprt is_cyclic_dll_expr("is_cyclic_dll");
is_cyclic_dll_expr.operands() = expr.arguments();
is_cyclic_dll_expr.add_source_location() = source_location;

return std::move(is_cyclic_dll_expr);
}
else if(identifier == CPROVER_PREFIX "is_sentinel_dll")
{
if(expr.arguments().size() != 2 && expr.arguments().size() != 3)
{
error().source_location = f_op.source_location();
error() << "is_sentinel_dll expects two or three operands" << eom;
throw 0;
}

typecheck_function_call_arguments(expr);

for(const auto &argument : expr.arguments())
{
if(
argument.type().id() != ID_pointer ||
to_pointer_type(argument.type()).base_type().id() != ID_struct_tag)
{
error().source_location = expr.arguments()[0].source_location();
error() << "is_sentinel_dll_node expects struct-pointer operands"
<< eom;
throw 0;
}
}

predicate_exprt is_sentinel_dll_expr("is_sentinel_dll");
is_sentinel_dll_expr.operands() = expr.arguments();
is_sentinel_dll_expr.add_source_location() = source_location;

return std::move(is_sentinel_dll_expr);
}
else if(identifier == CPROVER_PREFIX "is_cstring")
{
if(expr.arguments().size() != 1)
Expand Down Expand Up @@ -2414,6 +2498,38 @@ exprt c_typecheck_baset::do_special_functions(

return is_dynamic_object_expr;
}
else if(identifier == CPROVER_PREFIX "LIVE_OBJECT")
{
if(expr.arguments().size() != 1)
{
error().source_location = f_op.source_location();
error() << "live_object expects one argument" << eom;
throw 0;
}

typecheck_function_call_arguments(expr);

exprt live_object_expr = live_object_exprt(expr.arguments()[0]);
live_object_expr.add_source_location() = source_location;

return live_object_expr;
}
else if(identifier == CPROVER_PREFIX "WRITEABLE_OBJECT")
Copy link
Collaborator

Choose a reason for hiding this comment

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

I'm starting to wonder: to what extent is this different from __CPROVER_w_ok(p, 1)?

Copy link
Member Author

Choose a reason for hiding this comment

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

Very. The idea is to define w_ok(p, s) = writeable ∧ live ∧ offset+s≤object_size.
This won't work in CBMC without major changes, so this will be CHC only for now.

{
if(expr.arguments().size() != 1)
{
error().source_location = f_op.source_location();
error() << "writeable_object expects one argument" << eom;
throw 0;
}

typecheck_function_call_arguments(expr);

exprt writeable_object_expr = writeable_object_exprt(expr.arguments()[0]);
writeable_object_expr.add_source_location() = source_location;

return writeable_object_expr;
}
else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
{
if(expr.arguments().size()!=1)
Expand Down
5 changes: 5 additions & 0 deletions src/ansi-c/cprover_builtin_headers.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,9 @@ __CPROVER_bool __CPROVER_is_invalid_pointer(const void *);
_Bool __CPROVER_is_zero_string(const void *);
// a singly-linked null-terminated dynamically-allocated list
__CPROVER_bool __CPROVER_is_list();
__CPROVER_bool __CPROVER_is_dll();
__CPROVER_bool __CPROVER_is_cyclic_dll();
__CPROVER_bool __CPROVER_is_sentinel_dll();
__CPROVER_size_t __CPROVER_zero_string_length(const void *);
__CPROVER_bool __CPROVER_is_cstring(const char *);
__CPROVER_size_t __CPROVER_cstrlen(const char *);
Expand Down Expand Up @@ -46,6 +49,8 @@ void __CPROVER_old(const void *);
void __CPROVER_loop_entry(const void *);

// pointers
__CPROVER_bool __CPROVER_LIVE_OBJECT(const void *);
__CPROVER_bool __CPROVER_WRITEABLE_OBJECT(const void *);
__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
Expand Down
2 changes: 2 additions & 0 deletions src/ansi-c/expr2c.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3988,6 +3988,8 @@ optionalt<std::string> expr2ct::convert_function(const exprt &src)
{ID_count_leading_zeros, "__builtin_clz"},
{ID_count_trailing_zeros, "__builtin_ctz"},
{ID_dynamic_object, "DYNAMIC_OBJECT"},
{ID_live_object, "LIVE_OBJECT"},
{ID_writeable_object, "WRITEABLE_OBJECT"},
{ID_floatbv_div, "FLOAT/"},
{ID_floatbv_minus, "FLOAT-"},
{ID_floatbv_mult, "FLOAT*"},
Expand Down