From d3908857576b25f0ae781bdac41a2e6bdd42eb7c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 6 Apr 2017 18:37:29 +0100 Subject: [PATCH] Added utility to compare quantifier instantiation profiles generated via smt.qi.profile=true --- contrib/qprofdiff/Makefile | 7 + contrib/qprofdiff/main.cpp | 238 ++++++++++++++++++++ contrib/qprofdiff/qprofdiff.vcxproj | 137 +++++++++++ contrib/qprofdiff/qprofdiff.vcxproj.filters | 22 ++ 4 files changed, 404 insertions(+) create mode 100644 contrib/qprofdiff/Makefile create mode 100644 contrib/qprofdiff/main.cpp create mode 100644 contrib/qprofdiff/qprofdiff.vcxproj create mode 100644 contrib/qprofdiff/qprofdiff.vcxproj.filters diff --git a/contrib/qprofdiff/Makefile b/contrib/qprofdiff/Makefile new file mode 100644 index 000000000..6b90bed51 --- /dev/null +++ b/contrib/qprofdiff/Makefile @@ -0,0 +1,7 @@ +qprofdiff: main.cpp + $(CXX) $(CXXFLAGS) main.cpp -o qprofdiff + +all: qprofdiff + +clean: + rm -f qprofdiff diff --git a/contrib/qprofdiff/main.cpp b/contrib/qprofdiff/main.cpp new file mode 100644 index 000000000..44c76b17d --- /dev/null +++ b/contrib/qprofdiff/main.cpp @@ -0,0 +1,238 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + main.cpp + +Abstract: + + Main file for qprofdiff. + +Author: + + Christoph M. Wintersteiger (cwinter) + +Revision History: +--*/ +#include + +#include +#include +#include +#include +#include +#include +#include + +using namespace std; + +set options; + +// Profile format: +// [quantifier_instances] qname : num_instances : max_generation : max_cost_s +const string prefix = "[quantifier_instances]"; +unsigned prefix_len = prefix.length(); +typedef struct { unsigned num_instances, max_generation, max_cost; } map_entry; + +string trim(string str) { + size_t linx = str.find_first_not_of(' '); + size_t rinx = str.find_last_not_of(' '); + return str.substr(linx, rinx-linx+1); +} + +int parse(string const & filename, map & data) { + ifstream fs(filename.c_str()); + + if (!fs.is_open()) { + cout << "Can't open file '" << filename << "'" << endl; + return ENOENT; + } + + string qid; + string tokens[4]; + unsigned cur_token = 0; + + while (!fs.eof()) { + string line; + getline(fs, line); + + if (line.substr(0, prefix_len) == prefix) { + line = trim(line.substr(prefix_len)); + size_t from = 0, ti = 0; + for (size_t inx = line.find(':', from); + inx != string::npos; + inx = line.find(':', from)) { + tokens[ti] = trim(line.substr(from, inx-from)); + from = inx+1; + ti++; + } + if (from != line.length() && ti < 4) + tokens[ti] = trim(line.substr(from)); + + qid = tokens[0]; + + if (data.find(qid) == data.end()) { + map_entry & entry = data[qid]; + entry.num_instances = entry.max_generation = entry.max_cost = 0; + } + + map_entry & entry = data[qid]; + entry.num_instances += atoi(tokens[1].c_str()); + entry.max_generation = std::max(entry.max_generation, (unsigned)atoi(tokens[2].c_str())); + entry.max_cost = max(entry.max_cost, (unsigned)atoi(tokens[3].c_str())); + } + } + + fs.close(); + + return 0; +} + +void display_data(map & data) { + for (map::iterator it = data.begin(); + it != data.end(); + it++) + cout << it->first << ": " << it->second.num_instances << + ", " << it->second.max_generation << + ", " << it->second.max_cost << endl; +} + + +typedef struct { int d_num_instances, d_max_generation, d_max_cost; } diff_entry; +typedef struct { string qid; diff_entry e; } diff_item; + +bool diff_item_lt_inst(diff_item const & l, diff_item const & r) { + return l.e.d_num_instances < r.e.d_num_instances; +} + +bool diff_item_lt_gen(diff_item const & l, diff_item const & r) { + return l.e.d_max_generation< r.e.d_max_generation; +} + +bool diff_item_lt_cost(diff_item const & l, diff_item const & r) { + return l.e.d_max_cost < r.e.d_max_cost; +} + +void display_indicator(int const & delta, bool suppress_unchanged) { + if (delta < 0) + cout << "+ "; + else if (delta > 0) + cout << "- "; + else if (delta == 0 && !suppress_unchanged) + cout << "= "; +} + +void diff(map & left, map & right) { + map diff_data; + + for (map::const_iterator lit = left.begin(); + lit != left.end(); + lit++) { + string const & qid = lit->first; + map_entry const & lentry = lit->second; + + map::const_iterator rit = right.find(qid); + if (rit != right.end()) { + map_entry const & rentry = rit->second; + + diff_entry & de = diff_data[qid]; + de.d_num_instances = lentry.num_instances - rentry.num_instances; + de.d_max_generation = lentry.max_generation - rentry.max_generation; + de.d_max_cost = lentry.max_cost - rentry.max_cost; + } + } + + vector flat_data; + for (map::const_iterator it = diff_data.begin(); + it != diff_data.end(); + it++) { + flat_data.push_back(diff_item()); + flat_data.back().qid = it->first; + flat_data.back().e = it->second; + } + + stable_sort(flat_data.begin(), flat_data.end(), + options.find("-si") != options.end() ? diff_item_lt_inst : + options.find("-sg") != options.end() ? diff_item_lt_gen : + options.find("-sc") != options.end() ? diff_item_lt_cost : + diff_item_lt_inst); + + bool suppress_unchanged = options.find("-n") != options.end(); + + for (vector::const_iterator it = flat_data.begin(); + it != flat_data.end(); + it++) { + diff_item const & d = *it; + string const & qid = d.qid; + diff_entry const & e = d.e; + + int const & delta = + (options.find("-si") != options.end()) ? e.d_num_instances : + (options.find("-sg") != options.end()) ? e.d_max_generation : + (options.find("-sc") != options.end()) ? e.d_max_cost : + e.d_num_instances; + + display_indicator(delta, suppress_unchanged); + + if (delta != 0 || !suppress_unchanged) + cout << qid << " (" << + (e.d_num_instances > 0 ? "" : "+") << -e.d_num_instances << " inst., " << + (e.d_max_generation > 0 ? "" : "+") << -e.d_max_generation << " max. gen., " << + (e.d_max_cost > 0 ? "" : "+") << -e.d_max_cost << " max. cost)" << + endl; + } +} + +void display_usage() { + cout << "Usage: qprofdiff [options] " << endl; + cout << "Options:" << endl; + cout << " -n Suppress unchanged items" << endl; + cout << " -si Sort by difference in number of instances" << endl; + cout << " -sg Sort by difference in max. generation" << endl; + cout << " -sc Sort by difference in max. cost" << endl; +} + +int main(int argc, char ** argv) { + char * filename1 = 0; + char * filename2 = 0; + + for (int i = 1; i < argc; i++) { + int len = string(argv[i]).length(); + if (len > 1 && argv[i][0] == '-') { + options.insert(string(argv[i])); + } + else if (filename1 == 0) + filename1 = argv[i]; + else if (filename2 == 0) + filename2 = argv[i]; + else { + cout << "Invalid argument: " << argv[i] << endl << endl; + display_usage(); + return EINVAL; + } + } + + if (filename1 == 0 || filename2 == 0) { + cout << "Two filenames required." << endl << endl; + display_usage(); + return EINVAL; + } + + + cout << "Comparing " << filename1 << " to " << filename2 << endl; + + map data1, data2; + + int r = parse(filename1, data1); + if (r != 0) return r; + r = parse(filename2, data2); + if (r != 0) return r; + + // display_data(data1); + // display_data(data2); + + diff(data1, data2); + + return 0; +} \ No newline at end of file diff --git a/contrib/qprofdiff/qprofdiff.vcxproj b/contrib/qprofdiff/qprofdiff.vcxproj new file mode 100644 index 000000000..b6584e126 --- /dev/null +++ b/contrib/qprofdiff/qprofdiff.vcxproj @@ -0,0 +1,137 @@ + + + + + Debug + Win32 + + + Release + Win32 + + + Debug + x64 + + + Release + x64 + + + + 15.0 + {96E7E3EF-4162-474D-BD32-C702632AAF2B} + qprofdiff + 8.1 + + + + Application + true + v141 + NotSet + + + Application + false + v141 + true + MultiByte + + + Application + true + v141 + MultiByte + + + Application + false + v141 + true + MultiByte + + + + + + + + + + + + + + + + + + + + + $(IncludePath) + $(LibraryPath) + + + $(IncludePath) + $(LibraryPath) + + + + Level3 + Disabled + true + MultiThreadedDebugDLL + ..\..\src\util;%(AdditionalIncludeDirectories) + + + ProgramDatabase + + + $(LibraryPath);%(AdditionalLibraryDirectories) + + + + + Level3 + Disabled + true + ..\..\src\util;%(AdditionalIncludeDirectories) + + + + + Level3 + MaxSpeed + true + true + true + ..\..\src\util;%(AdditionalIncludeDirectories) + + + true + true + + + + + Level3 + MaxSpeed + true + true + true + ..\..\src\util;%(AdditionalIncludeDirectories) + + + true + true + + + + + + + + + \ No newline at end of file diff --git a/contrib/qprofdiff/qprofdiff.vcxproj.filters b/contrib/qprofdiff/qprofdiff.vcxproj.filters new file mode 100644 index 000000000..0d8d9e457 --- /dev/null +++ b/contrib/qprofdiff/qprofdiff.vcxproj.filters @@ -0,0 +1,22 @@ + + + + + {4FC737F1-C7A5-4376-A066-2A32D752A2FF} + cpp;c;cc;cxx;def;odl;idl;hpj;bat;asm;asmx + + + {93995380-89BD-4b04-88EB-625FBE52EBFB} + h;hh;hpp;hxx;hm;inl;inc;xsd + + + {67DA6AB6-F800-4c08-8B7A-83BB121AAD01} + rc;ico;cur;bmp;dlg;rc2;rct;bin;rgs;gif;jpg;jpeg;jpe;resx;tiff;tif;png;wav;mfcribbon-ms + + + + + Source Files + + + \ No newline at end of file