22 #define LOG(message, irep) \
24 debug().source_location = irep.source_location(); \
25 debug() << message << ": " << format(irep) << eom; \
40 symbol_table(symbol_table)
55 const exprt &base_expression,
71 const exprt &expression)
const
73 if(expression.
id()==ID_symbol)
79 if(symbol.
type.
id()!=ID_code)
96 exprt const_symbol_cleared_expr=expression;
97 const_symbol_cleared_expr.
operands().clear();
101 const_symbol_cleared_expr.
operands().push_back(const_symbol_cleared_op);
104 return const_symbol_cleared_expr;
134 if(simplified_expr.id()==ID_index)
139 else if(simplified_expr.id()==ID_member)
144 else if(simplified_expr.id()==ID_address_of)
148 address_expr, resolved_functions);
150 else if(simplified_expr.id()==ID_dereference)
155 else if(simplified_expr.id()==ID_typecast)
161 else if(simplified_expr.id()==ID_symbol)
163 if(simplified_expr.type().id()==ID_code)
170 LOG(
"Non const symbol wasn't squashed", simplified_expr);
174 else if(simplified_expr.id()==ID_constant)
176 if(simplified_expr.is_zero())
184 LOG(
"Non-zero constant value found", simplified_expr);
190 LOG(
"Unrecognised expression", simplified_expr);
196 out_functions.insert(resolved_functions.begin(), resolved_functions.end());
214 for(
const exprt &value : exprs)
222 out_functions.insert(
223 potential_out_functions.begin(),
224 potential_out_functions.end());
228 LOG(
"Could not resolve expression in array", value);
256 LOG(
"Could not resolve array", index_expr);
262 LOG(
"Array not const", index_expr);
288 LOG(
"Could not resolve struct", member_expr);
294 LOG(
"Struct was not const so can't resolve values on it", member_expr);
316 LOG(
"Failed to resolve address of", address_expr);
340 LOG(
"Failed to squash dereference", deref_expr);
346 LOG(
"Dereferenced value was not const so can't dereference", deref_expr);
375 out_functions.insert(typecast_values.begin(), typecast_values.end());
380 LOG(
"Failed to squash typecast", typecast_expr);
405 bool is_resolved_expression_const =
false;
406 if(simplified_expr.
id()==ID_index)
411 index_expr, resolved_expressions, is_resolved_expression_const);
413 else if(simplified_expr.
id()==ID_member)
417 member_expr, resolved_expressions, is_resolved_expression_const);
419 else if(simplified_expr.
id()==ID_dereference)
424 deref, resolved_expressions, is_resolved_expression_const);
426 else if(simplified_expr.
id()==ID_typecast)
431 typecast_expr, resolved_expressions, is_resolved_expression_const);
433 else if(simplified_expr.
id()==ID_symbol)
435 LOG(
"Non const symbol will not be squashed", simplified_expr);
440 resolved_expressions.push_back(simplified_expr);
447 out_resolved_expression.insert(
448 out_resolved_expression.end(),
449 resolved_expressions.begin(),
450 resolved_expressions.end());
451 out_is_const=is_resolved_expression_const;
476 if(index_value_expressions.size()==1 &&
477 index_value_expressions.front().id()==ID_constant)
482 bool errors=
to_integer(constant_expr, array_index);
485 out_array_index=array_index;
517 bool array_const=
false;
521 potential_array_exprs,
526 bool all_possible_const=
true;
527 for(
const exprt &potential_array_expr : potential_array_exprs)
530 all_possible_const &&
533 if(potential_array_expr.id()==ID_array)
540 const exprt &func_expr =
541 potential_array_expr.
operands()[numeric_cast_v<std::size_t>(value)];
542 bool value_const=
false;
548 out_expressions.insert(
549 out_expressions.end(),
550 array_out_functions.begin(),
551 array_out_functions.end());
555 LOG(
"Failed to resolve array value", func_expr);
563 for(
const exprt &array_entry : potential_array_expr.
operands())
569 array_entry, array_contents, is_entry_const);
573 LOG(
"Failed to resolve array value", array_entry);
577 for(
const exprt &resolved_array_entry : array_contents)
579 out_expressions.push_back(resolved_array_entry);
587 "Squashing index of did not result in an array",
588 potential_array_expr);
593 out_is_const=all_possible_const || array_const;
598 LOG(
"Failed to squash index of to array expression", index_expr);
617 bool is_struct_const;
620 bool resolved_struct=
622 member_expr.
compound(), potential_structs, is_struct_const);
625 for(
const exprt &potential_struct : potential_structs)
627 if(potential_struct.id()==ID_struct)
630 const exprt &component_value=
633 bool component_const=
false;
636 component_value, resolved_expressions, component_const);
639 out_expressions.insert(
640 out_expressions.end(),
641 resolved_expressions.begin(),
642 resolved_expressions.end());
646 LOG(
"Could not resolve component value", component_value);
653 "Squashing member access did not resolve in a struct",
658 out_is_const=is_struct_const;
663 LOG(
"Failed to squash struct access", member_expr);
690 if(resolved && pointer_const)
692 bool all_objects_const=
true;
693 for(
const exprt &pointer_val : pointer_values)
695 if(pointer_val.id()==ID_address_of)
698 bool object_const=
false;
701 address_expr.
object(), out_object_values, object_const);
705 out_expressions.insert(
706 out_expressions.end(),
707 out_object_values.begin(),
708 out_object_values.end());
710 all_objects_const&=object_const;
714 LOG(
"Failed to resolve value of a dereference", address_expr);
720 "Squashing dereference did not result in an address", pointer_val);
724 out_is_const=all_objects_const;
731 LOG(
"Failed to resolve pointer of dereference", deref_expr);
733 else if(!pointer_const)
735 LOG(
"Pointer value not const so can't squash", deref_expr);
757 typecast_expr.
op(), typecast_values, typecast_const);
761 out_expressions.insert(
762 out_expressions.end(),
763 typecast_values.begin(),
764 typecast_values.end());
765 out_is_const=typecast_const;
770 LOG(
"Could not resolve typecast value", typecast_expr);
779 const exprt &expression)
const
793 return type.
get_bool(ID_C_constant);
805 size_t component_number=
808 return struct_expr.
operands()[component_number];