From 535bf95d3c6e382204a91bd6816ea3371234a2dd Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 20 Oct 2023 14:38:20 -0500 Subject: [PATCH] Use only symbols from the original goto as terminals in synthesizer Collecting variables from trace will also collect those variables added during loop transformation, such as the car variables. Such variables should not appear in the loop contracts. This commit erases them from the terminals of the enumearting grammar used by the synthesizer. --- .../enumerative_loop_contracts_synthesizer.cpp | 18 ++++++++++++++++++ .../enumerative_loop_contracts_synthesizer.h | 6 +++++- 2 files changed, 23 insertions(+), 1 deletion(-) diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp index 4b4b04c5c67..fd55145916c 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp @@ -49,6 +49,12 @@ void replace_tmp_post( std::vector construct_terminals(const std::set &symbols) { + // Construct a vector of terminal expressions. + // Terminals include: + // 1: scalar type variables and their loop_entry version. + // 2: offsets of pointers and loop_entry of pointers. + // 3: constants 0 and 1. + std::vector result; for(const auto &e : symbols) { @@ -244,6 +250,18 @@ enumerative_loop_contracts_synthesizert::compute_dependent_symbols( for(const auto &e : live_vars) find_symbols(e, result); + // Erase all variables added during loop transformations---they are not in + // the original symbol table. + for(auto it = result.begin(); it != result.end();) + { + if(original_symbol_table.lookup(it->get_identifier()) == nullptr) + { + it = result.erase(it); + } + else + it++; + } + return result; } diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h index 9dbda380797..f39d1f6700b 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h @@ -36,7 +36,8 @@ class enumerative_loop_contracts_synthesizert messaget &log) : loop_contracts_synthesizer_baset(goto_model, log), options(options), - ns(goto_model.symbol_table) + ns(goto_model.symbol_table), + original_symbol_table(goto_model.symbol_table) { } @@ -97,6 +98,9 @@ class enumerative_loop_contracts_synthesizert /// Map from tmp_post variables to their original variables. std::unordered_map tmp_post_map; + + /// Symbol table of the input goto model + const symbol_tablet original_symbol_table; }; // NOLINTNEXTLINE(whitespace/line_length)