Skip to content

Commit 7bf2e3a

Browse files
author
martin
committed
Move the interface of domains to it's own header file.
ai.{h,cpp} is already crowded with two different interfaces. The following patch set will make this much worse, thus we start by refactoring.
1 parent ec79bdd commit 7bf2e3a

File tree

5 files changed

+206
-168
lines changed

5 files changed

+206
-168
lines changed

‎src/analyses/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
SRC = ai.cpp \
2+
ai_domain.cpp \
23
call_graph.cpp \
34
call_graph_helpers.cpp \
45
constant_propagator.cpp \

‎src/analyses/ai.cpp

Lines changed: 0 additions & 69 deletions
Original file line numberDiff line numberDiff line change
@@ -15,80 +15,11 @@ Author: Daniel Kroening, [email protected]
1515
#include <memory>
1616
#include <sstream>
1717

18-
#include <util/simplify_expr.h>
1918
#include <util/std_expr.h>
2019
#include <util/std_code.h>
2120

2221
#include "is_threaded.h"
2322

24-
jsont ai_domain_baset::output_json(
25-
const ai_baset &ai,
26-
const namespacet &ns) const
27-
{
28-
std::ostringstream out;
29-
output(out, ai, ns);
30-
json_stringt json(out.str());
31-
return json;
32-
}
33-
34-
xmlt ai_domain_baset::output_xml(
35-
const ai_baset &ai,
36-
const namespacet &ns) const
37-
{
38-
std::ostringstream out;
39-
output(out, ai, ns);
40-
xmlt xml("abstract_state");
41-
xml.data=out.str();
42-
return xml;
43-
}
44-
45-
/// Use the information in the domain to simplify the expression on the LHS of
46-
/// an assignment. This for example won't simplify symbols to their values, but
47-
/// does simplify indices in arrays, members of structs and dereferencing of
48-
/// pointers
49-
/// \param condition: the expression to simplify
50-
/// \param ns: the namespace
51-
/// \return True if condition did not change. False otherwise. condition will be
52-
/// updated with the simplified condition if it has worked
53-
bool ai_domain_baset::ai_simplify_lhs(
54-
exprt &condition, const namespacet &ns) const
55-
{
56-
// Care must be taken here to give something that is still writable
57-
if(condition.id()==ID_index)
58-
{
59-
index_exprt ie=to_index_expr(condition);
60-
bool no_simplification=ai_simplify(ie.index(), ns);
61-
if(!no_simplification)
62-
condition=simplify_expr(ie, ns);
63-
64-
return no_simplification;
65-
}
66-
else if(condition.id()==ID_dereference)
67-
{
68-
dereference_exprt de=to_dereference_expr(condition);
69-
bool no_simplification=ai_simplify(de.pointer(), ns);
70-
if(!no_simplification)
71-
condition=simplify_expr(de, ns); // So *(&x) -> x
72-
73-
return no_simplification;
74-
}
75-
else if(condition.id()==ID_member)
76-
{
77-
member_exprt me=to_member_expr(condition);
78-
// Since simplify_ai_lhs is required to return an addressable object
79-
// (so remains a valid left hand side), to simplify
80-
// `(something_simplifiable).b` we require that `something_simplifiable`
81-
// must also be addressable
82-
bool no_simplification=ai_simplify_lhs(me.compound(), ns);
83-
if(!no_simplification)
84-
condition=simplify_expr(me, ns);
85-
86-
return no_simplification;
87-
}
88-
else
89-
return true;
90-
}
91-
9223
void ai_baset::output(
9324
const namespacet &ns,
9425
const goto_functionst &goto_functions,

‎src/analyses/ai.h

Lines changed: 1 addition & 99 deletions
Original file line numberDiff line numberDiff line change
@@ -23,105 +23,7 @@ Author: Daniel Kroening, [email protected]
2323

2424
#include <goto-programs/goto_model.h>
2525

26-
// forward reference
27-
class ai_baset;
28-
29-
// don't use me -- I am just a base class
30-
// please derive from me
31-
class ai_domain_baset
32-
{
33-
public:
34-
// The constructor is expected to produce 'false'
35-
// or 'bottom'
36-
ai_domain_baset()
37-
{
38-
}
39-
40-
virtual ~ai_domain_baset()
41-
{
42-
}
43-
44-
typedef goto_programt::const_targett locationt;
45-
46-
// how function calls are treated:
47-
// a) there is an edge from each call site to the function head
48-
// b) there is an edge from the last instruction (END_FUNCTION)
49-
// of the function to the instruction _following_ the call site
50-
// (this also needs to set the LHS, if applicable)
51-
//
52-
// "this" is the domain before the instruction "from"
53-
// "from" is the instruction to be interpretted
54-
// "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
55-
//
56-
// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
57-
// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
58-
// PRECONDITION(are_comparable(from,to) ||
59-
// (from->is_function_call() || from->is_end_function())
60-
61-
virtual void transform(
62-
locationt from,
63-
locationt to,
64-
ai_baset &ai,
65-
const namespacet &ns) = 0;
66-
67-
virtual void output(
68-
std::ostream &out,
69-
const ai_baset &ai,
70-
const namespacet &ns) const
71-
{
72-
}
73-
74-
virtual jsont output_json(
75-
const ai_baset &ai,
76-
const namespacet &ns) const;
77-
78-
virtual xmlt output_xml(
79-
const ai_baset &ai,
80-
const namespacet &ns) const;
81-
82-
// no states
83-
virtual void make_bottom()=0;
84-
85-
// all states -- the analysis doesn't use this,
86-
// and domains may refuse to implement it.
87-
virtual void make_top()=0;
88-
89-
// a reasonable entry-point state
90-
virtual void make_entry()=0;
91-
92-
virtual bool is_bottom() const=0;
93-
94-
virtual bool is_top() const=0;
95-
96-
// also add
97-
//
98-
// bool merge(const T &b, locationt from, locationt to);
99-
//
100-
// This computes the join between "this" and "b".
101-
// Return true if "this" has changed.
102-
// In the usual case, "b" is the updated state after "from"
103-
// and "this" is the state before "to".
104-
//
105-
// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
106-
// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
107-
108-
// This method allows an expression to be simplified / evaluated using the
109-
// current state. It is used to evaluate assertions and in program
110-
// simplification
111-
112-
// return true if unchanged
113-
virtual bool ai_simplify(
114-
exprt &condition,
115-
const namespacet &ns) const
116-
{
117-
return true;
118-
}
119-
120-
// Simplifies the expression but keeps it as an l-value
121-
virtual bool ai_simplify_lhs(
122-
exprt &condition,
123-
const namespacet &ns) const;
124-
};
26+
#include "ai_domain.h"
12527

12628
// don't use me -- I am just a base class
12729
// use ait instead

‎src/analyses/ai_domain.cpp

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
/*******************************************************************\
2+
3+
Module: Abstract Interpretation
4+
5+
Author: Martin Brain, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Abstract Interpretation Domain
11+
12+
#include "ai_domain.h"
13+
14+
#include <util/simplify_expr.h>
15+
16+
jsont ai_domain_baset::output_json(
17+
const ai_baset &ai,
18+
const namespacet &ns) const
19+
{
20+
std::ostringstream out;
21+
output(out, ai, ns);
22+
json_stringt json(out.str());
23+
return json;
24+
}
25+
26+
xmlt ai_domain_baset::output_xml(
27+
const ai_baset &ai,
28+
const namespacet &ns) const
29+
{
30+
std::ostringstream out;
31+
output(out, ai, ns);
32+
xmlt xml("abstract_state");
33+
xml.data=out.str();
34+
return xml;
35+
}
36+
37+
/// Use the information in the domain to simplify the expression on the LHS of
38+
/// an assignment. This for example won't simplify symbols to their values, but
39+
/// does simplify indices in arrays, members of structs and dereferencing of
40+
/// pointers
41+
/// \param condition: the expression to simplify
42+
/// \param ns: the namespace
43+
/// \return True if condition did not change. False otherwise. condition will be
44+
/// updated with the simplified condition if it has worked
45+
bool ai_domain_baset::ai_simplify_lhs(
46+
exprt &condition, const namespacet &ns) const
47+
{
48+
// Care must be taken here to give something that is still writable
49+
if(condition.id()==ID_index)
50+
{
51+
index_exprt ie=to_index_expr(condition);
52+
bool no_simplification=ai_simplify(ie.index(), ns);
53+
if(!no_simplification)
54+
condition=simplify_expr(ie, ns);
55+
56+
return no_simplification;
57+
}
58+
else if(condition.id()==ID_dereference)
59+
{
60+
dereference_exprt de=to_dereference_expr(condition);
61+
bool no_simplification=ai_simplify(de.pointer(), ns);
62+
if(!no_simplification)
63+
condition=simplify_expr(de, ns); // So *(&x) -> x
64+
65+
return no_simplification;
66+
}
67+
else if(condition.id()==ID_member)
68+
{
69+
member_exprt me=to_member_expr(condition);
70+
// Since simplify_ai_lhs is required to return an addressable object
71+
// (so remains a valid left hand side), to simplify
72+
// `(something_simplifiable).b` we require that `something_simplifiable`
73+
// must also be addressable
74+
bool no_simplification=ai_simplify_lhs(me.compound(), ns);
75+
if(!no_simplification)
76+
condition=simplify_expr(me, ns);
77+
78+
return no_simplification;
79+
}
80+
else
81+
return true;
82+
}

‎src/analyses/ai_domain.h

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
/*******************************************************************\
2+
3+
Module: Abstract Interpretation
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Abstract Interpretation Domain
11+
12+
#ifndef CPROVER_ANALYSES_AI_DOMAIN_H
13+
#define CPROVER_ANALYSES_AI_DOMAIN_H
14+
15+
#include <util/json.h>
16+
#include <util/xml.h>
17+
#include <util/expr.h>
18+
#include <util/make_unique.h>
19+
20+
#include <goto-programs/goto_model.h>
21+
22+
// forward reference
23+
class ai_baset;
24+
25+
// don't use me -- I am just a base class
26+
// please derive from me
27+
class ai_domain_baset
28+
{
29+
public:
30+
// The constructor is expected to produce 'false'
31+
// or 'bottom'
32+
ai_domain_baset()
33+
{
34+
}
35+
36+
virtual ~ai_domain_baset()
37+
{
38+
}
39+
40+
typedef goto_programt::const_targett locationt;
41+
42+
// how function calls are treated:
43+
// a) there is an edge from each call site to the function head
44+
// b) there is an edge from the last instruction (END_FUNCTION)
45+
// of the function to the instruction _following_ the call site
46+
// (this also needs to set the LHS, if applicable)
47+
//
48+
// "this" is the domain before the instruction "from"
49+
// "from" is the instruction to be interpretted
50+
// "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
51+
//
52+
// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
53+
// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
54+
// PRECONDITION(are_comparable(from,to) ||
55+
// (from->is_function_call() || from->is_end_function())
56+
57+
virtual void transform(
58+
locationt from,
59+
locationt to,
60+
ai_baset &ai,
61+
const namespacet &ns) = 0;
62+
63+
virtual void output(
64+
std::ostream &out,
65+
const ai_baset &ai,
66+
const namespacet &ns) const
67+
{
68+
}
69+
70+
virtual jsont output_json(
71+
const ai_baset &ai,
72+
const namespacet &ns) const;
73+
74+
virtual xmlt output_xml(
75+
const ai_baset &ai,
76+
const namespacet &ns) const;
77+
78+
// no states
79+
virtual void make_bottom()=0;
80+
81+
// all states -- the analysis doesn't use this,
82+
// and domains may refuse to implement it.
83+
virtual void make_top()=0;
84+
85+
// a reasonable entry-point state
86+
virtual void make_entry()=0;
87+
88+
virtual bool is_bottom() const=0;
89+
90+
virtual bool is_top() const=0;
91+
92+
// also add
93+
//
94+
// bool merge(const T &b, locationt from, locationt to);
95+
//
96+
// This computes the join between "this" and "b".
97+
// Return true if "this" has changed.
98+
// In the usual case, "b" is the updated state after "from"
99+
// and "this" is the state before "to".
100+
//
101+
// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
102+
// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
103+
104+
// This method allows an expression to be simplified / evaluated using the
105+
// current state. It is used to evaluate assertions and in program
106+
// simplification
107+
108+
// return true if unchanged
109+
virtual bool ai_simplify(
110+
exprt &condition,
111+
const namespacet &ns) const
112+
{
113+
return true;
114+
}
115+
116+
// Simplifies the expression but keeps it as an l-value
117+
virtual bool ai_simplify_lhs(
118+
exprt &condition,
119+
const namespacet &ns) const;
120+
};
121+
122+
#endif

0 commit comments

Comments
 (0)