Skip to content

Commit 229bd5b

Browse files
smowtonpeterschrammel
authored andcommitted
Add symbol parsing utilities.
This returns some code that was deprecated and removed in master, thus this commit will need work before it can be PR'd.
1 parent 116d994 commit 229bd5b

File tree

2 files changed

+244
-0
lines changed

2 files changed

+244
-0
lines changed

src/util/namespace_utils.cpp

+127
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
#include "namespace_utils.h"
2+
#include "symbol.h"
3+
#include <goto-programs/remove_returns.h>
4+
5+
6+
/*******************************************************************\
7+
Function: namespace_utils_baset::does_symbol_match
8+
9+
Purpose:
10+
Checks whether an exprt is actually a symbolt matching a predicate
11+
12+
Inputs:
13+
lvalue:
14+
An exprt to be tested
15+
predicate:
16+
The predicate to test for
17+
18+
Outputs:
19+
Whether the exprt was actually a symbolt matching a predicate
20+
21+
\*******************************************************************/
22+
bool namespace_utils_baset::does_symbol_match(
23+
const exprt &lvalue,
24+
std::function<bool(symbolt)> predicate) const
25+
{
26+
if(lvalue.id()!=ID_symbol)
27+
return false;
28+
const symbolt *symbol;
29+
if(lookup(lvalue.get(ID_identifier), symbol))
30+
return false;
31+
return predicate(*symbol);
32+
}
33+
34+
/*******************************************************************\
35+
Function: namespace_utils_baset::is_parameter
36+
37+
Purpose:
38+
Checks whether an exprt is actually a parameter symbol
39+
40+
Inputs:
41+
lvalue:
42+
An exprt to be tested
43+
44+
Outputs:
45+
Whether the exprt was actually a parameter symbol
46+
47+
\*******************************************************************/
48+
bool namespace_utils_baset::is_parameter(const exprt &lvalue) const
49+
{
50+
return does_symbol_match(
51+
lvalue,
52+
[] (symbolt symbol) { return symbol.is_parameter; });
53+
}
54+
55+
/*******************************************************************\
56+
Function: namespace_utils_baset::is_static
57+
58+
Purpose:
59+
Checks whether an exprt is actually a static symbol
60+
61+
Inputs:
62+
lvalue:
63+
An exprt to be tested
64+
65+
Outputs:
66+
Whether the exprt was actually a static symbol
67+
68+
\*******************************************************************/
69+
bool namespace_utils_baset::is_static(const exprt &lvalue) const
70+
{
71+
// TODO: Also check for static member accesses
72+
return does_symbol_match(
73+
lvalue,
74+
[] (symbolt symbol) { return symbol.is_static_lifetime; });
75+
}
76+
77+
/*******************************************************************\
78+
Function: namespace_utils_baset::is_auxiliary_variable
79+
80+
Purpose:
81+
Checks whether an exprt is actually an auxiliary variable symbol
82+
83+
Inputs:
84+
lvalue:
85+
An exprt to be tested
86+
87+
Outputs:
88+
Whether the exprt was actually an auxiliary variable symbol
89+
90+
\*******************************************************************/
91+
bool namespace_utils_baset::is_auxiliary_variable(const exprt &lvalue) const
92+
{
93+
return does_symbol_match(
94+
lvalue,
95+
[] (symbolt symbol) { return symbol.is_auxiliary; });
96+
}
97+
98+
/*******************************************************************\
99+
Function: namespace_utils_baset::is_return_value_auxiliary
100+
101+
Purpose:
102+
Checks whether an exprt is actually an auxiliary return value symbol
103+
104+
Inputs:
105+
lvalue:
106+
An exprt to be tested
107+
108+
Outputs:
109+
Whether the exprt was actually an auxiliary return value symbol
110+
111+
\*******************************************************************/
112+
bool namespace_utils_baset::is_return_value_auxiliary(const exprt &lvalue) const
113+
{
114+
return
115+
does_symbol_match(
116+
lvalue,
117+
[] (symbolt symbol)
118+
{
119+
return
120+
symbol.is_static_lifetime
121+
&& symbol.is_auxiliary
122+
&& symbol.is_file_local
123+
&& symbol.is_thread_local;
124+
})
125+
&& as_string(lvalue.get(ID_identifier)).find(RETURN_VALUE_SUFFIX)
126+
!= std::string::npos;
127+
}

src/util/namespace_utils.h

+117
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
// THIS FILE IS DEPRECATED
10+
11+
#ifndef CPROVER_NAMESPACE_UTILS_H
12+
#define CPROVER_NAMESPACE_UTILS_H
13+
14+
#include <functional>
15+
#include "namespace.h"
16+
#include "base_type.h"
17+
#include "type_eq.h"
18+
#include "std_expr.h"
19+
20+
// second: true <=> not found
21+
22+
class namespace_utils_baset
23+
{
24+
public:
25+
virtual ~namespace_utils_baset()
26+
{
27+
}
28+
29+
const symbolt &lookup(const irep_idt &name) const
30+
{
31+
const symbolt *symbol;
32+
if(lookup(name, symbol))
33+
throw "identifier "+id2string(name)+" not found";
34+
return *symbol;
35+
}
36+
37+
const symbolt &lookup(const symbol_exprt &symbol_expr) const
38+
{
39+
const symbolt *symbol;
40+
if(lookup(symbol_expr.get_identifier(), symbol))
41+
throw "identifier "+id2string(symbol_expr.get_identifier())+" not found";
42+
return *symbol;
43+
}
44+
45+
bool lookup(const irep_idt &name, const symbolt *&symbol) const
46+
{
47+
return ns().lookup(name, symbol);
48+
}
49+
50+
bool lookup_symbol(const exprt &symbol_expr, const symbolt *&symbol) const
51+
{
52+
return ns().lookup(symbol_expr.get(ID_identifier), symbol);
53+
}
54+
55+
void follow_symbol(irept &irep) const
56+
{
57+
ns().follow_symbol(irep);
58+
}
59+
60+
void follow_macros(exprt &expr) const
61+
{
62+
ns().follow_macros(expr);
63+
}
64+
65+
/*
66+
void base_type(typet &type)
67+
{
68+
::base_type(type, ns());
69+
}
70+
71+
void base_type(exprt &expr)
72+
{
73+
::base_type(expr, ns());
74+
}
75+
*/
76+
77+
78+
private:
79+
bool does_symbol_match(
80+
const exprt& lvalue,
81+
std::function<bool(symbolt)> predicate) const;
82+
83+
public:
84+
bool is_parameter(const exprt& lvalue) const;
85+
bool is_static(const exprt& lvalue) const;
86+
bool is_auxiliary_variable(const exprt& lvalue) const;
87+
bool is_return_value_auxiliary(const exprt& lvalue) const;
88+
89+
bool type_eq(const typet &type1, const typet &type2)
90+
{
91+
return ::type_eq(type1, type2, ns());
92+
}
93+
94+
bool base_type_eq(const typet &type1, const typet &type2)
95+
{
96+
return ::base_type_eq(type1, type2, ns());
97+
}
98+
99+
protected:
100+
virtual const namespacet &ns() const=0;
101+
};
102+
103+
class namespace_utilst:public virtual namespace_utils_baset
104+
{
105+
public:
106+
namespace_utilst(const namespacet &_ns):__ns(_ns){}
107+
108+
protected:
109+
const namespacet &__ns;
110+
111+
virtual const namespacet &ns() const
112+
{
113+
return __ns;
114+
}
115+
};
116+
117+
#endif

0 commit comments

Comments
 (0)