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