-
Notifications
You must be signed in to change notification settings - Fork 139
/
Fact.h
164 lines (122 loc) · 5.38 KB
/
Fact.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
// -*- mode: C++ -*-
//
// Copyright (c) 2007, 2008, 2009, 2010, 2011, 2015 The University of Utah
// All rights reserved.
//
// This file is part of `csmith', a random generator of C programs.
//
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions are met:
//
// * Redistributions of source code must retain the above copyright notice,
// this list of conditions and the following disclaimer.
//
// * Redistributions in binary form must reproduce the above copyright
// notice, this list of conditions and the following disclaimer in the
// documentation and/or other materials provided with the distribution.
//
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
// POSSIBILITY OF SUCH DAMAGE.
#ifndef FACT_H
#define FACT_H
///////////////////////////////////////////////////////////////////////////////
#include <ostream>
#include <vector>
using namespace std;
enum eFactCategory {
ePointTo=1,
eUnionWrite=2,
/* todo
eIntRange=8,
eEquality=16,
eAlias=32,
*/
};
class Statement;
class StatementAssign;
class StatementReturn;
class Variable;
class Expression;
class Lhs;
class Function;
class ExpressionVariable;
///////////////////////////////////////////////////////////////////////////////
class Fact
{
public:
Fact(eFactCategory e);
virtual ~Fact(void);
virtual Fact* clone(void) const = 0;
virtual int join(const Fact& /*fact*/) {return 0; };
virtual int join_visits(const Fact& fact) { return join(fact);}
virtual bool imply(const Fact& /*fact*/) const = 0;
// lattice functions
virtual bool is_top(void) const = 0;
virtual bool is_bottom(void) const = 0;
virtual void set_top(void) = 0;
virtual void set_bottom(void) = 0;
virtual bool is_assertable(const Statement* s) const = 0;
virtual bool is_related(const Fact& fact) const { return eCat == fact.eCat && get_var() == fact.get_var();}
virtual bool equal(const Fact& fact) const { return this == &fact; };
virtual void Output(std::ostream &out) const = 0;
virtual void OutputAssertion(std::ostream &out, const Statement* s = NULL) const;
virtual const Variable* get_var(void) const { return 0;};
/// Given existing facts, LHS and RHS of the assignment, derive the new facts,
/// and return the number of possible assignees. In most cases that's 1. But
/// if LHS is a pointer dereference, the number of assignees could > 1 depending
/// on the points-to analysis.
virtual int abstract_fact_for_assign(const std::vector<const Fact*>& /*facts*/, const Lhs* /*lhs*/, const Expression* /*rhs*/, std::vector<const Fact*>&) = 0;
virtual vector<const Fact*> abstract_fact_for_return(const std::vector<const Fact*>& facts, const ExpressionVariable* expr, const Function* func);
vector<const Fact*> abstract_fact_for_var_init(const Variable* v);
static void doFinalization();
enum eFactCategory eCat;
protected:
// keep track all created facts. used for releasing memory in doFinalization
static std::vector<Fact*> facts_;
};
///////////////////////////////////////////////////////////////////////////////
typedef std::vector<const Fact*> FactVec;
typedef FactVec* FactVecP;
/******************* Fact Manipulating Functions **********************/
/* find a fact from facts env */
int find_fact(const FactVec& facts, const Fact* fact);
/* find a specific type of fact (same variable most likely) from facts env */
const Fact* find_related_fact(const FactVec& facts, const Fact* new_fact);
const Fact* find_related_fact(const vector<Fact*>& facts, const Fact* new_fact);
/* merge a fact into env */
bool merge_fact(FactVec& facts, const Fact* new_fact);
/* merge two facts env */
bool merge_facts(FactVec& facts, const FactVec& new_facts);
/* check if two facts env are identical */
bool same_facts(const FactVec& facts1, const FactVec& facts2);
/* check if one facts env is a subset of the other */
bool subset_facts(const FactVec& facts1, const FactVec& facts2);
/* renew a fact in env (append is absent) */
bool renew_fact(FactVec& facts, const Fact* new_fact);
/* renew facts in new_facts into existing facts env */
bool renew_facts(FactVec& facts, const FactVec& new_facts);
/* clone an env */
vector<Fact*> copy_facts(const FactVec& facts_in);
/* combine facts in two env, discard facts not exist in one of them */
void combine_facts(vector<Fact*>& facts1, const FactVec& facts2);
/* add a new variable fact to env */
void add_new_var_fact(const Variable* v, FactVec& facts);
/* print facts env */
void print_facts(const FactVec& facts);
/* print fact(s) in env regarding a given variable */
void print_var_fact(const FactVec& facts, const char* vname);
#endif // FACT_H
// Local Variables:
// c-basic-offset: 4
// tab-width: 4
// End:
// End of file.