Skip to content

Use from_{expr,type} matching the language of the expression/type #2085

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 1 commit into from
Apr 21, 2018
Merged

Use from_{expr,type} matching the language of the expression/type #2085

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
5 changes: 3 additions & 2 deletions src/analyses/constant_propagator.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Author: Peter Schrammel

#ifdef DEBUG
#include <iostream>
#include <util/format_expr.h>
#endif

#include <util/find_symbols.h>
Expand Down Expand Up @@ -219,7 +220,7 @@ bool constant_propagator_domaint::two_way_propagate_rec(
const namespacet &ns)
{
#ifdef DEBUG
std::cout << "two_way_propagate_rec: " << from_expr(ns, "", expr) << '\n';
std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
#endif

bool change=false;
Expand Down Expand Up @@ -379,7 +380,7 @@ void constant_propagator_domaint::valuest::output(

for(const auto &p : replace_const.expr_map)
{
out << ' ' << p.first << "=" << from_expr(ns, "", p.second) << '\n';
out << ' ' << p.first << "=" << from_expr(ns, p.first, p.second) << '\n';
}
}

Expand Down
73 changes: 35 additions & 38 deletions src/analyses/goto_check.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,8 @@ Author: Daniel Kroening, [email protected]
#include <util/cprover_prefix.h>
#include <util/options.h>

#include <langapi/language_util.h>
#include <langapi/language.h>
#include <langapi/mode.h>

#include "local_bitvector_analysis.h"

Expand Down Expand Up @@ -80,9 +81,8 @@ class goto_checkt
void check_rec(
const exprt &expr,
guardt &guard,
bool address,
const irep_idt &mode);
void check(const exprt &expr, const irep_idt &mode);
bool address);
void check(const exprt &expr);

void bounds_check(const index_exprt &expr, const guardt &guard);
void div_by_zero_check(const div_exprt &expr, const guardt &guard);
Expand All @@ -94,8 +94,7 @@ class goto_checkt
const dereference_exprt &expr,
const guardt &guard,
const exprt &access_lb,
const exprt &access_ub,
const irep_idt &mode);
const exprt &access_ub);
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 @@ -141,6 +140,8 @@ class goto_checkt
typedef std::pair<exprt, exprt> allocationt;
typedef std::list<allocationt> allocationst;
allocationst allocations;

irep_idt mode;
};

void goto_checkt::collect_allocations(
Expand Down Expand Up @@ -917,8 +918,7 @@ void goto_checkt::pointer_validity_check(
const dereference_exprt &expr,
const guardt &guard,
const exprt &access_lb,
const exprt &access_ub,
const irep_idt &mode)
const exprt &access_ub)
{
if(!enable_pointer_check)
return;
Expand Down Expand Up @@ -1274,7 +1274,8 @@ void goto_checkt::add_guarded_claim(

goto_programt::targett t=new_code.add_instruction(type);

std::string source_expr_string=from_expr(ns, "", src_expr);
std::string source_expr_string;
get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);

t->guard.swap(new_expr);
t->source_location=source_location;
Expand All @@ -1283,11 +1284,7 @@ void goto_checkt::add_guarded_claim(
}
}

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

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

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

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

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

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

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

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

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

exprt access_ub=nil_exprt();

Expand All @@ -1394,13 +1391,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, mode);
pointer_validity_check(deref, guard, member_offset, access_ub);

return;
}

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

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

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

