OILS / vendor / souffle / provenance / Explain.h View on Github | oilshell.org

649 lines, 371 significant
1/*
2 * Souffle - A Datalog Compiler
3 * Copyright (c) 2017, The Souffle Developers. All rights reserved
4 * Licensed under the Universal Permissive License v 1.0 as shown at:
5 * - https://opensource.org/licenses/UPL
6 * - <souffle root>/licenses/SOUFFLE-UPL.txt
7 */
8
9/************************************************************************
10 *
11 * @file Explain.h
12 *
13 * Provenance interface for Souffle; works for compiler and interpreter
14 *
15 ***********************************************************************/
16
17#pragma once
18
19#include "souffle/provenance/ExplainProvenance.h"
20#include "souffle/provenance/ExplainProvenanceImpl.h"
21#include "souffle/provenance/ExplainTree.h"
22#include <algorithm>
23#include <csignal>
24#include <cstdio>
25#include <fstream>
26#include <iostream>
27#include <map>
28#include <memory>
29#include <regex>
30#include <string>
31#include <utility>
32#include <vector>
33#include <unistd.h>
34
35#ifdef USE_NCURSES
36#include <ncurses.h>
37#endif
38
39#define MAX_TREE_HEIGHT 500
40#define MAX_TREE_WIDTH 500
41
42namespace souffle {
43class SouffleProgram;
44
45class ExplainConfig {
46public:
47 /* Deleted copy constructor */
48 ExplainConfig(const ExplainConfig&) = delete;
49
50 /* Deleted assignment operator */
51 ExplainConfig& operator=(const ExplainConfig&) = delete;
52
53 /* Obtain the global ExplainConfiguration */
54 static ExplainConfig& getExplainConfig() {
55 static ExplainConfig config;
56 return config;
57 }
58
59 /* Configuration variables */
60 Own<std::ostream> outputStream = nullptr;
61 bool json = false;
62 int depthLimit = 4;
63
64private:
65 ExplainConfig() = default;
66};
67
68class Explain {
69public:
70 ExplainProvenance& prov;
71
72 Explain(ExplainProvenance& prov) : prov(prov) {}
73 ~Explain() = default;
74
75 /* Process a command, a return value of true indicates to continue, returning false indicates to break (if
76 * the command is q/exit) */
77 bool processCommand(std::string& commandLine) {
78 std::vector<std::string> command = split(commandLine, ' ', 1);
79
80 if (command.empty()) {
81 return true;
82 }
83
84 if (command[0] == "setdepth") {
85 if (command.size() != 2) {
86 printError("Usage: setdepth <depth>\n");
87 return true;
88 }
89 try {
90 ExplainConfig::getExplainConfig().depthLimit = std::stoi(command[1]);
91 } catch (std::exception& e) {
92 printError("<" + command[1] + "> is not a valid depth\n");
93 return true;
94 }
95 printInfo("Depth is now " + std::to_string(ExplainConfig::getExplainConfig().depthLimit) + "\n");
96 } else if (command[0] == "explain") {
97 std::pair<std::string, std::vector<std::string>> query;
98 if (command.size() != 2) {
99 printError("Usage: explain relation_name(\"<string element1>\", <number element2>, ...)\n");
100 return true;
101 }
102 query = parseTuple(command[1]);
103 printTree(prov.explain(query.first, query.second, ExplainConfig::getExplainConfig().depthLimit));
104 } else if (command[0] == "subproof") {
105 std::pair<std::string, std::vector<std::string>> query;
106 int label = -1;
107 if (command.size() <= 1) {
108 printError("Usage: subproof relation_name(<label>)\n");
109 return true;
110 }
111 query = parseTuple(command[1]);
112 label = std::stoi(query.second[0]);
113 printTree(prov.explainSubproof(query.first, label, ExplainConfig::getExplainConfig().depthLimit));
114 } else if (command[0] == "explainnegation") {
115 std::pair<std::string, std::vector<std::string>> query;
116 if (command.size() != 2) {
117 printError(
118 "Usage: explainnegation relation_name(\"<string element1>\", <number element2>, "
119 "...)\n");
120 return true;
121 }
122 query = parseTuple(command[1]);
123
124 // a counter for the rule numbers
125 std::size_t i = 1;
126 std::string rules;
127
128 // if there are no rules, then this must be an EDB relation
129 if (prov.getRules(query.first).size() == 0) {
130 printInfo("The tuple would be an input fact!\n");
131 return true;
132 }
133
134 for (auto rule : prov.getRules(query.first)) {
135 rules += std::to_string(i) + ": ";
136 rules += rule;
137 rules += "\n\n";
138 i++;
139 }
140 printInfo(rules);
141
142 printPrompt("Pick a rule number: ");
143
144 std::string ruleNum = getInput();
145 auto variables = prov.explainNegationGetVariables(query.first, query.second, std::stoi(ruleNum));
146
147 // @ and @non_matching are special sentinel values returned by ExplainProvenance
148 if (variables.size() == 1 && variables[0] == "@") {
149 printInfo("The tuple exists, cannot explain negation of it!\n");
150 return true;
151 } else if (variables.size() == 1 && variables[0] == "@non_matching") {
152 printInfo("The variable bindings don't match, cannot explain!\n");
153 return true;
154 } else if (variables.size() == 1 && variables[0] == "@fact") {
155 printInfo("The rule is a fact!\n");
156 return true;
157 }
158
159 std::map<std::string, std::string> varValues;
160 for (auto var : variables) {
161 printPrompt("Pick a value for " + var + ": ");
162 varValues[var] = getInput();
163 }
164
165 printTree(prov.explainNegation(query.first, std::stoi(ruleNum), query.second, varValues));
166 } else if (command[0] == "rule" && command.size() == 2) {
167 auto query = split(command[1], ' ');
168 if (query.size() != 2) {
169 printError("Usage: rule <relation name> <rule number>\n");
170 return true;
171 }
172 try {
173 printInfo(prov.getRule(query[0], std::stoi(query[1])) + "\n");
174 } catch (std::exception& e) {
175 printError("Usage: rule <relation name> <rule number>\n");
176 }
177 } else if (command[0] == "measure") {
178 try {
179 printInfo(prov.measureRelation(command[1]));
180 } catch (std::exception& e) {
181 printError("Usage: measure <relation name>\n");
182 }
183 } else if (command[0] == "output") {
184 if (command.size() == 2) {
185 // assign a new filestream, the old one is deleted by unique_ptr
186 ExplainConfig::getExplainConfig().outputStream = mk<std::ofstream>(command[1]);
187 } else if (command.size() == 1) {
188 ExplainConfig::getExplainConfig().outputStream = nullptr;
189 } else {
190 printError("Usage: output [<filename>]\n");
191 }
192 } else if (command[0] == "format") {
193 if (command.size() == 2 && command[1] == "json") {
194 ExplainConfig::getExplainConfig().json = true;
195 } else if (command.size() == 2 && command[1] == "proof") {
196 ExplainConfig::getExplainConfig().json = false;
197 } else {
198 printError("Usage: format <json|proof>\n");
199 }
200 } else if (command[0] == "exit" || command[0] == "q" || command[0] == "quit") {
201 // close file stream so that output is actually written to file
202 printPrompt("Exiting explain\n");
203 return false;
204 } else if (command[0] == "query") {
205 // if there is no given relations, return directly
206 if (command.size() != 2) {
207 printError(
208 "Usage: query <relation1>(<element1>, <element2>, ...), "
209 "<relation2>(<element1>, <element2>, ...), ...\n");
210 return true;
211 }
212 // vector relations stores relation name, args pair parsed by parseQueryTuple()
213 std::vector<std::pair<std::string, std::vector<std::string>>> relations;
214 // regex for relation string
215 std::regex relationRegex(
216 "([a-zA-Z0-9_.-]*)[[:blank:]]*\\(([[:blank:]]*([0-9]+|\"[^\"]*\"|[a-zA-Z_][a-zA-Z_0-9]*)("
217 "[[:blank:]]*,[[:blank:]]*(["
218 "0-"
219 "9]+|\"[^\"]*\"|[a-zA-Z_][a-zA-Z_0-9]*))*)?\\)",
220 std::regex_constants::extended);
221 std::smatch relationMatcher;
222 std::string relationStr = command[1];
223 // use relationRegex to match each relation string and call parseQueryTuple() to parse the
224 // relation name and arguments
225 while (std::regex_search(relationStr, relationMatcher, relationRegex)) {
226 relations.push_back(parseQueryTuple(relationMatcher[0]));
227
228 // check return value for parseQueryTuple, return if relation name is empty string or tuple
229 // arguments is empty
230 if (relations.back().first.size() == 0 || relations.back().second.size() == 0) {
231 printError(
232 "Usage: query <relation1>(<element1>, <element2>, ...), "
233 "<relation2>(<element1>, <element2>, ...), ...\n");
234 return true;
235 }
236 relationStr = relationMatcher.suffix().str();
237 }
238
239 // is no valid relation can be identified, return directly
240 if (relations.size() == 0) {
241 printError(
242 "Usage: query <relation1>(<element1>, <element2>, ...), "
243 "<relation2>(<element1>, <element2>, ...), ...\n");
244 return true;
245 }
246
247 // call queryProcess function to process query
248 prov.queryProcess(relations);
249 } else {
250 printError(
251 "\n----------\n"
252 "Commands:\n"
253 "----------\n"
254 "setdepth <depth>: Set a limit for printed derivation tree height\n"
255 "explain <relation>(<element1>, <element2>, ...): Prints derivation tree\n"
256 "explainnegation <relation>(<element1>, <element2>, ...): Enters an interactive\n"
257 " interface where the non-existence of a tuple can be explained\n"
258 "subproof <relation>(<label>): Prints derivation tree for a subproof, label is\n"
259 " generated if a derivation tree exceeds height limit\n"
260 "rule <relation name> <rule number>: Prints a rule\n"
261 "output <filename>: Write output into a file, or provide empty filename to\n"
262 " disable output\n"
263 "format <json|proof>: switch format between json and proof-trees\n"
264 "query <relation1>(<element1>, <element2>, ...), <relation2>(<element1>, <element2>), "
265 "... :\n"
266 "check existence of constant tuples or find solutions for parameterised tuples\n"
267 "for parameterised query, use semicolon to find next solution and dot to break from "
268 "query\n"
269 "exit: Exits this interface\n\n");
270 }
271
272 return true;
273 }
274
275 /* The main explain call */
276 virtual void explain() = 0;
277
278private:
279 /* Get input */
280 virtual std::string getInput() = 0;
281
282 /* Print a command prompt, disabled for non-terminal outputs */
283 virtual void printPrompt(const std::string& prompt) = 0;
284
285 /* Print a tree */
286 virtual void printTree(Own<TreeNode> tree) = 0;
287
288 /* Print any other information, disabled for non-terminal outputs */
289 virtual void printInfo(const std::string& info) = 0;
290
291 /* Print an error, such as a wrong command */
292 virtual void printError(const std::string& error) = 0;
293
294 /**
295 * Parse tuple, split into relation name and values
296 * @param str The string to parse, should be something like "R(x1, x2, x3, ...)"
297 */
298 std::pair<std::string, std::vector<std::string>> parseTuple(const std::string& str) {
299 std::string relName;
300 std::vector<std::string> args;
301
302 // regex for matching tuples
303 // values matches numbers or strings enclosed in quotation marks
304 std::regex relationRegex(
305 "([a-zA-Z0-9_.-]*)[[:blank:]]*\\(([[:blank:]]*([0-9]+|\"[^\"]*\")([[:blank:]]*,[[:blank:]]*(["
306 "0-"
307 "9]+|\"[^\"]*\"))*)?\\)",
308 std::regex_constants::extended);
309 std::smatch relMatch;
310
311 // first check that format matches correctly
312 // and extract relation name
313 if (!std::regex_match(str, relMatch, relationRegex) || relMatch.size() < 3) {
314 return std::make_pair(relName, args);
315 }
316
317 // set relation name
318 relName = relMatch[1];
319
320 // extract each argument
321 std::string argsList = relMatch[2];
322 std::smatch argsMatcher;
323 std::regex argRegex(R"([0-9]+|"[^"]*")", std::regex_constants::extended);
324
325 while (std::regex_search(argsList, argsMatcher, argRegex)) {
326 // match the start of the arguments
327 std::string currentArg = argsMatcher[0];
328 args.push_back(currentArg);
329
330 // use the rest of the arguments
331 argsList = argsMatcher.suffix().str();
332 }
333
334 return std::make_pair(relName, args);
335 }
336
337 /**
338 * Parse tuple for query, split into relation name and args, additionally allow varaible as argument in
339 * relation tuple
340 * @param str The string to parse, should be in form "R(x1, x2, x3, ...)"
341 */
342 std::pair<std::string, std::vector<std::string>> parseQueryTuple(const std::string& str) {
343 std::string relName;
344 std::vector<std::string> args;
345 // regex for matching tuples
346 // values matches numbers or strings enclosed in quotation marks
347 std::regex relationRegex(
348 "([a-zA-Z0-9_.-]*)[[:blank:]]*\\(([[:blank:]]*([0-9]+|\"[^\"]*\"|[a-zA-Z_][a-zA-Z_0-9]*)([[:"
349 "blank:]]*,[[:blank:]]*(["
350 "0-"
351 "9]+|\"[^\"]*\"|[a-zA-Z_][a-zA-Z_0-9]*))*)?\\)",
352 std::regex_constants::extended);
353 std::smatch relMatch;
354
355 // if the given string does not match relationRegex, return a pair of empty string and empty vector
356 if (!std::regex_match(str, relMatch, relationRegex) || relMatch.size() < 3) {
357 return std::make_pair(relName, args);
358 }
359
360 // set relation name
361 relName = relMatch[1];
362
363 // extract each argument
364 std::string argsList = relMatch[2];
365 std::smatch argsMatcher;
366 std::regex argRegex(R"([0-9]+|"[^"]*"|[a-zA-Z_][a-zA-Z_0-9]*)", std::regex_constants::extended);
367 while (std::regex_search(argsList, argsMatcher, argRegex)) {
368 // match the start of the arguments
369 std::string currentArg = argsMatcher[0];
370 args.push_back(currentArg);
371
372 // use the rest of the arguments
373 argsList = argsMatcher.suffix().str();
374 }
375
376 return std::make_pair(relName, args);
377 }
378};
379
380class ExplainConsole : public Explain {
381public:
382 explicit ExplainConsole(ExplainProvenance& provenance) : Explain(provenance) {}
383
384 /* The main explain call */
385 void explain() override {
386 printPrompt("Explain is invoked.\n");
387
388 while (true) {
389 printPrompt("Enter command > ");
390 std::string line = getInput();
391 // a return value of false indicates that an exit/q command has been processed
392 if (!processCommand(line)) {
393 break;
394 }
395 }
396 }
397
398private:
399 /* Get input */
400 std::string getInput() override {
401 std::string line;
402
403 if (!getline(std::cin, line)) {
404 // if EOF has been reached, quit
405 line = "q";
406 }
407
408 return line;
409 }
410
411 /* Print a command prompt, disabled for non-terminal outputs */
412 void printPrompt(const std::string& prompt) override {
413 if (isatty(fileno(stdin)) == 0) {
414 return;
415 }
416 std::cout << prompt;
417 }
418
419 /* Print a tree */
420 void printTree(Own<TreeNode> tree) override {
421 if (!tree) {
422 return;
423 }
424
425 // handle a file ostream output
426 std::ostream* output;
427 if (ExplainConfig::getExplainConfig().outputStream == nullptr) {
428 output = &std::cout;
429 } else {
430 output = ExplainConfig::getExplainConfig().outputStream.get();
431 }
432
433 if (!ExplainConfig::getExplainConfig().json) {
434 tree->place(0, 0);
435 ScreenBuffer screenBuffer(tree->getWidth(), tree->getHeight());
436 tree->render(screenBuffer);
437 *output << screenBuffer.getString();
438 } else {
439 *output << "{ \"proof\":\n";
440 tree->printJSON(*output, 1);
441 *output << ",";
442 prov.printRulesJSON(*output);
443 *output << "}\n";
444 }
445 }
446
447 /* Print any other information, disabled for non-terminal outputs */
448 void printInfo(const std::string& info) override {
449 if (isatty(fileno(stdin)) == 0) {
450 return;
451 }
452 std::cout << info;
453 }
454
455 /* Print an error, such as a wrong command */
456 void printError(const std::string& error) override {
457 std::cout << error;
458 }
459};
460
461#ifdef USE_NCURSES
462class ExplainNcurses : public Explain {
463public:
464 explicit ExplainNcurses(ExplainProvenance& provenance) : Explain(provenance) {}
465
466 /* The main explain call */
467 void explain() override {
468 if (ExplainConfig::getExplainConfig().outputStream == nullptr) {
469 initialiseWindow();
470 std::signal(SIGWINCH, nullptr);
471 }
472
473 printPrompt("Explain is invoked.\n");
474
475 while (true) {
476 clearDisplay();
477 printPrompt("Enter command > ");
478 std::string line = getInput();
479
480 // a return value of false indicates that an exit/q command has been processed
481 if (!processCommand(line)) {
482 break;
483 }
484
485 // refresh treePad and allow scrolling
486 prefresh(treePad, 0, 0, 0, 0, maxy - 3, maxx - 1);
487 scrollTree(maxx, maxy);
488 }
489
490 // clean up
491 endwin();
492 }
493
494private:
495 WINDOW* treePad = nullptr;
496 WINDOW* queryWindow = nullptr;
497 int maxx, maxy;
498
499 /* Get input */
500 std::string getInput() override {
501 char buf[100];
502
503 curs_set(1);
504 echo();
505
506 // get next command
507 wgetnstr(queryWindow, buf, 100);
508 noecho();
509 curs_set(0);
510 std::string line = buf;
511
512 return line;
513 }
514
515 /* Print a command prompt, disabled for non-terminal outputs */
516 void printPrompt(const std::string& prompt) override {
517 if (!isatty(fileno(stdin))) {
518 return;
519 }
520 werase(queryWindow);
521 wrefresh(queryWindow);
522 mvwprintw(queryWindow, 1, 0, "%s", prompt.c_str());
523 }
524
525 /* Print a tree */
526 void printTree(Own<TreeNode> tree) override {
527 if (!tree) {
528 return;
529 }
530
531 if (!ExplainConfig::getExplainConfig().json) {
532 tree->place(0, 0);
533 ScreenBuffer screenBuffer(tree->getWidth(), tree->getHeight());
534 tree->render(screenBuffer);
535 wprintw(treePad, "%s", screenBuffer.getString().c_str());
536 } else {
537 if (ExplainConfig::getExplainConfig().outputStream == nullptr) {
538 std::stringstream ss;
539 ss << "{ \"proof\":\n";
540 tree->printJSON(ss, 1);
541 ss << ",";
542 prov.printRulesJSON(ss);
543 ss << "}\n";
544
545 wprintw(treePad, "%s", ss.str().c_str());
546 } else {
547 std::ostream* output = ExplainConfig::getExplainConfig().outputStream.get();
548 *output << "{ \"proof\":\n";
549 tree->printJSON(*output, 1);
550 *output << ",";
551 prov.printRulesJSON(*output);
552 *output << "}\n";
553 }
554 }
555 }
556
557 /* Print any other information, disabled for non-terminal outputs */
558 void printInfo(const std::string& info) override {
559 if (!isatty(fileno(stdin))) {
560 return;
561 }
562 wprintw(treePad, "%s", info.c_str());
563 prefresh(treePad, 0, 0, 0, 0, maxy - 3, maxx - 1);
564 }
565
566 /* Print an error, such as a wrong command */
567 void printError(const std::string& error) override {
568 wprintw(treePad, "%s", error.c_str());
569 prefresh(treePad, 0, 0, 0, 0, maxy - 3, maxx - 1);
570 }
571
572 /* Initialise ncurses command prompt window */
573 WINDOW* makeQueryWindow() {
574 WINDOW* queryWindow = newwin(3, maxx, maxy - 2, 0);
575 wrefresh(queryWindow);
576 return queryWindow;
577 }
578
579 /* Initialise ncurses window */
580 void initialiseWindow() {
581 initscr();
582
583 // get size of window
584 getmaxyx(stdscr, maxy, maxx);
585
586 // create windows for query and tree display
587 queryWindow = makeQueryWindow();
588 treePad = newpad(MAX_TREE_HEIGHT, MAX_TREE_WIDTH);
589
590 keypad(treePad, true);
591 }
592
593 /* Allow scrolling of provenance tree */
594 void scrollTree(int maxx, int maxy) {
595 int x = 0;
596 int y = 0;
597
598 while (true) {
599 int ch = wgetch(treePad);
600
601 if (ch == KEY_LEFT) {
602 if (x > 2) x -= 3;
603 } else if (ch == KEY_RIGHT) {
604 if (x < MAX_TREE_WIDTH - 3) x += 3;
605 } else if (ch == KEY_UP) {
606 if (y > 0) y -= 1;
607 } else if (ch == KEY_DOWN) {
608 if (y < MAX_TREE_HEIGHT - 1) y += 1;
609 } else {
610 ungetch(ch);
611 break;
612 }
613
614 prefresh(treePad, y, x, 0, 0, maxy - 3, maxx - 1);
615 }
616 }
617
618 /* Clear the tree display */
619 void clearDisplay() {
620 // reset tree display on each loop
621 werase(treePad);
622 prefresh(treePad, 0, 0, 0, 0, maxy - 3, maxx - 1);
623 }
624};
625#endif
626
627inline void explain(SouffleProgram& prog, bool ncurses) {
628 ExplainProvenanceImpl prov(prog);
629
630 if (ncurses) {
631#ifdef USE_NCURSES
632 ExplainNcurses exp(prov);
633 exp.explain();
634#else
635 std::cout << "The ncurses-based interface is not enabled\n";
636#endif
637 } else {
638 ExplainConsole exp(prov);
639 exp.explain();
640 }
641}
642
643// this is necessary because ncurses.h defines TRUE and FALSE macros, and they otherwise clash with our parser
644#ifdef USE_NCURSES
645#undef TRUE
646#undef FALSE
647#endif
648
649} // end of namespace souffle