cprover
does_remove_const.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Analyses
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
12#include "does_remove_const.h"
13
15
16#include <util/base_type.h>
17#include <util/pointer_expr.h>
18#include <util/std_code.h>
19
25 const goto_programt &goto_program,
26 const namespacet &ns):
27 goto_program(goto_program),
28 ns(ns)
29{}
30
33std::pair<bool, source_locationt> does_remove_constt::operator()() const
34{
35 for(const goto_programt::instructiont &instruction :
37 {
38 if(!instruction.is_assign())
39 {
40 continue;
41 }
42
43 const typet &rhs_type = instruction.assign_rhs().type();
44 const typet &lhs_type = instruction.assign_lhs().type();
45
46 // Compare the types recursively for a point where the rhs is more
47 // const that the lhs
48 if(!does_type_preserve_const_correctness(&lhs_type, &rhs_type))
49 {
50 return {true, instruction.source_location()};
51 }
52
53 if(does_expr_lose_const(instruction.assign_rhs()))
54 {
55 return {true, instruction.assign_rhs().find_source_location()};
56 }
57 }
58
59 return {false, source_locationt()};
60}
61
69{
70 const typet &root_type=expr.type();
71
72 // Look in each child that has the same base type as the root
73 for(const exprt &op : expr.operands())
74 {
75 const typet &op_type=op.type();
76 if(base_type_eq(op_type, root_type, ns))
77 {
78 // Is this child more const-qualified than the root
79 if(!does_type_preserve_const_correctness(&root_type, &op_type))
80 {
81 return true;
82 }
83 }
84
85 // Recursively check the children of this child
87 {
88 return true;
89 }
90 }
91 return false;
92}
93
122 const typet *target_type, const typet *source_type) const
123{
124 while(target_type->id()==ID_pointer)
125 {
126 PRECONDITION(source_type->id() == ID_pointer);
127
128 const auto &target_pointer_type = to_pointer_type(*target_type);
129 const auto &source_pointer_type = to_pointer_type(*source_type);
130
131 bool direct_subtypes_at_least_as_const = is_type_at_least_as_const_as(
132 target_pointer_type.base_type(), source_pointer_type.base_type());
133 // We have a pointer to something, but the thing it is pointing to can't be
134 // modified normally, but can through this pointer
135 if(!direct_subtypes_at_least_as_const)
136 return false;
137 // Check the subtypes if they are pointers
138 target_type = &target_pointer_type.base_type();
139 source_type = &source_pointer_type.base_type();
140 }
141 return true;
142}
143
166 const typet &type_more_const, const typet &type_compare) const
167{
168 return !type_compare.get_bool(ID_C_constant) ||
169 type_more_const.get_bool(ID_C_constant);
170}
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:291
Base Type Computation.
bool is_type_at_least_as_const_as(const typet &type_more_const, const typet &type_compare) const
A simple check to check the type_more_const is at least as const as type compare.
bool does_type_preserve_const_correctness(const typet *target_type, const typet *source_type) const
A recursive check that handles when assigning a source value to a target, is the assignment a loss of...
does_remove_constt(const goto_programt &goto_program, const namespacet &ns)
A naive analysis to look for casts that remove const-ness from pointers.
std::pair< bool, source_locationt > operator()() const
A naive analysis to look for casts that remove const-ness from pointers.
const goto_programt & goto_program
bool does_expr_lose_const(const exprt &expr) const
Search the expression tree to look for any children that have the same base type, but a less strict c...
const namespacet & ns
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:199
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:213
const source_locationt & source_location() const
Definition: goto_program.h:332
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irep_idt & id() const
Definition: irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The type of an expression, extends irept.
Definition: type.h:29
Concrete Goto Program.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
#define PRECONDITION(CONDITION)
Definition: invariant.h:463