1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 dl_instruction.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Krystof Hoder (t-khoder) 2010-09-14. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include<iostream> 22 #include<string> 23 #include<utility> 24 #include "ast/ast.h" 25 #include "util/vector.h" 26 #include "muz/rel/dl_base.h" 27 #include "muz/base/dl_costs.h" 28 #include "muz/base/dl_context.h" 29 30 namespace datalog { 31 32 class instruction_block; 33 class rel_context; 34 check_overflow(unsigned i)35 inline void check_overflow(unsigned i) { 36 if (i == UINT_MAX) { 37 throw out_of_memory_error(); 38 } 39 } 40 41 // ----------------------------------- 42 // 43 // execution_context 44 // 45 // ----------------------------------- 46 47 class execution_context { 48 public: 49 typedef relation_base * reg_type; 50 typedef vector<reg_type> reg_vector; 51 typedef unsigned reg_idx; 52 53 /** 54 \brief A register number that should never be referenced to. Can stand e.g. for a tail 55 table in a rule with no tail. 56 */ 57 static const reg_idx void_register = UINT_MAX; 58 private: 59 typedef u_map<std::string> reg_annotations; 60 61 context & m_context; 62 reg_vector m_registers; 63 64 reg_annotations m_reg_annotation; 65 stopwatch * m_stopwatch; 66 unsigned m_timelimit_ms; //zero means no limit 67 public: 68 execution_context(context & context); 69 ~execution_context(); 70 71 void reset(); 72 73 rel_context & get_rel_context(); 74 rel_context const & get_rel_context() const; 75 76 void set_timelimit(unsigned time_in_ms); 77 void reset_timelimit(); 78 bool should_terminate(); 79 80 struct stats { 81 unsigned m_join; 82 unsigned m_project; 83 unsigned m_filter; 84 unsigned m_total; 85 unsigned m_unary_singleton; 86 unsigned m_filter_by_negation; 87 unsigned m_select_equal_project; 88 unsigned m_join_project; 89 unsigned m_project_rename; 90 unsigned m_union; 91 unsigned m_filter_interp_project; 92 unsigned m_filter_id; 93 unsigned m_filter_eq; 94 unsigned m_min; statsstats95 stats() { reset(); } resetstats96 void reset() { memset(this, 0, sizeof(*this)); } 97 }; 98 stats m_stats; 99 100 void collect_statistics(statistics& st) const; 101 102 /** 103 \brief Return reference to \c i -th register that contains pointer to a relation. 104 105 If register contains zero, it should be treated as if it contains an empty relation. 106 */ reg(reg_idx i)107 reg_type reg(reg_idx i) const { 108 if (i >= m_registers.size()) { 109 return nullptr; 110 } 111 return m_registers[i]; 112 } 113 /** 114 \brief Return value of the register and assign zero into it place. 115 */ release_reg(reg_idx i)116 reg_type release_reg(reg_idx i) { 117 SASSERT(i < m_registers.size()); 118 SASSERT(m_registers[i]); 119 reg_type res = m_registers[i]; 120 m_registers[i] = 0; 121 return res; 122 } 123 124 /** 125 \brief Assign value to a register. If it was non-empty, deallocate its content first. 126 */ set_reg(reg_idx i,reg_type val)127 void set_reg(reg_idx i, reg_type val) { 128 if (i >= m_registers.size()) { 129 check_overflow(i); 130 m_registers.resize(i+1); 131 } 132 if (m_registers[i]) { 133 m_registers[i]->deallocate(); 134 } 135 m_registers[i] = val; 136 } 137 make_empty(reg_idx i)138 void make_empty(reg_idx i) { 139 if (reg(i)) { 140 set_reg(i, nullptr); 141 } 142 } 143 register_count()144 unsigned register_count() const { 145 return m_registers.size(); 146 } 147 get_register_annotation(reg_idx reg,std::string & res)148 bool get_register_annotation(reg_idx reg, std::string & res) const { 149 return m_reg_annotation.find(reg, res); 150 } 151 set_register_annotation(reg_idx reg,const std::string & str)152 void set_register_annotation(reg_idx reg, const std::string & str) { 153 m_reg_annotation.insert(reg, str); 154 } 155 156 void report_big_relations(unsigned threshold, std::ostream & out) const; 157 }; 158 159 160 161 // ----------------------------------- 162 // 163 // instruction 164 // 165 // ----------------------------------- 166 167 168 /** 169 \brief Base class for instructions used in datalog saturation. 170 171 A relation in a register is owned by that register and is not referenced from anywhere else. 172 173 Instructions that move context of one register to another leave the source register empty 174 and deallocate the previous content of the target register. 175 */ 176 class instruction : public accounted_object { 177 typedef u_map<base_relation_fn *> fn_cache; 178 179 fn_cache m_fn_cache; 180 181 182 static const int rk_encode_base = 1024; 183 encode_kind(family_id k)184 inline static unsigned encode_kind(family_id k) 185 { SASSERT(k<rk_encode_base); return k; } encode_kinds(family_id k1,family_id k2)186 inline static unsigned encode_kinds(family_id k1, family_id k2) 187 { SASSERT(k1<rk_encode_base && k2<rk_encode_base); return (k1+1)*rk_encode_base + k2; } encode_kinds(family_id k1,family_id k2,family_id k3)188 inline static unsigned encode_kinds(family_id k1, family_id k2, family_id k3) { 189 SASSERT(k1<rk_encode_base && k2<rk_encode_base && k3<rk_encode_base); 190 return ((k1+1)*rk_encode_base + k2)*rk_encode_base + k3; 191 } 192 193 protected: 194 friend class instruction_block; 195 196 template<typename T> find_fn(const relation_base & r,T * & result)197 bool find_fn(const relation_base & r, T* & result) const 198 { return m_fn_cache.find(encode_kind(r.get_kind()), reinterpret_cast<base_relation_fn*&>(result)); } 199 200 template<typename T> find_fn(const relation_base & r1,const relation_base & r2,T * & result)201 bool find_fn(const relation_base & r1, const relation_base & r2, T*& result) const 202 { return m_fn_cache.find(encode_kinds(r1.get_kind(), r2.get_kind()), reinterpret_cast<base_relation_fn*&>(result)); } 203 204 template<typename T> find_fn(const relation_base & r1,const relation_base & r2,const relation_base & r3,T * & result)205 bool find_fn(const relation_base & r1, const relation_base & r2, const relation_base & r3, T * & result) const 206 { return m_fn_cache.find(encode_kinds(r1.get_kind(), r2.get_kind(), r3.get_kind()), reinterpret_cast<base_relation_fn*&>(result)); } 207 store_fn(const relation_base & r,base_relation_fn * fn)208 void store_fn(const relation_base & r, base_relation_fn * fn) 209 { m_fn_cache.insert(encode_kind(r.get_kind()), fn); } store_fn(const relation_base & r1,const relation_base & r2,base_relation_fn * fn)210 void store_fn(const relation_base & r1, const relation_base & r2, base_relation_fn * fn) 211 { m_fn_cache.insert(encode_kinds(r1.get_kind(), r2.get_kind()), fn); } store_fn(const relation_base & r1,const relation_base & r2,const relation_base & r3,base_relation_fn * fn)212 void store_fn(const relation_base & r1, const relation_base & r2, const relation_base & r3, 213 base_relation_fn * fn) 214 { m_fn_cache.insert(encode_kinds(r1.get_kind(), r2.get_kind(), r3.get_kind()), fn); } 215 216 /** 217 Process not only costs associated with the current instruction, but in case of 218 block instructions, process also costs associated with its child instructions. 219 */ 220 virtual void process_all_costs(); 221 222 /** 223 \brief Output one line header of the current instruction. 224 225 The newline character at the end should not be printed. 226 */ display_head_impl(execution_context const & ctx,std::ostream & out)227 virtual std::ostream& display_head_impl(execution_context const & ctx, std::ostream & out) const { 228 return out << "<instruction>"; 229 } 230 /** 231 \brief If relevant, output the body of the current instruction. 232 233 Each line must be prepended by \c indentation and ended by a newline character. 234 */ display_body_impl(execution_context const & ctx,std::ostream & out,const std::string & indentation)235 virtual void display_body_impl(execution_context const & ctx, std::ostream & out, const std::string & indentation) const {} 236 void log_verbose(execution_context& ctx); 237 238 public: 239 typedef execution_context::reg_type reg_type; 240 typedef execution_context::reg_idx reg_idx; 241 242 virtual ~instruction(); 243 244 virtual bool perform(execution_context & ctx) = 0; 245 246 virtual void make_annotations(execution_context & ctx) = 0; 247 display(execution_context const & ctx,std::ostream & out)248 void display(execution_context const& ctx, std::ostream & out) const { 249 display_indented(ctx, out, ""); 250 } 251 void display_indented(execution_context const & ctx, std::ostream & out, const std::string & indentation) const; 252 253 static instruction * mk_load(ast_manager & m, func_decl * pred, reg_idx tgt); 254 /** 255 \brief The store operation moves the relation from a register into the context. The register 256 is set to zero after the operation. 257 */ 258 static instruction * mk_store(ast_manager & m, func_decl * pred, reg_idx src); 259 static instruction * mk_dealloc(reg_idx reg); //maybe not necessary 260 static instruction * mk_clone(reg_idx from, reg_idx to); 261 static instruction * mk_move(reg_idx from, reg_idx to); 262 263 /** 264 \brief Return instruction that performs \c body as long as at least one register 265 in \c control_regs contains non-empty relation. 266 267 The instruction object takes over the ownership of the \c body object. 268 */ 269 static instruction * mk_while_loop(unsigned control_reg_cnt, const reg_idx * control_regs, 270 instruction_block * body); 271 272 static instruction * mk_join(reg_idx rel1, reg_idx rel2, unsigned col_cnt, 273 const unsigned * cols1, const unsigned * cols2, reg_idx result); 274 static instruction * mk_filter_equal(ast_manager & m, reg_idx reg, const relation_element & value, unsigned col); 275 static instruction * mk_filter_identical(reg_idx reg, unsigned col_cnt, const unsigned * identical_cols); 276 static instruction * mk_filter_interpreted(reg_idx reg, app_ref & condition); 277 static instruction * mk_filter_interpreted_and_project(reg_idx src, app_ref & condition, 278 unsigned col_cnt, const unsigned * removed_cols, reg_idx result); 279 static instruction * mk_union(reg_idx src, reg_idx tgt, reg_idx delta); 280 static instruction * mk_widen(reg_idx src, reg_idx tgt, reg_idx delta); 281 static instruction * mk_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols, 282 reg_idx tgt); 283 static instruction * mk_join_project(reg_idx rel1, reg_idx rel2, unsigned joined_col_cnt, 284 const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, 285 const unsigned * removed_cols, reg_idx result); 286 static instruction * mk_min(reg_idx source, reg_idx target, const unsigned_vector & group_by_cols, 287 unsigned min_col); 288 static instruction * mk_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle, 289 reg_idx tgt); 290 static instruction * mk_filter_by_negation(reg_idx tgt, reg_idx neg_rel, unsigned col_cnt, 291 const unsigned * cols1, const unsigned * cols2); 292 static instruction * mk_select_equal_and_project(ast_manager & m, reg_idx src, 293 const relation_element & value, unsigned col, reg_idx result); 294 295 static instruction * mk_unary_singleton(ast_manager & m, func_decl* pred, const relation_sort & s, const relation_element & val, reg_idx tgt); 296 static instruction * mk_total(const relation_signature & sig, func_decl* pred, reg_idx tgt); 297 298 /** 299 \brief The mark_saturated instruction marks a relation as saturated, so that after 300 next restart it does not have to be part of the saturation again. 301 */ 302 static instruction * mk_mark_saturated(ast_manager & m, func_decl * pred); 303 304 static instruction * mk_assert_signature(const relation_signature & s, reg_idx tgt); 305 306 void collect_statistics(statistics& st) const; 307 308 }; 309 310 311 // ----------------------------------- 312 // 313 // instruction_block 314 // 315 // ----------------------------------- 316 317 class instruction_block { 318 public: 319 struct instruction_observer { ~instruction_observerinstruction_observer320 virtual ~instruction_observer() {} notifyinstruction_observer321 virtual void notify(instruction * i) {} 322 }; 323 private: 324 typedef ptr_vector<instruction> instr_seq_type; 325 instr_seq_type m_data; 326 instruction_observer* m_observer; 327 public: instruction_block()328 instruction_block() : m_observer(nullptr) {} 329 ~instruction_block(); 330 void reset(); 331 push_back(instruction * i)332 void push_back(instruction * i) { 333 m_data.push_back(i); 334 if (m_observer) { 335 m_observer->notify(i); 336 } 337 } set_observer(instruction_observer * o)338 void set_observer(instruction_observer * o) { 339 SASSERT(o==0 || m_observer==0); 340 m_observer = o; 341 } 342 343 void collect_statistics(statistics& st) const; 344 345 /** 346 \brief Perform instructions in the block. If the run was interrupted before completion, 347 return false; otherwise return true. 348 349 The execution can terminate before completion if the function 350 \c execution_context::should_terminate() returns true. 351 */ 352 bool perform(execution_context & ctx) const; 353 354 void process_all_costs(); 355 356 void make_annotations(execution_context & ctx); 357 display(execution_context const & ctx,std::ostream & out)358 void display(execution_context const & ctx, std::ostream & out) const { 359 display_indented(ctx, out, ""); 360 } 361 void display_indented(execution_context const & ctx, std::ostream & out, const std::string & indentation) const; 362 num_instructions()363 unsigned num_instructions() const { return m_data.size(); } 364 }; 365 366 367 }; 368 369 370