SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Database.h
Go to the documentation of this file.
1 /**
2  * @file Database.h
3  * @author Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
4  */
5 
6 #pragma once
7 
8 #include <filesystem>
9 
10 #ifdef BENCHMAX_DATABASE
11 // Include exactly one implementation.
13 //#include "Database_mysqlpp.h"
14 #endif
15 
16 #include "../logging.h"
17 #include "../tools/Tool.h"
18 
19 namespace benchmax {
20 
21 namespace fs = std::filesystem;
22 
23 #ifdef BENCHMAX_DATABASE
24 /**
25  * Database abstraction that allows to store benchmark results.
26  * Note that it does not abstract from the database (we assume MySQL) but only from the mysql library.
27  *
28  * Storing to database should be considered unstable!
29  */
30 class Database {
31  DBAL conn;
32 public:
33  /// Index type.
34  using Index = DBAL::Index;
35 
36  /// Add a new tool.
37  Index addTool(const Tool* tool) {
38  Index id = conn.insert("INSERT INTO main_tool (`interface`, `hash`) VALUES (%0q, %1q)", tool->name(), tool->attributeHash());
39  DBAL::Statement stmt = conn.prepare("INSERT INTO main_toolattribute (`key`, `value`, `tool_id`) VALUES (%0q, %1q, %2q)");
40  for (const auto& it: tool->attributes()) {
41  conn.execute(stmt, it.first, it.second, id);
42  }
43  return id;
44  }
45 
46  /// Get id of a tool.
47  Index getToolID(const Tool* tool) {
48  DBAL::Results res = conn.select("SELECT id FROM main_tool WHERE `interface` = %0q AND `hash` = %1q", tool->name(), tool->attributeHash());
49  if (conn.size(res) == 0) {
50  return addTool(tool);
51  }
52  assert(conn.size(res) == 1);
53  return conn.getIndex(res, "id");
54  }
55 
56  /// Add a new file.
57  Index addFile(const fs::path& file) {
58  return conn.insert("INSERT INTO main_file (`filename`) VALUES (%0q)", file.native());
59  }
60 
61  /// Get id of a file.
62  Index getFileID(const fs::path& file) {
63  DBAL::Results res = conn.select("SELECT id FROM main_file WHERE `filename` = %0q", file.native());
64  if (conn.size(res) == 0) {
65  return addFile(file);
66  }
67  assert(conn.size(res) == 1);
68  return conn.getIndex(res, "id");
69  }
70 
71  /// Create a new benchmark run.
73  return conn.insert("INSERT INTO main_benchmark () VALUES ()");
74  }
75 
76  /// Add results for an individual benchmark.
77  Index addBenchmarkResult(Index benchmark, Index tool, Index file, int exitCode, std::size_t time) {
78  return conn.insert("INSERT INTO main_benchmarkresult (`exitcode`, `time`, `memory`, `benchmark_id`, `tool_id`, `file_id`) VALUES (%0q, %1q, %2q, %3q, %4q, %5q)", exitCode, time, std::size_t(0), benchmark, tool, file);
79  }
80 
81  /// Add arbitrary attributes for a benchmark result.
82  void addBenchmarkAttribute(Index benchmarkResult, const std::string& key, const std::string& value) {
83  conn.insert("INSERT INTO main_benchmarkattribute (`key`, `value`, `result_id`) VALUES (%0q, %1q, %2q)", key, value, benchmarkResult);
84  }
85 
86  /// Establish database connection.
87  Database() {
88  if (!conn.connect("benchmarks", "ths.informatik.rwth-aachen.de", "benchmax", "Km2FLeJJ2wX3nMqq")) {
89  BENCHMAX_LOG_FATAL("benchmax.database", "Failed to connect to database.");
90  exit(1);
91  }
92  }
93 };
94 #else
95 /// Dummy database that effectively disables storing to database. Set BENCHMAX_DATABASE to actually use a database.
96 class Database {
97 public:
98  /// Dummy index type.
99  using Index = std::size_t;
100  /// Dummy.
101  Index addTool(const Tool*) { return 0; }
102  /// Dummy.
103  Index getToolID(const Tool*) { return 0; }
104  /// Dummy.
105  Index addFile(const fs::path&) { return 0; }
106  /// Dummy.
107  Index getFileID(const fs::path&) { return 0; }
108  /// Dummy.
109  Index createBenchmark() { return 0; }
110  /// Dummy.
111  Index addBenchmarkResult(Index, Index, Index, int, std::size_t) { return 0; }
112  /// Dummy.
113  void addBenchmarkAttribute(Index, const std::string&, const std::string&) {}
114 };
115 #endif
116 
117 }
#define BENCHMAX_LOG_FATAL(channel, msg)
Log fatal errors.
Definition: logging.h:47
std::unique_ptr< sql::ResultSet > Results
Results type.
std::unique_ptr< sql::PreparedStatement > Statement
Statement type.
std::size_t Index
Indec type.
Dummy database that effectively disables storing to database. Set BENCHMAX_DATABASE to actually use a...
Definition: Database.h:96
Index getToolID(const Tool *)
Dummy.
Definition: Database.h:103
void addBenchmarkAttribute(Index, const std::string &, const std::string &)
Dummy.
Definition: Database.h:113
Index createBenchmark()
Dummy.
Definition: Database.h:109
Index addBenchmarkResult(Index, Index, Index, int, std::size_t)
Dummy.
Definition: Database.h:111
Index getFileID(const fs::path &)
Dummy.
Definition: Database.h:107
std::size_t Index
Dummy index type.
Definition: Database.h:99
Index addTool(const Tool *)
Dummy.
Definition: Database.h:101
Index addFile(const fs::path &)
Dummy.
Definition: Database.h:105
Base class for any tool.
Definition: Tool.h:38