add an external cache using Redis
This commit gives alive-tv and the opt pass the capacity to not
perform a refinement check that has been performed before, by asking
an external redis server if it has seen a checksum of the src/tgt
alive IR before.
MODIFY
CMakeLists.txt
CMakeLists.txt
@@ -167,7 +167,12 @@ if (BUILD_LLVM_UTILS OR BUILD_TV)
include_directories(${LLVM_INCLUDE_DIRS})
add_definitions(${LLVM_DEFINITIONS})
+ find_package(hiredis REQUIRED)
+ include_directories(${HIREDIS_INCLUDE_DIR})
+
set(LLVM_UTIL_SRCS
+ "llvm_util/cache.cpp"
+ "llvm_util/crc.cpp"
"llvm_util/known_fns.cpp"
"llvm_util/llvm_optimizer.cpp"
"llvm_util/llvm2alive.cpp"
@@ -235,15 +240,16 @@ endif()
if (CYGWIN)
# cmake on cygwin doesn't seem to know about dlls..
get_filename_component(Z3_LIB_DIR "${Z3_LIBRARIES}" DIRECTORY)
- set(CMAKE_EXE_LINKER_FLAGS "-L${Z3_LIB_DIR} -lz3")
- set(CMAKE_SHARED_LINKER_FLAGS "-L${Z3_LIB_DIR} -lz3")
- file(COPY "${Z3_LIBRARIES}" DESTINATION "${PROJECT_BINARY_DIR}")
+ get_filename_component(HIREDIS_LIB_DIR "${HIREDIS_LIBRARIES}" DIRECTORY)
+ set(CMAKE_EXE_LINKER_FLAGS "-L${Z3_LIB_DIR} -lz3 -L${HIREDIS_LIB_DIR} -lhiredis")
+ set(CMAKE_SHARED_LINKER_FLAGS "-L${Z3_LIB_DIR} -lz3 -L${HIREDIS_LIB_DIR} -lhiredis")
+ file(COPY "${Z3_LIBRARIES} ${HIREDIS_LIBRARIES}" DESTINATION "${PROJECT_BINARY_DIR}")
else()
- target_link_libraries(alive PRIVATE ${Z3_LIBRARIES})
- #target_link_libraries(alive2 PRIVATE ${Z3_LIBRARIES})
+ target_link_libraries(alive PRIVATE ${Z3_LIBRARIES} ${HIREDIS_LIBRARIES})
+ #target_link_libraries(alive2 PRIVATE ${Z3_LIBRARIES} ${HIREDIS_LIBRARIES})
if (BUILD_LLVM_UTILS OR BUILD_TV)
- target_link_libraries(alive-tv PRIVATE ${Z3_LIBRARIES})
- target_link_libraries(alive-exec PRIVATE ${Z3_LIBRARIES})
+ target_link_libraries(alive-tv PRIVATE ${Z3_LIBRARIES} ${HIREDIS_LIBRARIES})
+ target_link_libraries(alive-exec PRIVATE ${Z3_LIBRARIES} ${HIREDIS_LIBRARIES})
endif()
endif()

MODIFY
README.md
README.md
@@ -33,6 +33,7 @@ To build Alive2 you need recent versions of:
* re2c
* Z3
* LLVM (optional)
+* hiredis (required if building with LLVM)
Building
@@ -268,6 +269,20 @@ the function cannot take inputs, cannot use memory, cannot depend on
undefined behaviors, and cannot include loops that execute too many
iterations.
+Caching
+--------
+
+The alive-tv tool and the Alive2 translation validation opt plugin
+support using an external Redis server to avoid performing redundant
+queries. This feature is not intended for general use, but rather to
+speed up certain systematic testing workloads that perform a lot of
+repeated work. When it hits a repeated refinement check, it prints
+"Skipping repeated query" instead of performing the query.
+
+If you want to use this functionality, you will need to manually start
+and stop, as appropriate, a Redis server instance on localhost. Alive2
+should be the only user of this server.
+
LLVM Bugs Found by Alive2
--------

ADD
cmake/Findhiredis.cmake
+find_path(HIREDIS_INCLUDE_DIR NAMES hiredis/hiredis.h)
+find_library(HIREDIS_LIBRARIES NAMES hiredis)
+
+if(NOT HIREDIS_INCLUDE_DIR)
+ message(FATAL_ERROR "hiredis include directory not found")
+endif()
+
+if(NOT HIREDIS_LIBRARIES)
+ message(FATAL_ERROR "hiredis library not found")
+endif()
+
+message(STATUS "hiredis: ${HIREDIS_INCLUDE_DIR} ${HIREDIS_LIBRARIES}")

ADD
llvm_util/cache.cpp
+#include "cache.h"
+#include "crc.h"
+#include "util/errors.h"
+#include "util/version.h"
+
+#include <cassert>
+#include <iostream>
+#include <sstream>
+#include <string>
+#include <vector>
+
+using namespace std;
+
+static string redis_reply_string(int reply_type) {
+ switch (reply_type) {
+ case REDIS_REPLY_STRING:
+ return "STRING";
+ case REDIS_REPLY_ARRAY:
+ return "ARRAY";
+ case REDIS_REPLY_INTEGER:
+ return "INTEGER";
+ case REDIS_REPLY_NIL:
+ return "NIL";
+ case REDIS_REPLY_STATUS:
+ return "STATUS";
+ case REDIS_REPLY_ERROR:
+ return "ERROR";
+ default:
+ return "UNKNOWN REPLY";
+ }
+}
+
+static bool remote_get(const string &key, string &value, redisContext *ctx) {
+ assert(ctx);
+ redisReply *reply = (redisReply *)redisCommand(ctx, "GET %s", key.data());
+ if (!reply || ctx->err) {
+ cerr << "Redis error in remote_get: " << ctx->errstr << "\n";
+ exit(-1);
+ }
+ if (reply->type == REDIS_REPLY_NIL) {
+ // not found
+ freeReplyObject(reply);
+ return false;
+ } else if (reply->type == REDIS_REPLY_STRING) {
+ // found
+ value = reply->str;
+ freeReplyObject(reply);
+ return true;
+ } else {
+ cerr << "Redis protocol error in remote_get, didn't expect reply type "
+ << redis_reply_string(reply->type) << "\n";
+ exit(-1);
+ }
+}
+
+static void remote_set(const string &key, const string &value, redisContext *ctx) {
+ assert(ctx);
+ redisReply *reply =
+ (redisReply *)redisCommand(ctx, "SET %s %s", key.data(), value.data());
+ if (!reply || ctx->err) {
+ cerr << "Redis error in remote_set: " << ctx->errstr << "\n";
+ exit(-1);
+ }
+ if (reply->type != REDIS_REPLY_STATUS) {
+ cerr << "Redis protocol error in remote_set, didn't expect reply type "
+ << redis_reply_string(reply->type) << "\n";
+ exit(-1);
+ }
+ freeReplyObject(reply);
+}
+
+static crc_t string_crc(const string &s) {
+ return crc_finalize(crc_update(crc_init(), s.data(), s.size()));
+}
+
+bool Cache::lookup(const string &s) {
+ static const string default_value("XXX");
+ // Alive IR is bulky, so send a hash of it over to the cache. If
+ // this still uses too much RAM, the next step will be to use a
+ // Bloom filter
+ string remote_data, crc_string = to_string(string_crc(s));
+ if (remote_get(crc_string, remote_data, ctx)) {
+ assert(remote_data == default_value);
+ return true;
+ } else {
+ remote_set(crc_string, default_value, ctx);
+ return false;
+ }
+}
+
+Cache::Cache(unsigned port, bool allow_version_mismatch) {
+ const char *hostname = "127.0.0.1";
+ struct timeval timeout = {1, 500000}; // 1.5 seconds
+ ctx = redisConnectWithTimeout(hostname, port, timeout);
+ if (!ctx) {
+ cerr << "Can't allocate redis context\n";
+ exit(-1);
+ }
+ if (ctx->err) {
+ cerr << "Redis connection error: " << ctx->errstr << "\n";
+ exit(-1);
+ }
+ string version;
+ if (remote_get("Alive2_version", version, ctx)) {
+ if (version != util::alive_version) {
+ cerr << "Cache version mismatch!\n";
+ cerr << "This version of Alive2 is " << util::alive_version << "\n";
+ cerr << "But the cache was created by version " << version << "\n";
+ if (!allow_version_mismatch)
+ exit(-1);
+ }
+ } else {
+ remote_set("Alive2_version", util::alive_version, ctx);
+ }
+}
+
+
+Cache::~Cache() {
+ redisFree(ctx);
+}

ADD
llvm_util/cache.h
+#pragma once
+
+#include <hiredis/hiredis.h>
+#include <memory>
+#include <string>
+#include <string_view>
+
+class Cache {
+ redisContext *ctx = nullptr;
+
+public:
+ Cache(unsigned port, bool allow_version_mismatch);
+ ~Cache();
+ bool lookup(const std::string &s);
+};

MODIFY
llvm_util/cmd_args_list.h
llvm_util/cmd_args_list.h
@@ -139,6 +139,19 @@ llvm::cl::opt<bool> opt_overwrite_reports(LLVM_ARGS_PREFIX "overwrite-reports",
llvm::cl::desc("Overwrite existing report files"),
llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));
+llvm::cl::opt<bool> opt_cache(LLVM_ARGS_PREFIX "cache",
+ llvm::cl::init(false),
+ llvm::cl::desc("Use external cache (default=false)"));
+
+llvm::cl::opt<unsigned> opt_cache_port(LLVM_ARGS_PREFIX "cache-port",
+ llvm::cl::init(6379),
+ llvm::cl::desc("Port to connect to Redis server (default=6379"));
+
+llvm::cl::opt<bool> opt_cache_allow_version_mismatch(LLVM_ARGS_PREFIX
+ "cache-allow-version-mismatch", llvm::cl::init(false),
+ llvm::cl::desc("Allow external cache to have been created by a different "
+ "version of Alive2 (default=false"));
+
llvm::cl::opt<unsigned> opt_max_offset_in_bits(
LLVM_ARGS_PREFIX "max-offset-in-bits", llvm::cl::init(64),
llvm::cl::desc("Upper bound for the maximum pointer offset in bits. Note "

ADD
llvm_util/crc.cpp
+/**
+ * \file
+ * Functions and types for CRC checks.
+ *
+ * Generated on Mon Aug 22 17:42:14 2022
+ * by pycrc v0.9.2, https://pycrc.org
+ * using the configuration:
+ * - Width = 64
+ * - Poly = 0x000000000000001b
+ * - XorIn = 0x0000000000000000
+ * - ReflectIn = True
+ * - XorOut = 0x0000000000000000
+ * - ReflectOut = True
+ * - Algorithm = table-driven
+ */
+#include "crc.h" /* include the header file generated with pycrc */
+#include <stdint.h>
+#include <stdlib.h>
+
+/**
+ * Static table used for the table_driven implementation.
+ */
+static const crc_t crc_table[256] = {
+ 0x0000000000000000, 0x01b0000000000000, 0x0360000000000000,
+ 0x02d0000000000000, 0x06c0000000000000, 0x0770000000000000,
+ 0x05a0000000000000, 0x0410000000000000, 0x0d80000000000000,
+ 0x0c30000000000000, 0x0ee0000000000000, 0x0f50000000000000,
+ 0x0b40000000000000, 0x0af0000000000000, 0x0820000000000000,
+ 0x0990000000000000, 0x1b00000000000000, 0x1ab0000000000000,
+ 0x1860000000000000, 0x19d0000000000000, 0x1dc0000000000000,
+ 0x1c70000000000000, 0x1ea0000000000000, 0x1f10000000000000,
+ 0x1680000000000000, 0x1730000000000000, 0x15e0000000000000,
+ 0x1450000000000000, 0x1040000000000000, 0x11f0000000000000,
+ 0x1320000000000000, 0x1290000000000000, 0x3600000000000000,
+ 0x37b0000000000000, 0x3560000000000000, 0x34d0000000000000,
+ 0x30c0000000000000, 0x3170000000000000, 0x33a0000000000000,
+ 0x3210000000000000, 0x3b80000000000000, 0x3a30000000000000,
+ 0x38e0000000000000, 0x3950000000000000, 0x3d40000000000000,
+ 0x3cf0000000000000, 0x3e20000000000000, 0x3f90000000000000,
+ 0x2d00000000000000, 0x2cb0000000000000, 0x2e60000000000000,
+ 0x2fd0000000000000, 0x2bc0000000000000, 0x2a70000000000000,
+ 0x28a0000000000000, 0x2910000000000000, 0x2080000000000000,
+ 0x2130000000000000, 0x23e0000000000000, 0x2250000000000000,
+ 0x2640000000000000, 0x27f0000000000000, 0x2520000000000000,
+ 0x2490000000000000, 0x6c00000000000000, 0x6db0000000000000,
+ 0x6f60000000000000, 0x6ed0000000000000, 0x6ac0000000000000,
+ 0x6b70000000000000, 0x69a0000000000000, 0x6810000000000000,
+ 0x6180000000000000, 0x6030000000000000, 0x62e0000000000000,
+ 0x6350000000000000, 0x6740000000000000, 0x66f0000000000000,
+ 0x6420000000000000, 0x6590000000000000, 0x7700000000000000,
+ 0x76b0000000000000, 0x7460000000000000, 0x75d0000000000000,
+ 0x71c0000000000000, 0x7070000000000000, 0x72a0000000000000,
+ 0x7310000000000000, 0x7a80000000000000, 0x7b30000000000000,
+ 0x79e0000000000000, 0x7850000000000000, 0x7c40000000000000,
+ 0x7df0000000000000, 0x7f20000000000000, 0x7e90000000000000,
+ 0x5a00000000000000, 0x5bb0000000000000, 0x5960000000000000,
+ 0x58d0000000000000, 0x5cc0000000000000, 0x5d70000000000000,
+ 0x5fa0000000000000, 0x5e10000000000000, 0x5780000000000000,
+ 0x5630000000000000, 0x54e0000000000000, 0x5550000000000000,
+ 0x5140000000000000, 0x50f0000000000000, 0x5220000000000000,
+ 0x5390000000000000, 0x4100000000000000, 0x40b0000000000000,
+ 0x4260000000000000, 0x43d0000000000000, 0x47c0000000000000,
+ 0x4670000000000000, 0x44a0000000000000, 0x4510000000000000,
+ 0x4c80000000000000, 0x4d30000000000000, 0x4fe0000000000000,
+ 0x4e50000000000000, 0x4a40000000000000, 0x4bf0000000000000,
+ 0x4920000000000000, 0x4890000000000000, 0xd800000000000000,
+ 0xd9b0000000000000, 0xdb60000000000000, 0xdad0000000000000,
+ 0xdec0000000000000, 0xdf70000000000000, 0xdda0000000000000,
+ 0xdc10000000000000, 0xd580000000000000, 0xd430000000000000,
+ 0xd6e0000000000000, 0xd750000000000000, 0xd340000000000000,
+ 0xd2f0000000000000, 0xd020000000000000, 0xd190000000000000,
+ 0xc300000000000000, 0xc2b0000000000000, 0xc060000000000000,
+ 0xc1d0000000000000, 0xc5c0000000000000, 0xc470000000000000,
+ 0xc6a0000000000000, 0xc710000000000000, 0xce80000000000000,
+ 0xcf30000000000000, 0xcde0000000000000, 0xcc50000000000000,
+ 0xc840000000000000, 0xc9f0000000000000, 0xcb20000000000000,
+ 0xca90000000000000, 0xee00000000000000, 0xefb0000000000000,
+ 0xed60000000000000, 0xecd0000000000000, 0xe8c0000000000000,
+ 0xe970000000000000, 0xeba0000000000000, 0xea10000000000000,
+ 0xe380000000000000, 0xe230000000000000, 0xe0e0000000000000,
+ 0xe150000000000000, 0xe540000000000000, 0xe4f0000000000000,
+ 0xe620000000000000, 0xe790000000000000, 0xf500000000000000,
+ 0xf4b0000000000000, 0xf660000000000000, 0xf7d0000000000000,
+ 0xf3c0000000000000, 0xf270000000000000, 0xf0a0000000000000,
+ 0xf110000000000000, 0xf880000000000000, 0xf930000000000000,
+ 0xfbe0000000000000, 0xfa50000000000000, 0xfe40000000000000,
+ 0xfff0000000000000, 0xfd20000000000000, 0xfc90000000000000,
+ 0xb400000000000000, 0xb5b0000000000000, 0xb760000000000000,
+ 0xb6d0000000000000, 0xb2c0000000000000, 0xb370000000000000,
+ 0xb1a0000000000000, 0xb010000000000000, 0xb980000000000000,
+ 0xb830000000000000, 0xbae0000000000000, 0xbb50000000000000,
+ 0xbf40000000000000, 0xbef0000000000000, 0xbc20000000000000,
+ 0xbd90000000000000, 0xaf00000000000000, 0xaeb0000000000000,
+ 0xac60000000000000, 0xadd0000000000000, 0xa9c0000000000000,
+ 0xa870000000000000, 0xaaa0000000000000, 0xab10000000000000,
+ 0xa280000000000000, 0xa330000000000000, 0xa1e0000000000000,
+ 0xa050000000000000, 0xa440000000000000, 0xa5f0000000000000,
+ 0xa720000000000000, 0xa690000000000000, 0x8200000000000000,
+ 0x83b0000000000000, 0x8160000000000000, 0x80d0000000000000,
+ 0x84c0000000000000, 0x8570000000000000, 0x87a0000000000000,
+ 0x8610000000000000, 0x8f80000000000000, 0x8e30000000000000,
+ 0x8ce0000000000000, 0x8d50000000000000, 0x8940000000000000,
+ 0x88f0000000000000, 0x8a20000000000000, 0x8b90000000000000,
+ 0x9900000000000000, 0x98b0000000000000, 0x9a60000000000000,
+ 0x9bd0000000000000, 0x9fc0000000000000, 0x9e70000000000000,
+ 0x9ca0000000000000, 0x9d10000000000000, 0x9480000000000000,
+ 0x9530000000000000, 0x97e0000000000000, 0x9650000000000000,
+ 0x9240000000000000, 0x93f0000000000000, 0x9120000000000000,
+ 0x9090000000000000};
+
+crc_t crc_update(crc_t crc, const void *data, size_t data_len) {
+ const unsigned char *d = (const unsigned char *)data;
+ unsigned int tbl_idx;
+
+ while (data_len--) {
+ tbl_idx = (crc ^ *d) & 0xff;
+ crc = (crc_table[tbl_idx] ^ (crc >> 8)) & 0xffffffffffffffff;
+ d++;
+ }
+ return crc & 0xffffffffffffffff;
+}

ADD
llvm_util/crc.h
+/**
+ * \file
+ * Functions and types for CRC checks.
+ *
+ * Generated on Mon Aug 22 17:42:03 2022
+ * by pycrc v0.9.2, https://pycrc.org
+ * using the configuration:
+ * - Width = 64
+ * - Poly = 0x000000000000001b
+ * - XorIn = 0x0000000000000000
+ * - ReflectIn = True
+ * - XorOut = 0x0000000000000000
+ * - ReflectOut = True
+ * - Algorithm = table-driven
+ *
+ * This file defines the functions crc_init(), crc_update() and crc_finalize().
+ *
+ * The crc_init() function returns the initial \c crc value and must be called
+ * before the first call to crc_update().
+ * Similarly, the crc_finalize() function must be called after the last call
+ * to crc_update(), before the \c crc is being used.
+ * is being used.
+ *
+ * The crc_update() function can be called any number of times (including zero
+ * times) in between the crc_init() and crc_finalize() calls.
+ *
+ * This pseudo-code shows an example usage of the API:
+ * \code{.c}
+ * crc_t crc;
+ * unsigned char data[MAX_DATA_LEN];
+ * size_t data_len;
+ *
+ * crc = crc_init();
+ * while ((data_len = read_data(data, MAX_DATA_LEN)) > 0) {
+ * crc = crc_update(crc, data, data_len);
+ * }
+ * crc = crc_finalize(crc);
+ * \endcode
+ */
+#ifndef CRC_H
+#define CRC_H
+
+#include <stdint.h>
+#include <stdlib.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/**
+ * The definition of the used algorithm.
+ *
+ * This is not used anywhere in the generated code, but it may be used by the
+ * application code to call algorithm-specific code, if desired.
+ */
+#define CRC_ALGO_TABLE_DRIVEN 1
+
+/**
+ * The type of the CRC values.
+ *
+ * This type must be big enough to contain at least 64 bits.
+ */
+typedef uint_fast64_t crc_t;
+
+/**
+ * Calculate the initial crc value.
+ *
+ * \return The initial crc value.
+ */
+static inline crc_t crc_init(void) {
+ return 0x0000000000000000;
+}
+
+/**
+ * Update the crc value with new data.
+ *
+ * \param[in] crc The current crc value.
+ * \param[in] data Pointer to a buffer of \a data_len bytes.
+ * \param[in] data_len Number of bytes in the \a data buffer.
+ * \return The updated crc value.
+ */
+crc_t crc_update(crc_t crc, const void *data, size_t data_len);
+
+/**
+ * Calculate the final crc value.
+ *
+ * \param[in] crc The current crc value.
+ * \return The final crc value.
+ */
+static inline crc_t crc_finalize(crc_t crc) {
+ return crc;
+}
+
+#ifdef __cplusplus
+} /* closing brace for extern "C" */
+#endif
+
+#endif /* CRC_H */

MODIFY
scripts/alivecc.in
scripts/alivecc.in
@@ -30,8 +30,22 @@ if ($0 =~ /alivecc$/) {
die "Unexpected invocation as '$0'";
}
+my $print_cmd = 0;
+
if (compiling()) {
+ if (getenv("ALIVECC_CACHE")) {
+ push @ARGV, ("-mllvm", "-tv-cache=true");
+ }
+
+ if (getenv("ALIVECC_CACHE_ALLOW_VERSION_MISMATCH")) {
+ push @ARGV, ("-mllvm", "-tv-cache-allow-version-mismatch=true");
+ }
+
+ if (getenv("ALIVECC_PRINT_COMMAND")) {
+ $print_cmd = 1;
+ }
+
if (getenv("ALIVECC_QUIET")) {
push @ARGV, ("-mllvm", "-tv-quiet");
}
@@ -108,4 +122,11 @@ if (compiling()) {
push @ARGV, ("-Xclang", "-load", "-Xclang", "@CMAKE_BINARY_DIR@/tv/${TV_SHAREDLIB}");
}
+if ($print_cmd) {
+ foreach my $arg (@ARGV) {
+ print "$arg ";
+ }
+ print "\n\n";
+}
+
exec @ARGV;

MODIFY
tools/alive-exec.cpp
tools/alive-exec.cpp
@@ -83,7 +83,7 @@ void execFunction(llvm::Function &F, llvm::TargetLibraryInfoWrapperPass &TLI,
t.src = std::move(*Func);
t.tgt = *llvm2alive(F, TLI.getTLI(F), false);
t.preprocess();
- TransformVerify verifier(t, false);
+ TransformVerify verifier(t, false, nullptr);
if (!opt_quiet)
t.src.print(cout << "\n----------------------------------------\n");

MODIFY
tools/alive-tv.cpp
tools/alive-tv.cpp
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+#include "llvm_util/cache.h"
#include "llvm_util/llvm2alive.h"
#include "llvm_util/llvm_optimizer.h"
#include "smt/smt.h"
@@ -109,6 +110,8 @@ struct Results {
}
};
+static unique_ptr<Cache> cache;
+
Results verify(llvm::Function &F1, llvm::Function &F2,
llvm::TargetLibraryInfoWrapperPass &TLI,
bool print_transform = false,
@@ -141,7 +144,7 @@ Results verify(llvm::Function &F1, llvm::Function &F2,
smt_init->reset();
r.t.preprocess();
- TransformVerify verifier(r.t, false);
+ TransformVerify verifier(r.t, false, &*cache);
if (print_transform)
r.t.print(*out, {});
@@ -296,6 +299,10 @@ convenient way to demonstrate an existing optimizer bug.
llvm::cl::HideUnrelatedOptions(alive_cmdargs);
llvm::cl::ParseCommandLineOptions(argc, argv, Usage);
+ if (opt_cache)
+ cache = make_unique<Cache>(opt_cache_port,
+ opt_cache_allow_version_mismatch);
+
auto M1 = openInputFile(Context, opt_file1);
if (!M1.get()) {
cerr << "Could not read bitcode from '" << opt_file1 << "'\n";

MODIFY
tools/alive.cpp
tools/alive.cpp
@@ -116,7 +116,7 @@ int main(int argc, char **argv) {
t.print(cout, print_opts);
cout << '\n';
- TransformVerify tv(t, !root_only);
+ TransformVerify tv(t, !root_only, nullptr);
auto types = tv.getTypings();
if (!types) {
cerr << "Doesn't type check!\n";

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -29,7 +29,6 @@ using namespace util;
using namespace std;
using util::config::dbg;
-
static void print_single_varval(ostream &os, const State &st, const Model &m,
const Value *var, const Type &type,
const StateValue &val, unsigned child) {
@@ -1095,8 +1094,9 @@ static void calculateAndInitConstants(Transform &t) {
namespace tools {
-TransformVerify::TransformVerify(Transform &t, bool check_each_var) :
- t(t), check_each_var(check_each_var) {
+TransformVerify::TransformVerify(Transform &t, bool check_each_var,
+ Cache *cache) :
+ t(t), check_each_var(check_each_var), cache(cache) {
if (check_each_var) {
for (auto &i : t.tgt.instrs()) {
tgt_instrs.emplace(i.getName(), &i);

MODIFY
tools/transform.h
tools/transform.h
#include "smt/solver.h"
#include "util/errors.h"
#include <memory>
-#include <string>
#include <ostream>
+#include <string>
#include <unordered_map>
+class Cache;
+
namespace tools {
struct TransformPrintOpts {
@@ -51,9 +53,10 @@ class TransformVerify {
Transform &t;
std::unordered_map<std::string, const IR::Instr*> tgt_instrs;
bool check_each_var;
+ Cache *cache;
public:
- TransformVerify(Transform &t, bool check_each_var);
+ TransformVerify(Transform &t, bool check_each_var, Cache *cache);
std::pair<std::unique_ptr<IR::State>,std::unique_ptr<IR::State>> exec() const;
util::Errors verify() const;
TypingAssignments getTypings() const;

MODIFY
tv/CMakeLists.txt
tv/CMakeLists.txt
@@ -26,7 +26,7 @@ configure_file(
@ONLY
)
-target_link_libraries(tv PRIVATE ${ALIVE_LIBS_LLVM} ${Z3_LIBRARIES}
+target_link_libraries(tv PRIVATE ${ALIVE_LIBS_LLVM} ${Z3_LIBRARIES} ${HIREDIS_LIBRARIES}
$<$<AND:$<CXX_COMPILER_ID:GNU>,$<VERSION_LESS:$<CXX_COMPILER_VERSION>,9.0>>:stdc++fs>)
if(APPLE)

MODIFY
tv/tv.cpp
tv/tv.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/memory.h"
+#include "llvm_util/cache.h"
#include "llvm_util/llvm2alive.h"
#include "llvm_util/utils.h"
#include "smt/smt.h"
@@ -81,6 +82,7 @@ bool showed_stats = false;
bool has_failure = false;
// If is_clangtv is true, tv should exit with zero
bool is_clangtv = false;
+unique_ptr<Cache> cache;
unique_ptr<parallel> parallelMgr;
stringstream parent_ss;
std::unique_ptr<llvm::Module> MClone;
@@ -240,9 +242,10 @@ struct TVLegacyPass final : public llvm::ModulePass {
static void verify(Transform &t, int n, const string &src_tostr) {
printDot(t.tgt, n);
+ auto tgt_tostr = toString(t.tgt);
if (!opt_always_verify) {
// Compare Alive2 IR and skip if syntactically equal
- if (src_tostr == toString(t.tgt)) {
+ if (src_tostr == tgt_tostr) {
if (!opt_quiet)
t.print(*out, print_opts);
*out << "Transformation seems to be correct! (syntactically equal)\n\n";
@@ -250,6 +253,13 @@ struct TVLegacyPass final : public llvm::ModulePass {
}
}
+ // Since we have an open connection to the Redis server, we have
+ // to do this before forking. Anyway, this is fast.
+ if (cache && cache->lookup(src_tostr + "===\n" + tgt_tostr)) {
+ *out << "Skipping repeated query\n\n";
+ return false;
+ }
+
if (parallelMgr) {
auto [pid, osp, index] = parallelMgr->limitedFork();
@@ -294,7 +304,7 @@ struct TVLegacyPass final : public llvm::ModulePass {
smt_init->reset();
t.preprocess();
- TransformVerify verifier(t, false);
+ TransformVerify verifier(t, false, &*cache);
if (!opt_quiet)
t.print(*out, print_opts);
@@ -337,11 +347,6 @@ struct TVLegacyPass final : public llvm::ModulePass {
}
}
- bool doInitialization(llvm::Module &module) override {
- initialize(module);
- return false;
- }
-
static void initialize(llvm::Module &module) {
if (initialized++)
return;
@@ -372,6 +377,10 @@ struct TVLegacyPass final : public llvm::ModulePass {
}
}
+ if (opt_cache)
+ cache = make_unique<Cache>(opt_cache_port,
+ opt_cache_allow_version_mismatch);
+
showed_stats = false;
llvm_util_init.emplace(*out, module.getDataLayout());
smt_init.emplace();

add an external cache using Redis (#836)

This commit gives alive-tv and the opt pass the capacity to not
perform a refinement check that has been performed before, by asking
an external redis server if it has seen a checksum of the src/tgt
alive IR before.