void goto_checkt::goto_check(
goto_functiont &goto_function,
const irep_idt &mode)
const irep_idt &_mode)
{
assertions.clear();
mode = _mode;

local_bitvector_analysist local_bitvector_analysis_obj(goto_function);
local_bitvector_analysis=&local_bitvector_analysis_obj;
Expand All @@ -1497,7 +1494,7 @@ void goto_checkt::goto_check(
i.is_target())
assertions.clear();

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

// magic ERROR label?
for(const auto &label : error_labels)
Expand All @@ -1523,20 +1520,20 @@ void goto_checkt::goto_check(

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

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

// the LHS might invalidate any assertion
invalidate(code_assign.lhs());
Expand Down Expand Up @@ -1576,7 +1573,7 @@ void goto_checkt::goto_check(
}

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

// the call might invalidate any assertion
assertions.clear();
Expand All @@ -1585,7 +1582,7 @@ void goto_checkt::goto_check(
{
if(i.code.operands().size()==1)
{
check(i.code.op0(), mode);
check(i.code.op0());
// the return value invalidate any assertion
invalidate(i.code.op0());
}
Expand Down
2 changes: 2 additions & 0 deletions src/analyses/goto_rw.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -633,6 +633,8 @@ void guarded_range_domaint::output(
if(itr!=begin())
out << ";";
out << itr->first << ":" << itr->second.first;
// we don't know what mode (language) we are in, so we rely on the default
// language to be reasonable for from_expr
out << " if " << from_expr(ns, "", itr->second.second);
}
out << "]";
Expand Down
3 changes: 2 additions & 1 deletion src/analyses/invariant_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,6 +131,8 @@ std::string inv_object_storet::build_string(const exprt &expr) const

// we also like "address_of" and "reference_to"
// if the object is constant
// we don't know what mode (language) we are in, so we rely on the default
// language to be reasonable for from_expr
if(is_constant_address(expr))
return from_expr(ns, "", expr);

Expand Down Expand Up @@ -884,7 +886,6 @@ std::string inv_object_storet::to_string(
unsigned a,
const irep_idt &identifier) const
{
// return from_expr(ns, "", get_expr(a));
return id2string(map[a]);
}

Expand Down
5 changes: 4 additions & 1 deletion src/analyses/local_may_alias.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -457,7 +457,10 @@ void local_may_aliast::output(
if(loc_info.aliases.find(j)==i)
{
assert(j<objects.size());
out << ' ' << from_expr(ns, "", objects[j]);
irep_idt identifier = "";
if(objects[j].id() == ID_symbol)
identifier = to_symbol_expr(objects[j]).get_identifier();
out << ' ' << from_expr(ns, identifier, objects[j]);
}

out << " }";
Expand Down
28 changes: 10 additions & 18 deletions src/cbmc/bmc.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -239,17 +239,16 @@ void bmct::show_program()
{
std::cout << "// " << step.source.pc->location_number << " ";
std::cout << step.source.pc->source_location.as_string() << "\n";
const irep_idt &function = step.source.pc->function;

if(step.is_assignment())
{
std::string string_value=
from_expr(ns, "", step.cond_expr);
std::string string_value = from_expr(ns, function, step.cond_expr);
std::cout << "(" << count << ") " << string_value << "\n";

if(!step.guard.is_true())
{
std::string string_value=
from_expr(ns, "", step.guard);
std::string string_value = from_expr(ns, function, step.guard);
std::cout << std::string(std::to_string(count).size()+3, ' ');
std::cout << "guard: " << string_value << "\n";
}
Expand All @@ -258,15 +257,13 @@ void bmct::show_program()
}
else if(step.is_assert())
{
std::string string_value=
from_expr(ns, "", step.cond_expr);
std::string string_value = from_expr(ns, function, step.cond_expr);
std::cout << "(" << count << ") ASSERT("
<< string_value <<") " << "\n";

if(!step.guard.is_true())
{
std::string string_value=
from_expr(ns, "", step.guard);
std::string string_value = from_expr(ns, function, step.guard);
std::cout << std::string(std::to_string(count).size()+3, ' ');
std::cout << "guard: " << string_value << "\n";
}
Expand All @@ -275,15 +272,13 @@ void bmct::show_program()
}
else if(step.is_assume())
{
std::string string_value=
from_expr(ns, "", step.cond_expr);
std::string string_value = from_expr(ns, function, step.cond_expr);
std::cout << "(" << count << ") ASSUME("
<< string_value <<") " << "\n";

if(!step.guard.is_true())
{
std::string string_value=
from_expr(ns, "", step.guard);
std::string string_value = from_expr(ns, function, step.guard);
std::cout << std::string(std::to_string(count).size()+3, ' ');
std::cout << "guard: " << string_value << "\n";
}
Expand All @@ -292,25 +287,22 @@ void bmct::show_program()
}
else if(step.is_constraint())
{
std::string string_value=
from_expr(ns, "", step.cond_expr);
std::string string_value = from_expr(ns, function, step.cond_expr);
std::cout << "(" << count << ") CONSTRAINT("
<< string_value <<") " << "\n";

count++;
}
else if(step.is_shared_read() || step.is_shared_write())
{
std::string string_value=
from_expr(ns, "", step.ssa_lhs);
std::string string_value = from_expr(ns, function, step.ssa_lhs);
std::cout << "(" << count << ") SHARED_"
<< (step.is_shared_write()?"WRITE":"READ")
<< "(" << string_value <<")\n";

if(!step.guard.is_true())
{
std::string string_value=
from_expr(ns, "", step.guard);
std::string string_value = from_expr(ns, function, step.guard);
std::cout << std::string(std::to_string(count).size()+3, ' ');
std::cout << "guard: " << string_value << "\n";
}
Expand Down
Loading