move IR globals to globals.cpp
MODIFY
CMakeLists.txt
CMakeLists.txt
@@ -48,6 +48,7 @@ include_directories(${PROJECT_SOURCE_DIR})
set(IR_SRCS
ir/constant.cpp
ir/function.cpp
+ ir/globals.cpp
ir/instr.cpp
ir/memory.cpp
ir/precondition.cpp

ADD
ir/globals.cpp
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include "ir/globals.h"
+
+namespace IR {
+
+unsigned num_max_nonlocals_inst;
+unsigned num_locals;
+unsigned num_nonlocals;
+unsigned bits_for_bid;
+unsigned bits_for_offset;
+bool little_endian;
+bool nullptr_is_used;
+bool has_int2ptr;
+bool has_ptr2int;
+
+}

ADD
ir/globals.h
+#pragma once
+
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+namespace IR {
+
+/// Upperbound of the number of non-local pointers returned by instructions
+extern unsigned num_max_nonlocals_inst;
+
+/// Upperbound of the number of local blocks (max(src, tgt))
+extern unsigned num_locals;
+
+// Upperbound of the number of nonlocal blocks
+extern unsigned num_nonlocals;
+
+/// Number of bits needed for encoding a memory block id
+extern unsigned bits_for_bid;
+
+// Number of bits needed for encoding a pointer's offset
+extern unsigned bits_for_offset;
+
+extern bool little_endian;
+
+/// Wether the null pointer is used in either function
+extern bool nullptr_is_used;
+
+/// Wether int2ptr or ptr2int are used in either function
+extern bool has_int2ptr;
+extern bool has_ptr2int;
+
+}

MODIFY
ir/memory.cpp
ir/memory.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/memory.h"
+#include "ir/globals.h"
#include "ir/state.h"
#include "util/compiler.h"
@@ -451,8 +452,8 @@ static bool memory_unused() {
return num_locals == 0 && num_nonlocals == 1 && !nullptr_is_used;
}
-Memory::Memory(State &state, bool little_endian)
- : state(&state), little_endian(little_endian),
+Memory::Memory(State &state)
+ : state(&state),
local_blk_addr(expr::mkUInt(0, bits_size_t - 1)),
local_blk_size(expr::mkUInt(0, bits_size_t - 1)),
local_blk_kind(expr::mkUInt(0, 2)) {

MODIFY
ir/memory.h
ir/memory.h
@@ -111,8 +111,6 @@ class Memory {
// bits_size_t is equivalent to the size of a pointer.
unsigned bits_size_t = 64;
- bool little_endian;
-
smt::expr non_local_block_val; // array: (bid, offset) -> Byte
smt::expr local_block_val;
@@ -133,7 +131,7 @@ public:
HEAP, STACK, GLOBAL, CONSTGLOBAL
};
- Memory(State &state, bool little_endian);
+ Memory(State &state);
static void resetGlobalData();
static void resetLocalBids();

MODIFY
ir/state.cpp
ir/state.cpp
@@ -13,41 +13,9 @@ using namespace std;
namespace IR {
-unsigned num_max_nonlocals_inst;
-unsigned num_locals;
-unsigned num_nonlocals;
-unsigned bits_for_bid;
-unsigned bits_for_offset;
-bool nullptr_is_used;
-bool has_int2ptr;
-bool has_ptr2int;
-
-void initConstants(unsigned num_globals, unsigned num_ptrinputs,
- unsigned num_max_nonlocals_inst, unsigned num_locals,
- bool nullptr_is_used, bool has_int2ptr, bool has_ptr2int) {
- IR::bits_for_offset = 64;
- IR::num_max_nonlocals_inst = num_max_nonlocals_inst;
- IR::num_locals = num_locals;
- // Include null block
- IR::num_nonlocals = num_globals + num_ptrinputs + num_max_nonlocals_inst + 1;
-
- IR::nullptr_is_used = nullptr_is_used;
- IR::has_int2ptr = has_int2ptr;
- IR::has_ptr2int = has_ptr2int;
-
- unsigned maxblks = max(num_locals, num_nonlocals);
- if (maxblks == 1)
- IR::bits_for_bid = 2; // local/non-local bit + one bit for bid
- else {
- unsigned n = ilog2(2 * maxblks - 1); // floor(log2(maxblks))
- IR::bits_for_bid = 1 + n;
- }
-}
-
State::State(const Function &f, bool source)
- : f(f), source(source), memory(*this, f.isLittleEndian()),
- return_domain(false), return_val(f.getType().getDummyValue(false)),
- return_memory(memory) {}
+ : f(f), source(source), memory(*this), return_domain(false),
+ return_val(f.getType().getDummyValue(false)), return_memory(memory) {}
void State::resetGlobals() {
Memory::resetGlobalData();

MODIFY
ir/state.h
ir/state.h
namespace IR {
-// The upperbound of # of non-local pointers that are returned by instructions.
-extern unsigned num_max_nonlocals_inst;
-// The upperbound of # of local blocks (max(src, tgt))
-extern unsigned num_locals;
-// The upperbound of # of nonlocal blocks
-extern unsigned num_nonlocals;
-// The number of bits needed for encoding block id.
-extern unsigned bits_for_bid;
-// The number of bits needed for encoding pointer's offset.
-extern unsigned bits_for_offset;
-extern bool nullptr_is_used;
-extern bool has_int2ptr;
-extern bool has_ptr2int;
-
-void initConstants(unsigned num_globals, unsigned num_ptrinputs,
- unsigned num_max_nonlocals_inst, unsigned num_locals,
- bool nullptr_is_used, bool has_int2ptr, bool has_ptr2int);
-
-
class Value;
class BasicBlock;
class Function;

MODIFY
ir/type.cpp
ir/type.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/type.h"
+#include "ir/globals.h"
#include "ir/state.h"
#include "smt/solver.h"
#include "util/compiler.h"

MODIFY
tools/transform.cpp
tools/transform.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "tools/transform.h"
+#include "ir/globals.h"
#include "ir/state.h"
#include "smt/expr.h"
#include "smt/smt.h"
@@ -372,27 +373,29 @@ static void calculateAndInitConstants(Transform &t) {
};
// The number of instructions that can return a pointer to a non-local block.
- unsigned num_inst_nonlocals = 0;
+ num_max_nonlocals_inst = 0;
// The number of local blocks.
unsigned num_locals_src = 0, num_locals_tgt = 0;
+
for (auto BB : t.src.getBBs()) {
const auto &instrs = BB->instrs();
for_each(instrs.begin(), instrs.end(), [&](const auto &i) {
num_locals_src += returns_local(i);
- num_inst_nonlocals += returns_nonlocal(i);
+ num_max_nonlocals_inst += returns_nonlocal(i);
});
}
for (auto BB : t.tgt.getBBs()) {
const auto &instrs = BB->instrs();
for_each(instrs.begin(), instrs.end(), [&](const auto &i) {
num_locals_tgt += returns_local(i);
- num_inst_nonlocals += returns_nonlocal(i);
+ num_max_nonlocals_inst += returns_nonlocal(i);
});
}
+ num_locals = max(num_locals_src, num_locals_tgt);
- bool nullptr_is_used = false;
- bool has_int2ptr = false;
- bool has_ptr2int = false;
+ nullptr_is_used = false;
+ has_int2ptr = false;
+ has_ptr2int = false;
for (auto fn : { &t.src, &t.tgt }) {
for (auto BB : fn->getBBs()) {
@@ -420,9 +423,17 @@ static void calculateAndInitConstants(Transform &t) {
}
exit_gv_loop:
- initConstants(num_globals, num_ptrinputs, num_inst_nonlocals,
- max(num_locals_src, num_locals_tgt), nullptr_is_used,
- has_int2ptr, has_ptr2int);
+ // Include null block
+ num_nonlocals = num_globals + num_ptrinputs + num_max_nonlocals_inst + 1;
+
+ // floor(log2(maxblks)) + 1 for local bit
+ unsigned maxblks = max(num_locals, num_nonlocals);
+ bits_for_bid = (maxblks == 1 ? 1 : ilog2(2 * maxblks - 1)) + 1;
+
+ // TODO
+ bits_for_offset = 64;
+
+ little_endian = t.src.isLittleEndian();
}
@@ -475,7 +486,7 @@ Errors TransformVerify::verify() const {
}
}
- ::calculateAndInitConstants(t);
+ calculateAndInitConstants(t);
State::resetGlobals();
State src_state(t.src, true), tgt_state(t.tgt, false);

move IR globals to globals.cpp