1 // -*- mode: C++ -*- 2 // 3 // Copyright (c) 2007, 2008, 2009, 2010, 2011, 2015 The University of Utah 4 // All rights reserved. 5 // 6 // This file is part of `csmith', a random generator of C programs. 7 // 8 // Redistribution and use in source and binary forms, with or without 9 // modification, are permitted provided that the following conditions are met: 10 // 11 // * Redistributions of source code must retain the above copyright notice, 12 // this list of conditions and the following disclaimer. 13 // 14 // * Redistributions in binary form must reproduce the above copyright 15 // notice, this list of conditions and the following disclaimer in the 16 // documentation and/or other materials provided with the distribution. 17 // 18 // THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" 19 // AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE 20 // IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE 21 // ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE 22 // LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 23 // CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF 24 // SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS 25 // INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN 26 // CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) 27 // ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 28 // POSSIBILITY OF SUCH DAMAGE. 29 30 #ifdef WIN32 31 #pragma warning(disable : 4786) /* Disable annoying warning messages */ 32 #endif 33 34 #ifndef FACT_MGR_H 35 #define FACT_MGR_H 36 37 class StatementAssign; 38 class StatementIf; 39 class StatementReturn; 40 class StatementFor; 41 class StatementExpr; 42 class Block; 43 class Expression; 44 class Fact; 45 class Variable; 46 class Expression; 47 class Statement; 48 class Function; 49 class FunctionInvocationUser; 50 class CGContext; 51 class Lhs; 52 class CFGEdge; 53 54 /////////////////////////////////////////////////////////////////////////////// 55 56 #include <ostream> 57 #include <vector> 58 #include <map> 59 #include "Effect.h" 60 #include "Fact.h" 61 using namespace std; 62 63 /////////////////////////////////////////////////////////////////////////////// 64 65 class FactMgr 66 { 67 public: 68 FactMgr(const Function* f); 69 70 FactMgr(const Function* f, const FactVec& facts); 71 72 static void doFinalization(); 73 74 static void add_interested_facts(int interests); 75 76 ~FactMgr(void); 77 78 //FactMgr* clone(void); 79 80 bool validate_fact(const Fact* f, const FactVec& facts); 81 82 bool validate_assign(const Lhs* v, const Expression* e); 83 84 void restore_facts(vector<const Fact*>& old_facts); 85 86 void makeup_new_var_facts(vector<const Fact*>& old_facts, const vector<const Fact*>& new_facts); 87 88 void add_new_var_fact_and_update_inout_maps(const Block* blk, const Variable* var); 89 90 void setup_in_out_maps(bool first_time); 91 92 void set_fact_in(const Statement* s, const FactVec& facts); 93 void set_fact_out(const Statement* s, const FactVec& facts); 94 void add_fact_out(const Statement* stm, const Fact* fact); 95 96 void create_cfg_edge(const Statement* src, const Statement* dest, bool post_stm_edge, bool back_link); 97 98 void clear_map_visited(void); 99 void backup_stm_fact_maps(const Statement* stm, map<const Statement*, FactVec>& facts_in, map<const Statement*, FactVec>& facts_out); 100 void restore_stm_fact_maps(const Statement* stm, map<const Statement*, FactVec>& facts_in, map<const Statement*, FactVec>& facts_out); 101 void reset_stm_fact_maps(const Statement* stm); 102 103 void output_assertions(std::ostream &out, const Statement* stm, int indent, bool post_condition); 104 void find_updated_final_facts(const Statement* stm, vector<Fact*>& facts); 105 void find_updated_facts(const Statement* stm, vector<const Fact*>& facts); 106 107 void find_dangling_global_ptrs(Function* f); 108 109 /* add paramters facts to env */ 110 void add_param_facts(const vector<const Expression*>& param_values, FactVec& facts); 111 void caller_to_callee_handover(const FunctionInvocationUser* fiu, std::vector<const Fact*>& inputs); 112 113 /* remove facts related to return variables (except rv of this function) from env */ 114 void remove_rv_facts(FactVec& facts); 115 116 static void remove_loop_local_facts(const Statement* s, FactVec& facts); 117 /* remove facts localized to a given function up to a given return statement */ 118 static void remove_function_local_facts(std::vector<const Fact*>& inputs, const Statement* stm); 119 static bool merge_jump_facts(FactVec& facts, const FactVec& jump_facts); 120 /* add a new variable fact to env */ 121 static void add_new_var_fact(const Variable* v, FactVec& facts); 122 static const vector<const Fact*>& get_program_end_facts(void); 123 124 /* remove facts related to certain variables from env */ 125 static void update_facts_for_oos_vars(const vector<Variable*>& vars, FactVec& facts); 126 static void update_facts_for_oos_vars(const vector<const Variable*>& vars, FactVec& facts); 127 128 /* update fact(s) from assignments */ 129 static bool update_fact_for_assign(const StatementAssign* sa, FactVec& inputs); 130 static bool update_fact_for_assign(const Lhs* lhs, const Expression* rhs, FactVec& inputs); 131 132 /* update facts(s) from return statement */ 133 static void update_fact_for_return(const StatementReturn* sa, FactVec& inputs); 134 135 /* update fact(s) for a jump destination */ 136 static void update_facts_for_dest(const FactVec& facts_in, FactVec& facts_out, const Statement* dest); 137 138 void sanity_check_map() const; 139 140 static std::vector<Fact*> meta_facts; 141 142 // maps to track facts and effects at historical generation points. 143 // they are used for bypassing analyzing statements if possible 144 std::map<const Statement*, FactVec> map_facts_in; 145 std::map<const Statement*, FactVec> map_facts_out; 146 std::map<const Statement*, std::vector<Fact*> > map_facts_in_final; 147 std::map<const Statement*, std::vector<Fact*> > map_facts_out_final; 148 std::map<const Statement*, Effect> map_stm_effect; 149 std::map<const Statement*, Effect> map_accum_effect; 150 std::map<const Statement*, bool> map_visited; 151 152 std::vector<const CFGEdge*> cfg_edges; 153 FactVec global_facts; 154 155 const Function* func; 156 }; 157 158 /////////////////////////////////////////////////////////////////////////////// 159 160 #endif // FACT_MGR_H 161 162 // Local Variables: 163 // c-basic-offset: 4 164 // tab-width: 4 165 // End: 166 167 // End of file. 168