diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index ede4dc76..60c99d90 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -191,3 +191,52 @@ jobs: run: make -C regression/verilog test-z3 - name: Print ccache stats run: ccache -s + + # This job takes approximately 1 minute + check-ubuntu-22_04-nuterm: + runs-on: ubuntu-22.04 + steps: + - uses: actions/checkout@v3 + with: + submodules: recursive + - name: Fetch dependencies + env: + # This is needed in addition to -yq to prevent apt-get from asking for + # user input + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -yq gcc g++ ccache cmake + - name: Prepare ccache + uses: actions/cache@v3 + with: + path: .ccache + key: ${{ runner.os }}-22.04-nuterm-${{ github.ref }}-${{ github.sha }}-PR + restore-keys: | + ${{ runner.os }}-22.04-nuterm-${{ github.ref }} + ${{ runner.os }}-22.04-nuterm + - name: ccache environment + run: | + echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV + echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV + - name: Zero ccache stats and limit in size + run: ccache -z --max-size=500M + - name: Get pytorch + run: | + cd src/nuterm + wget -q https://download.pytorch.org/libtorch/cpu/libtorch-cxx11-abi-shared-with-deps-2.1.2%2Bcpu.zip + unzip -q *.zip + - name: Build with cmake + run: | + cd src/nuterm + LIBTORCH=`pwd`/libtorch + mkdir build + cd build + cmake -DCMAKE_PREFIX_PATH=$LIBTORCH -DCMAKE_CXX_COMPILER_LAUNCHER=ccache .. + cmake --build . --config Release + - name: Run the unit tests + run: src/nuterm/build/pytorch_tests + - name: Run the system tests + run: make -C regression/nuterm + - name: Print ccache stats + run: ccache -s diff --git a/regression/nuterm/Makefile b/regression/nuterm/Makefile new file mode 100644 index 00000000..e7129229 --- /dev/null +++ b/regression/nuterm/Makefile @@ -0,0 +1,7 @@ +default: test + +TEST_PL = ../../lib/cbmc/regression/test.pl + +test: + @$(TEST_PL) -c ../../../src/nuterm/build/nuterm + diff --git a/regression/nuterm/counters/counter1.desc b/regression/nuterm/counters/counter1.desc new file mode 100644 index 00000000..fb18fddc --- /dev/null +++ b/regression/nuterm/counters/counter1.desc @@ -0,0 +1,9 @@ +CORE +counter1 + +^weight main.clk = 0 .*$ +^weight main.counter = 1 .*$ +^RESULT: main.counter-1$ +^bias: -1 .*$ +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/nuterm/counters/counter1.v b/regression/nuterm/counters/counter1.v new file mode 100644 index 00000000..8602870e --- /dev/null +++ b/regression/nuterm/counters/counter1.v @@ -0,0 +1,9 @@ +module main(input clk); + + reg [31:0] counter; + + always @(posedge clk) + if(counter != 0) + counter = counter - 1; + +endmodule diff --git a/regression/nuterm/counters/counter1/trace.1 b/regression/nuterm/counters/counter1/trace.1 new file mode 100644 index 00000000..bf4d73ec --- /dev/null +++ b/regression/nuterm/counters/counter1/trace.1 @@ -0,0 +1,37 @@ +$date + Sun Jan 7 16:33:39 2024 +$end +$timescale + 1ns +$end +$scope module main $end + $var reg 32 main.counter main.counter [31:0] $end + $var wire 1 main.clk main.clk $end +$upscope $end +$enddefinitions $end +#0 +b00010000000000000000000000000000 main.counter +0main.clk +#1 +b00001111111111111111111111111111 main.counter +1main.clk +#2 +b00001111111111111111111111111110 main.counter +#3 +b00001111111111111111111111111101 main.counter +0main.clk +#4 +b00001111111111111111111111111100 main.counter +1main.clk +#5 +b00001111111111111111111111111011 main.counter +#6 +b00001111111111111111111111111010 main.counter +#7 +b00001111111111111111111111111001 main.counter +#8 +b00001111111111111111111111111000 main.counter +#9 +b00001111111111111111111111110111 main.counter +#10 +b00001111111111111111111111110110 main.counter diff --git a/regression/nuterm/counters/counter1/trace.10 b/regression/nuterm/counters/counter1/trace.10 new file mode 100644 index 00000000..01b330e5 --- /dev/null +++ b/regression/nuterm/counters/counter1/trace.10 @@ -0,0 +1,40 @@ +$date + Sun Jan 7 16:33:39 2024 +$end +$timescale + 1ns +$end +$scope module main $end + $var reg 32 main.counter main.counter [31:0] $end + $var wire 1 main.clk main.clk $end +$upscope $end +$enddefinitions $end +#0 +b00010000000000000000000000000000 main.counter +0main.clk +#1 +b00001111111111111111111111111111 main.counter +1main.clk +#2 +b00001111111111111111111111111110 main.counter +0main.clk +#3 +b00001111111111111111111111111101 main.counter +#4 +b00001111111111111111111111111100 main.counter +1main.clk +#5 +b00001111111111111111111111111011 main.counter +0main.clk +#6 +b00001111111111111111111111111010 main.counter +#7 +b00001111111111111111111111111001 main.counter +#8 +b00001111111111111111111111111000 main.counter +1main.clk +#9 +b00001111111111111111111111110111 main.counter +#10 +b00001111111111111111111111110110 main.counter +0main.clk diff --git a/regression/nuterm/counters/counter1/trace.2 b/regression/nuterm/counters/counter1/trace.2 new file mode 100644 index 00000000..cdbc97ec --- /dev/null +++ b/regression/nuterm/counters/counter1/trace.2 @@ -0,0 +1,39 @@ +$date + Sun Jan 7 16:33:39 2024 +$end +$timescale + 1ns +$end +$scope module main $end + $var reg 32 main.counter main.counter [31:0] $end + $var wire 1 main.clk main.clk $end +$upscope $end +$enddefinitions $end +#0 +b00010000000000000000000000000000 main.counter +0main.clk +#1 +b00001111111111111111111111111111 main.counter +#2 +b00001111111111111111111111111110 main.counter +1main.clk +#3 +b00001111111111111111111111111101 main.counter +0main.clk +#4 +b00001111111111111111111111111100 main.counter +#5 +b00001111111111111111111111111011 main.counter +#6 +b00001111111111111111111111111010 main.counter +#7 +b00001111111111111111111111111001 main.counter +#8 +b00001111111111111111111111111000 main.counter +1main.clk +#9 +b00001111111111111111111111110111 main.counter +0main.clk +#10 +b00001111111111111111111111110110 main.counter +1main.clk diff --git a/regression/nuterm/counters/counter1/trace.3 b/regression/nuterm/counters/counter1/trace.3 new file mode 100644 index 00000000..bb73ef9f --- /dev/null +++ b/regression/nuterm/counters/counter1/trace.3 @@ -0,0 +1,40 @@ +$date + Sun Jan 7 16:33:39 2024 +$end +$timescale + 1ns +$end +$scope module main $end + $var reg 32 main.counter main.counter [31:0] $end + $var wire 1 main.clk main.clk $end +$upscope $end +$enddefinitions $end +#0 +b00010000000000000000000000000000 main.counter +1main.clk +#1 +b00001111111111111111111111111111 main.counter +0main.clk +#2 +b00001111111111111111111111111110 main.counter +#3 +b00001111111111111111111111111101 main.counter +1main.clk +#4 +b00001111111111111111111111111100 main.counter +#5 +b00001111111111111111111111111011 main.counter +#6 +b00001111111111111111111111111010 main.counter +#7 +b00001111111111111111111111111001 main.counter +0main.clk +#8 +b00001111111111111111111111111000 main.counter +1main.clk +#9 +b00001111111111111111111111110111 main.counter +0main.clk +#10 +b00001111111111111111111111110110 main.counter +1main.clk diff --git a/regression/nuterm/counters/counter1/trace.4 b/regression/nuterm/counters/counter1/trace.4 new file mode 100644 index 00000000..a73e1f43 --- /dev/null +++ b/regression/nuterm/counters/counter1/trace.4 @@ -0,0 +1,41 @@ +$date + Sun Jan 7 16:33:39 2024 +$end +$timescale + 1ns +$end +$scope module main $end + $var reg 32 main.counter main.counter [31:0] $end + $var wire 1 main.clk main.clk $end +$upscope $end +$enddefinitions $end +#0 +b00010000000000000000000000000000 main.counter +0main.clk +#1 +b00001111111111111111111111111111 main.counter +1main.clk +#2 +b00001111111111111111111111111110 main.counter +#3 +b00001111111111111111111111111101 main.counter +0main.clk +#4 +b00001111111111111111111111111100 main.counter +1main.clk +#5 +b00001111111111111111111111111011 main.counter +#6 +b00001111111111111111111111111010 main.counter +0main.clk +#7 +b00001111111111111111111111111001 main.counter +#8 +b00001111111111111111111111111000 main.counter +1main.clk +#9 +b00001111111111111111111111110111 main.counter +0main.clk +#10 +b00001111111111111111111111110110 main.counter +1main.clk diff --git a/regression/nuterm/counters/counter1/trace.5 b/regression/nuterm/counters/counter1/trace.5 new file mode 100644 index 00000000..328a71c5 --- /dev/null +++ b/regression/nuterm/counters/counter1/trace.5 @@ -0,0 +1,38 @@ +$date + Sun Jan 7 16:33:39 2024 +$end +$timescale + 1ns +$end +$scope module main $end + $var reg 32 main.counter main.counter [31:0] $end + $var wire 1 main.clk main.clk $end +$upscope $end +$enddefinitions $end +#0 +b00010000000000000000000000000000 main.counter +1main.clk +#1 +b00001111111111111111111111111111 main.counter +#2 +b00001111111111111111111111111110 main.counter +#3 +b00001111111111111111111111111101 main.counter +#4 +b00001111111111111111111111111100 main.counter +0main.clk +#5 +b00001111111111111111111111111011 main.counter +1main.clk +#6 +b00001111111111111111111111111010 main.counter +0main.clk +#7 +b00001111111111111111111111111001 main.counter +1main.clk +#8 +b00001111111111111111111111111000 main.counter +#9 +b00001111111111111111111111110111 main.counter +#10 +b00001111111111111111111111110110 main.counter diff --git a/regression/nuterm/counters/counter1/trace.6 b/regression/nuterm/counters/counter1/trace.6 new file mode 100644 index 00000000..b5b0e6b6 --- /dev/null +++ b/regression/nuterm/counters/counter1/trace.6 @@ -0,0 +1,42 @@ +$date + Sun Jan 7 16:33:39 2024 +$end +$timescale + 1ns +$end +$scope module main $end + $var reg 32 main.counter main.counter [31:0] $end + $var wire 1 main.clk main.clk $end +$upscope $end +$enddefinitions $end +#0 +b00010000000000000000000000000000 main.counter +0main.clk +#1 +b00001111111111111111111111111111 main.counter +1main.clk +#2 +b00001111111111111111111111111110 main.counter +0main.clk +#3 +b00001111111111111111111111111101 main.counter +#4 +b00001111111111111111111111111100 main.counter +1main.clk +#5 +b00001111111111111111111111111011 main.counter +#6 +b00001111111111111111111111111010 main.counter +0main.clk +#7 +b00001111111111111111111111111001 main.counter +1main.clk +#8 +b00001111111111111111111111111000 main.counter +0main.clk +#9 +b00001111111111111111111111110111 main.counter +1main.clk +#10 +b00001111111111111111111111110110 main.counter +0main.clk diff --git a/regression/nuterm/counters/counter1/trace.7 b/regression/nuterm/counters/counter1/trace.7 new file mode 100644 index 00000000..51912c31 --- /dev/null +++ b/regression/nuterm/counters/counter1/trace.7 @@ -0,0 +1,37 @@ +$date + Sun Jan 7 16:33:39 2024 +$end +$timescale + 1ns +$end +$scope module main $end + $var reg 32 main.counter main.counter [31:0] $end + $var wire 1 main.clk main.clk $end +$upscope $end +$enddefinitions $end +#0 +b00010000000000000000000000000000 main.counter +0main.clk +#1 +b00001111111111111111111111111111 main.counter +#2 +b00001111111111111111111111111110 main.counter +#3 +b00001111111111111111111111111101 main.counter +#4 +b00001111111111111111111111111100 main.counter +1main.clk +#5 +b00001111111111111111111111111011 main.counter +#6 +b00001111111111111111111111111010 main.counter +0main.clk +#7 +b00001111111111111111111111111001 main.counter +#8 +b00001111111111111111111111111000 main.counter +#9 +b00001111111111111111111111110111 main.counter +1main.clk +#10 +b00001111111111111111111111110110 main.counter diff --git a/regression/nuterm/counters/counter1/trace.8 b/regression/nuterm/counters/counter1/trace.8 new file mode 100644 index 00000000..fbcfcfe6 --- /dev/null +++ b/regression/nuterm/counters/counter1/trace.8 @@ -0,0 +1,39 @@ +$date + Sun Jan 7 16:33:39 2024 +$end +$timescale + 1ns +$end +$scope module main $end + $var reg 32 main.counter main.counter [31:0] $end + $var wire 1 main.clk main.clk $end +$upscope $end +$enddefinitions $end +#0 +b00010000000000000000000000000000 main.counter +0main.clk +#1 +b00001111111111111111111111111111 main.counter +1main.clk +#2 +b00001111111111111111111111111110 main.counter +0main.clk +#3 +b00001111111111111111111111111101 main.counter +#4 +b00001111111111111111111111111100 main.counter +1main.clk +#5 +b00001111111111111111111111111011 main.counter +0main.clk +#6 +b00001111111111111111111111111010 main.counter +1main.clk +#7 +b00001111111111111111111111111001 main.counter +#8 +b00001111111111111111111111111000 main.counter +#9 +b00001111111111111111111111110111 main.counter +#10 +b00001111111111111111111111110110 main.counter diff --git a/regression/nuterm/counters/counter1/trace.9 b/regression/nuterm/counters/counter1/trace.9 new file mode 100644 index 00000000..b4d53fb2 --- /dev/null +++ b/regression/nuterm/counters/counter1/trace.9 @@ -0,0 +1,40 @@ +$date + Sun Jan 7 16:33:39 2024 +$end +$timescale + 1ns +$end +$scope module main $end + $var reg 32 main.counter main.counter [31:0] $end + $var wire 1 main.clk main.clk $end +$upscope $end +$enddefinitions $end +#0 +b00010000000000000000000000000000 main.counter +1main.clk +#1 +b00001111111111111111111111111111 main.counter +0main.clk +#2 +b00001111111111111111111111111110 main.counter +1main.clk +#3 +b00001111111111111111111111111101 main.counter +#4 +b00001111111111111111111111111100 main.counter +0main.clk +#5 +b00001111111111111111111111111011 main.counter +#6 +b00001111111111111111111111111010 main.counter +1main.clk +#7 +b00001111111111111111111111111001 main.counter +0main.clk +#8 +b00001111111111111111111111111000 main.counter +#9 +b00001111111111111111111111110111 main.counter +1main.clk +#10 +b00001111111111111111111111110110 main.counter diff --git a/src/nuterm/CMakeLists.txt b/src/nuterm/CMakeLists.txt new file mode 100644 index 00000000..fa238365 --- /dev/null +++ b/src/nuterm/CMakeLists.txt @@ -0,0 +1,13 @@ +cmake_minimum_required(VERSION 3.18 FATAL_ERROR) +project(nuterm) + +find_package(Torch REQUIRED) +set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${TORCH_CXX_FLAGS}") + +add_executable(pytorch_tests pytorch_tests.cpp) +target_link_libraries(pytorch_tests "${TORCH_LIBRARIES}") +set_property(TARGET pytorch_tests PROPERTY CXX_STANDARD 17) + +add_executable(nuterm nuterm_main.cpp vcd_parser.cpp training.cpp) +target_link_libraries(nuterm "${TORCH_LIBRARIES}") +set_property(TARGET nuterm PROPERTY CXX_STANDARD 17) diff --git a/src/nuterm/README b/src/nuterm/README new file mode 100644 index 00000000..d509a713 --- /dev/null +++ b/src/nuterm/README @@ -0,0 +1,7 @@ +wget https://download.pytorch.org/libtorch/cpu/libtorch-macos-2.1.2.zip + +mkdir build +cd build +cmake -DCMAKE_OSX_ARCHITECTURES=x86_64 -DCMAKE_PREFIX_PATH=/Users/kroening/progr/2hw-cbmc/src/nuterm/libtorch .. +cmake --build . --config Release + diff --git a/src/nuterm/nuterm_main.cpp b/src/nuterm/nuterm_main.cpp new file mode 100644 index 00000000..e5db7f5d --- /dev/null +++ b/src/nuterm/nuterm_main.cpp @@ -0,0 +1,258 @@ +/*******************************************************************\ + +Module: nuterm main + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "training.h" +#include "vcd_parser.h" + +#include +#include +#include +#include +#include +#include + +using tracest = std::list; + +tracest read_traces(const std::string &path) +{ + std::vector file_names; + + for(const auto &entry : std::filesystem::directory_iterator(path)) + file_names.push_back(entry.path()); + + // sort to get a fixed ordering + std::sort(file_names.begin(), file_names.end()); + + tracest traces; + + for(const auto &entry : file_names) + { + std::cout << "Reading " << entry << '\n'; + std::ifstream in(entry); + traces.push_back(vcd_parser(in)); + } + + return traces; +} + +std::size_t number_of_transitions(const tracest &traces) +{ + std::size_t result = 0; + + for(auto &trace : traces) + result += trace.states.empty() ? 0 : trace.states.size() - 1; + + return result; +} + +using state_variablest = std::map; + +state_variablest state_variables(const tracest &traces) +{ + // number all identifiers + state_variablest identifiers; + for(auto &trace : traces) + for(auto &state : trace.states) + for(auto &value_change : state.changes) + identifiers.emplace(value_change.first, identifiers.size()); + + return identifiers; +} + +#include + +double vcd_to_value(const std::string &src) +{ + // VCD gives binary values + auto integer = std::stoull(src, nullptr, 2); + //std::cout << "VALUE " << src << " -> " << double(integer) << "\n"; + return integer; +} + +torch::Tensor state_to_tensor( + const state_variablest &state_variables, + const vcdt::statet &state) +{ + std::vector data; + data.resize(state_variables.size(), 0); + for(auto &var : state_variables) + { + auto v_it = state.changes.find(var.first); + if(v_it != state.changes.end()) + data[var.second] = vcd_to_value(v_it->second); + } + + return torch::tensor(data, torch::kFloat64); +} + +torch::Tensor state_pair_to_tensor( + const state_variablest &state_variables, + const vcdt::statet ¤t, + const vcdt::statet &next) +{ + // We make a tensor that has dimensions 2 x |V|. + // The '2' allows for current and next state. + auto tensor_current = state_to_tensor(state_variables, current); + auto tensor_next = state_to_tensor(state_variables, next); + auto tensor_pair = torch::stack({tensor_current, tensor_next}, 0); + // std::cout << "P: " << tensor_pair << "\n" << std::flush; + return std::move(tensor_pair); +} + +std::vector traces_to_tensors( + const state_variablest &state_variables, + const tracest &traces) +{ + auto t = number_of_transitions(traces); + + std::vector result; + result.reserve(t); + + for(auto &trace : traces) + { + const auto full_trace = trace.full_trace(); + for(std::size_t t = 1; t < full_trace.size(); t++) + { + auto ¤t = full_trace[t - 1]; + auto &next = full_trace[t]; + auto tensor = state_pair_to_tensor(state_variables, current, next); + result.push_back(std::move(tensor)); + } + } + + return result; +} + +std::string sum(const std::vector &terms) +{ + std::string result; + for(auto &term : terms) + { + if(result.empty()) + result = term; + else if(term != "" && term[0] == '-') + result += term; + else + result += "+" + term; + } + return result; +} + +std::string ranking_net_to_string( + const state_variablest &state_variables, + const std::shared_ptr net) +{ + std::vector terms; + + auto weight = net->named_parameters()["fc1.weight"]; + auto bias = net->named_parameters()["fc1.bias"]; + + for(auto &var : state_variables) + { + assert(var.second < state_variables.size()); + long long weight_int = round(weight[0][var.second].item()); + if(weight_int == 0) + { + } + else if(weight_int == 1) + { + terms.push_back(var.first); + } + else if(weight_int == -1) + { + terms.push_back("-" + var.first); + } + else + { + terms.push_back(std::to_string(weight_int) + "*" + var.first); + } + } + + long long bias_int = round(bias.item()); + terms.push_back(std::to_string(bias_int)); + + return sum(terms); +} + +int main(int argc, const char *argv[]) +{ + // The first argument is the directory with the VCD files. + if(argc != 2) + { + std::cout << "Usage: nuterm trace_directory\n"; + return 1; + } + + const auto traces = read_traces(argv[1]); + + auto state_variables = ::state_variables(traces); + + if(state_variables.empty()) + { + std::cout << "no state variables\n"; + return 1; + } + + for(auto &v : state_variables) + std::cout << "V" << v.second << "=" << v.first << '\n'; + + torch::manual_seed(0); + + const auto tensors = traces_to_tensors(state_variables, traces); + + std::cout << "Got " << tensors.size() << " transitions\n"; + + const auto net = std::make_shared(state_variables.size()); + +#if 0 + for(auto &p : net->named_parameters()) + { + std::cout << p.key() << ": " << p.value() << "\n"; + } +#endif + + { + auto weight = net->named_parameters()["fc1.weight"]; + auto bias = net->named_parameters()["fc1.bias"]; + assert(weight.dim() == 2); + assert(bias.dim() == 1); + std::cout << "#weights: " << weight.size(1) << "\n"; + assert(weight.size(1) == state_variables.size()); + +#if 0 + for(auto &var : state_variables) + { + assert(var.second < state_variables.size()); + std::cout << "weight " << var.first << " = " << weight[0][var.second].item() << '\n'; + } + + std::cout << "bias: " << bias.item() << "\n"; +#endif + } + + std::cout << "TRAINING\n"; + ranking_function_training(net, tensors); + + { + auto weight = net->named_parameters()["fc1.weight"]; + auto bias = net->named_parameters()["fc1.bias"]; + for(auto &var : state_variables) + { + assert(var.second < state_variables.size()); + std::cout << "weight " << var.first << " = " + << (long long)round(weight[0][var.second].item()) << ' ' + << weight[0][var.second].item() << '\n'; + } + + std::cout << "bias: " << (long long)(round(bias.item())) << ' ' + << bias.item() << "\n"; + } + + std::cout << "RESULT: " << ranking_net_to_string(state_variables, net) + << '\n'; +} diff --git a/src/nuterm/pytorch_tests.cpp b/src/nuterm/pytorch_tests.cpp new file mode 100644 index 00000000..b5f5120f --- /dev/null +++ b/src/nuterm/pytorch_tests.cpp @@ -0,0 +1,436 @@ +#include + +#include +#include + +struct test_net : torch::nn::Module +{ + test_net() + { + fc1 = register_module("fc1", torch::nn::Linear(1, 1)); + fc1->to(torch::kFloat64); + } + + torch::Tensor forward(torch::Tensor x) + { + return fc1->forward(x); + } + + torch::nn::Linear fc1{nullptr}; +}; + +struct test_batcht +{ + torch::Tensor data; + torch::Tensor target; +}; + +void train( + std::shared_ptr net, + const std::vector &batches) +{ + torch::optim::SGD optimizer(net->parameters(), /*lr=*/0.1); + + for(size_t epoch = 1; epoch <= 30; ++epoch) + { + size_t batch_index = 0; + + // Iterate the data loader to yield batches from the dataset. + for(auto &batch : batches) + { + // Reset gradients. + optimizer.zero_grad(); + + // Execute the model on the input data. + torch::Tensor prediction = net->forward(batch.data); + + // Compute a loss value to judge the prediction of our model. + torch::Tensor loss = torch::mse_loss(prediction, batch.target); + + // Compute gradients of the loss w.r.t. the parameters of our model. + loss.backward(); + + // Update the parameters based on the calculated gradients. + optimizer.step(); + } + } +} + +void pytorch_test1() +{ + torch::manual_seed(0); + + auto net = std::make_shared(); + + std::vector batches = { + {.data = torch::full({1}, /*value*/ 0, torch::kFloat64), + .target = torch::full({1}, /*value*/ 10, torch::kFloat64)}, + {.data = torch::full({1}, /*value*/ 1, torch::kFloat64), + .target = torch::full({1}, /*value*/ 11, torch::kFloat64)}, + {.data = torch::full({1}, /*value*/ 2, torch::kFloat64), + .target = torch::full({1}, /*value*/ 12, torch::kFloat64)}}; + + train(net, batches); + + assert(round(net->parameters()[0].item()) == 1); // coefficient + assert(round(net->parameters()[1].item()) == 10); // bias +} + +void pytorch_test2() +{ + torch::manual_seed(0); + + auto net = std::make_shared(); + + std::vector batches = { + {.data = torch::full({1}, /*value*/ 0, torch::kFloat64), + .target = torch::full({1}, /*value*/ 0, torch::kFloat64)}, + {.data = torch::full({1}, /*value*/ 1, torch::kFloat64), + .target = torch::full({1}, /*value*/ -1, torch::kFloat64)}, + {.data = torch::full({1}, /*value*/ 2, torch::kFloat64), + .target = torch::full({1}, /*value*/ -2, torch::kFloat64)}}; + + train(net, batches); + + assert(round(net->parameters()[0].item()) == -1); // coefficient + assert(round(net->parameters()[1].item()) == 0); // bias +} + +void pytorch_test3() +{ + torch::manual_seed(0); + + auto net = std::make_shared(); + + std::vector batches = { + {.data = torch::full({1}, /*value*/ 0, torch::kFloat64), + .target = torch::full({1}, /*value*/ 10, torch::kFloat64)}, + {.data = torch::full({1}, /*value*/ 1, torch::kFloat64), + .target = torch::full({1}, /*value*/ 9, torch::kFloat64)}, + {.data = torch::full({1}, /*value*/ 2, torch::kFloat64), + .target = torch::full({1}, /*value*/ 8, torch::kFloat64)}}; + + train(net, batches); + + assert(round(net->parameters()[0].item()) == -1); // coefficient + assert(round(net->parameters()[1].item()) == 10); // bias +} + +void pytorch_test4() +{ + torch::manual_seed(0); + + auto net = std::make_shared(); + + std::vector data = { + torch::full({1}, /*value*/ 0, torch::kFloat64), + torch::full({1}, /*value*/ 1, torch::kFloat64), + torch::full({1}, /*value*/ 2, torch::kFloat64), + torch::full({1}, /*value*/ 3, torch::kFloat64), + torch::full({1}, /*value*/ 4, torch::kFloat64), + torch::full({1}, /*value*/ 5, torch::kFloat64)}; + + auto my_loss = [](const torch::Tensor &input) -> torch::Tensor + { return input.abs(); }; + + torch::optim::SGD optimizer(net->parameters(), /*lr=*/0.1); + + for(size_t epoch = 1; epoch <= 10; ++epoch) + { + size_t batch_index = 0; + + // Iterate the data loader to yield batches from the dataset. + for(auto &batch : data) + { + // Reset gradients. + optimizer.zero_grad(); + + // Execute the model on the input data. + torch::Tensor prediction = net->forward(batch); + + // Compute a loss value to judge the prediction of our model. + torch::Tensor loss = my_loss(prediction); + + // Compute gradients of the loss w.r.t. the parameters of our model. + loss.backward(); + + // Update the parameters based on the calculated gradients. + optimizer.step(); + } + } + + assert(round(net->parameters()[0].item()) == 0); // coefficient + assert(round(net->parameters()[1].item()) == 0); // bias +} + +struct test_net2 : torch::nn::Module +{ + explicit test_net2(std::size_t number_of_inputs) + { + fc1 = register_module("fc1", torch::nn::Linear(number_of_inputs, 1)); + fc1->to(torch::kFloat64); + } + + torch::Tensor forward(torch::Tensor x) + { + x = fc1->forward(x); + // the relu ensures x is bounded from below + x = torch::relu(x); + return x; + } + + torch::nn::Linear fc1{nullptr}; +}; + +void pytorch_test5() +{ + torch::manual_seed(0); + + auto net = std::make_shared(2); + + std::vector data = { + torch::tensor({0, 0}, torch::kFloat64), + torch::tensor({1, 0}, torch::kFloat64), + torch::tensor({2, 0}, torch::kFloat64), + torch::tensor({3, 0}, torch::kFloat64), + torch::tensor({4, 0}, torch::kFloat64), + torch::tensor({5, 0}, torch::kFloat64)}; + + auto my_loss = [](const torch::Tensor &input) -> torch::Tensor + { return input.abs(); }; + + torch::optim::SGD optimizer(net->parameters(), /*lr=*/0.1); + + for(size_t epoch = 1; epoch <= 10; ++epoch) + { + size_t batch_index = 0; + + // Iterate the data loader to yield batches from the dataset. + for(auto &batch : data) + { + // Reset gradients. + optimizer.zero_grad(); + + // Execute the model on the input data. + torch::Tensor prediction = net->forward(batch); + + // Compute a loss value to judge the prediction of our model. + torch::Tensor loss = my_loss(prediction); + + // Compute gradients of the loss w.r.t. the parameters of our model. + loss.backward(); + + // Update the parameters based on the calculated gradients. + optimizer.step(); + } + } + + assert(round(net->parameters()[0][0][0].item()) == 0); // coefficient + assert(round(net->parameters()[0][0][1].item()) == 0); // coefficient + assert(round(net->parameters()[1].item()) == -1); // bias +} + +void pytorch_test6() +{ + torch::manual_seed(0); + + auto net = std::make_shared(1); + + // one state variable, pairs are transitions + std::vector data = { + torch::stack( + {torch::tensor({5}, torch::kFloat64), + torch::tensor({4}, torch::kFloat64)}), + torch::stack( + {torch::tensor({4}, torch::kFloat64), + torch::tensor({3}, torch::kFloat64)}), + torch::stack( + {torch::tensor({3}, torch::kFloat64), + torch::tensor({2}, torch::kFloat64)}), + torch::stack( + {torch::tensor({2}, torch::kFloat64), + torch::tensor({1}, torch::kFloat64)}), + torch::stack( + {torch::tensor({1}, torch::kFloat64), + torch::tensor({0}, torch::kFloat64)})}; + + auto my_loss = + [](const torch::Tensor &curr, const torch::Tensor &next) -> torch::Tensor + { return torch::relu(next - curr + 1.0); }; + + torch::optim::SGD optimizer(net->parameters(), /*lr=*/0.1); + + for(size_t epoch = 1; epoch <= 3; ++epoch) + { + size_t batch_index = 0; + + // Iterate the data loader to yield batches from the dataset. + for(auto &batch : data) + { + // Reset gradients. + optimizer.zero_grad(); + + // Execute the model on the input data. + torch::Tensor prediction_curr = net->forward(batch[0]); + torch::Tensor prediction_next = net->forward(batch[1]); + + // Compute a loss value to judge the prediction of our model. + torch::Tensor loss = my_loss(prediction_curr, prediction_next); + + // Compute gradients of the loss w.r.t. the parameters of our model. + loss.backward(); + + // Update the parameters based on the calculated gradients. + optimizer.step(); + } + } + + assert(round(net->parameters()[0].item()) == 1); // coefficient + assert(round(net->parameters()[1].item()) == 1); // bias +} + +void pytorch_test7() +{ + torch::manual_seed(0); + + auto net = std::make_shared(2); + + // two state variables, pairs are transitions + std::vector data = { + torch::stack( + {torch::tensor({0, 5}, torch::kFloat64), + torch::tensor({0, 4}, torch::kFloat64)}), + torch::stack( + {torch::tensor({0, 4}, torch::kFloat64), + torch::tensor({0, 3}, torch::kFloat64)}), + torch::stack( + {torch::tensor({0, 3}, torch::kFloat64), + torch::tensor({0, 2}, torch::kFloat64)}), + torch::stack( + {torch::tensor({0, 2}, torch::kFloat64), + torch::tensor({0, 1}, torch::kFloat64)}), + torch::stack( + {torch::tensor({0, 1}, torch::kFloat64), + torch::tensor({0, 0}, torch::kFloat64)})}; + + auto my_loss = + [](const torch::Tensor &curr, const torch::Tensor &next) -> torch::Tensor + { return torch::relu(next - curr + 1.0); }; + + torch::optim::SGD optimizer(net->parameters(), /*lr=*/0.1); + + for(size_t epoch = 1; epoch <= 3; ++epoch) + { + size_t batch_index = 0; + + // Iterate the data loader to yield batches from the dataset. + for(auto &batch : data) + { + // Reset gradients. + optimizer.zero_grad(); + + // Execute the model on the input data. + torch::Tensor prediction_curr = net->forward(batch[0]); + torch::Tensor prediction_next = net->forward(batch[1]); + + // Compute a loss value to judge the prediction of our model. + torch::Tensor loss = my_loss(prediction_curr, prediction_next); + + // Compute gradients of the loss w.r.t. the parameters of our model. + loss.backward(); + //std::cout << "L " << loss.item() << "\n"; + + // Update the parameters based on the calculated gradients. + optimizer.step(); + } + } + + //std::cout << "XX: " << net->parameters() << "\n"; + //std::cout << "C: " << net->parameters()[0][0][0].item() << "\n"; + //std::cout << "C: " << net->parameters()[0][0][1].item() << "\n"; + //std::cout << "B: " << net->parameters()[1].item() << "\n"; + assert(round(net->parameters()[0][0][0].item()) == 0); // coefficient + assert(round(net->parameters()[0][0][1].item()) == 1); // coefficient + assert(round(net->parameters()[1].item()) == 0); // bias +} + +void pytorch_test8() +{ + torch::manual_seed(0); + + auto net = std::make_shared(1); + + // one state variable, pairs are transitions + std::vector data = { + torch::stack( + {torch::tensor({1}, torch::kFloat64), + torch::tensor({2}, torch::kFloat64)}), + torch::stack( + {torch::tensor({2}, torch::kFloat64), + torch::tensor({3}, torch::kFloat64)}), + torch::stack( + {torch::tensor({3}, torch::kFloat64), + torch::tensor({4}, torch::kFloat64)}), + torch::stack( + {torch::tensor({4}, torch::kFloat64), + torch::tensor({5}, torch::kFloat64)}), + torch::stack( + {torch::tensor({5}, torch::kFloat64), + torch::tensor({6}, torch::kFloat64)})}; + + auto my_loss = + [](const torch::Tensor &curr, const torch::Tensor &next) -> torch::Tensor + { + // std::cout << "LL " << from.item() << " -> " << to.item() << "\n"; + return torch::relu(next - curr + 1.0); + }; + + //torch::optim::SGD optimizer(net->parameters(), /*lr=*/0.1); + torch::optim::Adam optimizer(net->parameters(), /*lr=*/0.1); + + for(size_t epoch = 1; epoch <= 30; ++epoch) + { + size_t batch_index = 0; + + // Iterate the data loader to yield batches from the dataset. + for(auto &batch : data) + { + // Reset gradients. + optimizer.zero_grad(); + + // Execute the model on the input data. + torch::Tensor prediction_curr = net->forward(batch[0]); + torch::Tensor prediction_next = net->forward(batch[1]); + + // Compute a loss value to judge the prediction of our model. + torch::Tensor loss = my_loss(prediction_curr, prediction_next); + + // Compute gradients of the loss w.r.t. the parameters of our model. + loss.backward(); + + // Update the parameters based on the calculated gradients. + optimizer.step(); + + // std::cout << "L " << loss.item() << "\n"; + } + } + + //std::cout << "C: " << net->parameters()[0].item() << "\n"; + //std::cout << "B: " << net->parameters()[1].item() << "\n"; + assert(round(net->parameters()[0].item()) == -1); // coefficient + assert(round(net->parameters()[1].item()) == 6); // bias +} + +int main() +{ + std::cout << "Running tests\n"; + + pytorch_test1(); + pytorch_test2(); + pytorch_test3(); + pytorch_test4(); + pytorch_test5(); + pytorch_test6(); + pytorch_test7(); + pytorch_test8(); +} diff --git a/src/nuterm/training.cpp b/src/nuterm/training.cpp new file mode 100644 index 00000000..60a74850 --- /dev/null +++ b/src/nuterm/training.cpp @@ -0,0 +1,78 @@ +/*******************************************************************\ + +Module: Ranking Function Training + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "training.h" + +#include + +const double delta = 1; + +#include + +void ranking_function_training( + std::shared_ptr net, + const std::vector &data) +{ + auto ranking_function_loss = + [](const torch::Tensor &curr, const torch::Tensor &next) -> torch::Tensor + { + assert(curr.dim() == 1 && next.dim() == 1); + // The ranking needs to decrease from 'curr' to 'next' + // by at least 'delta'. Anything less than that is loss. + return torch::relu(next - curr + delta); + }; + + torch::optim::SGD optimizer(net->parameters(), /*lr=*/0.1); + torch::Tensor last_loss = {}; + + for(size_t epoch = 1; epoch <= 10; ++epoch) + { + size_t batch_index = 0; + + // Iterate the data loader to yield batches from the dataset. + for(auto &batch : data) + { + // Reset gradients. + optimizer.zero_grad(); + + // Execute the model on the input data. + assert(batch.size(1) == 2); + torch::Tensor prediction_curr = net->forward(batch[0]); + torch::Tensor prediction_next = net->forward(batch[1]); + // std::cout << "B: " << std::fixed << batch[0][1].item() << " -> " << batch[1][1].item() << "\n"; + // std::cout << "R: " << std::fixed << prediction_curr.item() << " -> " << prediction_next.item() << "\n"; + + // Compute a loss value to judge the prediction of our model. + torch::Tensor loss = + ranking_function_loss(prediction_curr, prediction_next); + + // Compute gradients of the loss w.r.t. the parameters of our model. + loss.backward(); + + // Update the parameters based on the calculated gradients. + optimizer.step(); + +#if 0 + if(1) + { + std::cout << "Epoch: " << epoch << " | Batch: " << batch_index + << " | Loss: " << std::fixed << std::setprecision(3) + << loss.item() << '\n'; + //torch::save(net, "net.pt"); + } +#endif + + batch_index++; + + last_loss = loss; + } + } + + std::cout << "Final loss: " << std::fixed << std::setprecision(3) + << last_loss.item() << '\n'; +} diff --git a/src/nuterm/training.h b/src/nuterm/training.h new file mode 100644 index 00000000..fd782c45 --- /dev/null +++ b/src/nuterm/training.h @@ -0,0 +1,40 @@ +/*******************************************************************\ + +Module: Training + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include + +//#include + +struct RankingNet : torch::nn::Module +{ + explicit RankingNet(std::size_t number_of_state_variables) + { + fc1 = + register_module("fc1", torch::nn::Linear(number_of_state_variables, 1)); + fc1->to(torch::kFloat64); +#if 0 + // The default values for nn::Linear are kaiming_uniform(sqrt(5)). + // Use zeros instead. + fc1->named_parameters()["weight"].fill_(0, torch::requires_grad()); + fc1->named_parameters()["bias"] = torch::zeros({1}); // .fill_(0, torch::requires_grad()); + std::cout << "CON: " << fc1->named_parameters()["bias"].item() << "\n"; +#endif + } + + torch::Tensor forward(torch::Tensor x) + { + // the relu ensures that the function is bounded from below by 0 + return torch::relu(fc1->forward(x)); + } + + torch::nn::Linear fc1{nullptr}; +}; + +void ranking_function_training( + const std::shared_ptr net, + const std::vector &); diff --git a/src/nuterm/vcd_parser.cpp b/src/nuterm/vcd_parser.cpp new file mode 100644 index 00000000..1c2cfae0 --- /dev/null +++ b/src/nuterm/vcd_parser.cpp @@ -0,0 +1,123 @@ +/*******************************************************************\ + +Module: VCD Parser + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "vcd_parser.h" + +#include + +static bool is_whitespace(char ch) +{ + return ch == ' ' || ch == '\t' || ch == '\r' || ch == '\n'; +} + +static std::string vcd_token(std::istream &in) +{ + std::string token; + char ch; + while(!in.eof()) + { + ch = in.get(); + if(is_whitespace(ch)) + { + if(!token.empty()) + return token; + } + else + token += ch; + } + + return token; +} + +void vcd_command(vcdt &, const std::string &token, std::istream &in) +{ + // look for $end + while(true) + { + auto t = vcd_token(in); + if(t.empty() || t == "$end") + return; + } +} + +vcdt vcd_parser(std::istream &in) +{ + vcdt vcd; + + while(true) + { + auto token = vcd_token(in); + if(token.empty()) + break; + switch(token[0]) + { + case '$': + vcd_command(vcd, token, in); + break; + case '#': + // #decimal + vcd.simulation_time(token.substr(1, std::string::npos)); + break; + case '0': + case '1': + case 'x': + case 'X': + case 'z': + case 'Z': + // (0 | 1 | x | X | z | Z) identifier + // one token, no space + vcd.value_change(token.substr(0, 1), token.substr(1)); + break; + case 'b': + case 'B': + // (b | B) value identifier + // two tokens, space between value and identifier + vcd.value_change(token.substr(1), vcd_token(in)); + break; + case 'r': + case 'R': + // (r | R) value identifier + // two tokens, space between value and identifier + vcd.value_change(token.substr(1), vcd_token(in)); + break; + default: + break; + } + } + + return vcd; +} + +std::vector vcdt::full_trace() const +{ + std::vector result; + result.reserve(states.size()); + + for(auto &state : states) + { + if(result.empty()) + { + result.push_back(state); + } + else + { + statet full_state(state.simulation_time); + + // copy the previous map + full_state.changes = result.back().changes; + + // apply the changes + for(auto &change : state.changes) + full_state.changes[change.first] = change.second; + + result.push_back(std::move(state)); + } + } + + return result; +} diff --git a/src/nuterm/vcd_parser.h b/src/nuterm/vcd_parser.h new file mode 100644 index 00000000..5c08bae8 --- /dev/null +++ b/src/nuterm/vcd_parser.h @@ -0,0 +1,48 @@ +/*******************************************************************\ + +Module: VCD Parser + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include +#include +#include +#include + +class vcdt +{ +public: + using value_mapt = std::map; + + struct statet + { + explicit statet(std::string t) : simulation_time(std::move(t)) + { + } + + std::string simulation_time; + value_mapt changes; + }; + + std::vector states; + + void simulation_time(const std::string &t) + { + states.push_back(statet(t)); + } + + void value_change(std::string value, const std::string &identifier) + { + if(states.empty()) + simulation_time(""); + states.back().changes[identifier] = std::move(value); + } + + // Expand the differential trace into a trace of full states, + // including all unchanged values. + std::vector full_trace() const; +}; + +vcdt vcd_parser(std::istream &);