diff --git a/CHANGELOG b/CHANGELOG index f7505385..35fa6228 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -5,6 +5,7 @@ use --bmc-with-assumptions to re-enable the previous algorithm. * SystemVerilog: streaming concatenation {<<{...}} and {>>{...}} * SystemVerilog: set membership operator +* word-level BMC: LTL/SVA to Buechi with --buechi # EBMC 5.3 diff --git a/regression/ebmc/Buechi/FGp1.desc b/regression/ebmc/Buechi/FGp1.desc new file mode 100644 index 00000000..bc71b789 --- /dev/null +++ b/regression/ebmc/Buechi/FGp1.desc @@ -0,0 +1,9 @@ +CORE +FGp1.smv +--buechi --bound 2 +^\[.*\] F G p: PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/FGp1.smv b/regression/ebmc/Buechi/FGp1.smv new file mode 100644 index 00000000..0dd410b7 --- /dev/null +++ b/regression/ebmc/Buechi/FGp1.smv @@ -0,0 +1,9 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := FALSE; + next(p) := TRUE; + +-- should pass +LTLSPEC F G p diff --git a/regression/ebmc/Buechi/Fp1.desc b/regression/ebmc/Buechi/Fp1.desc new file mode 100644 index 00000000..25032d4f --- /dev/null +++ b/regression/ebmc/Buechi/Fp1.desc @@ -0,0 +1,9 @@ +CORE +Fp1.smv +--buechi --bound 2 +^\[.*\] F p: PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/Fp1.smv b/regression/ebmc/Buechi/Fp1.smv new file mode 100644 index 00000000..4c220d22 --- /dev/null +++ b/regression/ebmc/Buechi/Fp1.smv @@ -0,0 +1,9 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := FALSE; + next(p) := TRUE; + +-- should pass +LTLSPEC F p diff --git a/regression/ebmc/Buechi/GFp1.desc b/regression/ebmc/Buechi/GFp1.desc new file mode 100644 index 00000000..878331a9 --- /dev/null +++ b/regression/ebmc/Buechi/GFp1.desc @@ -0,0 +1,9 @@ +CORE +GFp1.smv +--buechi --bound 2 +^\[.*\] G F p: PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/GFp1.smv b/regression/ebmc/Buechi/GFp1.smv new file mode 100644 index 00000000..cd99bc0f --- /dev/null +++ b/regression/ebmc/Buechi/GFp1.smv @@ -0,0 +1,9 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := FALSE; + next(p) := !p; + +-- should pass +LTLSPEC G F p diff --git a/regression/ebmc/Buechi/Gp1.desc b/regression/ebmc/Buechi/Gp1.desc new file mode 100644 index 00000000..87af6367 --- /dev/null +++ b/regression/ebmc/Buechi/Gp1.desc @@ -0,0 +1,9 @@ +CORE +Gp1.smv +--buechi --bound 2 +^\[.*\] G p: PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/Gp1.smv b/regression/ebmc/Buechi/Gp1.smv new file mode 100644 index 00000000..d0fcb3ab --- /dev/null +++ b/regression/ebmc/Buechi/Gp1.smv @@ -0,0 +1,9 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := TRUE; + next(p) := TRUE; + +-- should pass +LTLSPEC G p diff --git a/regression/ebmc/Buechi/Xp1.desc b/regression/ebmc/Buechi/Xp1.desc new file mode 100644 index 00000000..75c6937f --- /dev/null +++ b/regression/ebmc/Buechi/Xp1.desc @@ -0,0 +1,9 @@ +CORE +Xp1.smv +--buechi --bound 2 +^\[.*\] X p: PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/Xp1.smv b/regression/ebmc/Buechi/Xp1.smv new file mode 100644 index 00000000..424cf3f0 --- /dev/null +++ b/regression/ebmc/Buechi/Xp1.smv @@ -0,0 +1,9 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := FALSE; + next(p) := TRUE; + +-- should pass +LTLSPEC X p diff --git a/regression/ebmc/Buechi/and1.desc b/regression/ebmc/Buechi/and1.desc new file mode 100644 index 00000000..ff3daa95 --- /dev/null +++ b/regression/ebmc/Buechi/and1.desc @@ -0,0 +1,9 @@ +CORE +and1.smv +--buechi --bound 2 +^\[.*\] X p & X q: PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/and1.smv b/regression/ebmc/Buechi/and1.smv new file mode 100644 index 00000000..fa313d5e --- /dev/null +++ b/regression/ebmc/Buechi/and1.smv @@ -0,0 +1,15 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := FALSE; + next(p) := TRUE; + +VAR q : boolean; + +ASSIGN init(q) := FALSE; + next(q) := TRUE; + +-- should pass +LTLSPEC X p & X q + diff --git a/regression/ebmc/Buechi/and2.desc b/regression/ebmc/Buechi/and2.desc new file mode 100644 index 00000000..ae9c56f2 --- /dev/null +++ b/regression/ebmc/Buechi/and2.desc @@ -0,0 +1,9 @@ +CORE +and2.smv +--buechi --bound 2 +^\[.*\] X \(p & q\): PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/and2.smv b/regression/ebmc/Buechi/and2.smv new file mode 100644 index 00000000..3ad65c69 --- /dev/null +++ b/regression/ebmc/Buechi/and2.smv @@ -0,0 +1,15 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := FALSE; + next(p) := TRUE; + +VAR q : boolean; + +ASSIGN init(q) := FALSE; + next(q) := TRUE; + +-- should pass +LTLSPEC X (p & q) + diff --git a/regression/ebmc/Buechi/iff1.desc b/regression/ebmc/Buechi/iff1.desc new file mode 100644 index 00000000..bde2e436 --- /dev/null +++ b/regression/ebmc/Buechi/iff1.desc @@ -0,0 +1,9 @@ +CORE +iff1.smv +--buechi --bound 2 +^\[.*\] X p <-> X q: PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/iff1.smv b/regression/ebmc/Buechi/iff1.smv new file mode 100644 index 00000000..6fc3d251 --- /dev/null +++ b/regression/ebmc/Buechi/iff1.smv @@ -0,0 +1,14 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := TRUE; + next(p) := FALSE; + +VAR q : boolean; + +ASSIGN init(q) := TRUE; + next(q) := FALSE; + +-- should pass +LTLSPEC X p <-> X q diff --git a/regression/ebmc/Buechi/iff2.desc b/regression/ebmc/Buechi/iff2.desc new file mode 100644 index 00000000..737e3edc --- /dev/null +++ b/regression/ebmc/Buechi/iff2.desc @@ -0,0 +1,9 @@ +CORE +iff2.smv +--buechi --bound 2 +^\[.*\] X \(p <-> q\): PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/iff2.smv b/regression/ebmc/Buechi/iff2.smv new file mode 100644 index 00000000..6af00543 --- /dev/null +++ b/regression/ebmc/Buechi/iff2.smv @@ -0,0 +1,14 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := TRUE; + next(p) := FALSE; + +VAR q : boolean; + +ASSIGN init(q) := TRUE; + next(q) := FALSE; + +-- should pass +LTLSPEC X (p <-> q) diff --git a/regression/ebmc/Buechi/implies1.desc b/regression/ebmc/Buechi/implies1.desc new file mode 100644 index 00000000..d90489e7 --- /dev/null +++ b/regression/ebmc/Buechi/implies1.desc @@ -0,0 +1,9 @@ +CORE +implies1.smv +--buechi --bound 2 +^\[.*\] X p -> X q: PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/implies1.smv b/regression/ebmc/Buechi/implies1.smv new file mode 100644 index 00000000..4651e134 --- /dev/null +++ b/regression/ebmc/Buechi/implies1.smv @@ -0,0 +1,14 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := TRUE; + next(p) := FALSE; + +VAR q : boolean; + +ASSIGN init(q) := TRUE; + next(q) := FALSE; + +-- should pass +LTLSPEC X p -> X q diff --git a/regression/ebmc/Buechi/implies2.desc b/regression/ebmc/Buechi/implies2.desc new file mode 100644 index 00000000..d574e71c --- /dev/null +++ b/regression/ebmc/Buechi/implies2.desc @@ -0,0 +1,9 @@ +CORE +implies2.smv +--buechi --bound 2 +^\[.*\] X \(p -> q\): PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/implies2.smv b/regression/ebmc/Buechi/implies2.smv new file mode 100644 index 00000000..345654ca --- /dev/null +++ b/regression/ebmc/Buechi/implies2.smv @@ -0,0 +1,14 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := TRUE; + next(p) := FALSE; + +VAR q : boolean; + +ASSIGN init(q) := TRUE; + next(q) := FALSE; + +-- should pass +LTLSPEC X (p -> q) diff --git a/regression/ebmc/Buechi/or1.desc b/regression/ebmc/Buechi/or1.desc new file mode 100644 index 00000000..63337efa --- /dev/null +++ b/regression/ebmc/Buechi/or1.desc @@ -0,0 +1,9 @@ +CORE +or1.smv +--buechi --bound 2 +^\[.*\] X p \| X q: PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/or1.smv b/regression/ebmc/Buechi/or1.smv new file mode 100644 index 00000000..35a424fd --- /dev/null +++ b/regression/ebmc/Buechi/or1.smv @@ -0,0 +1,14 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := FALSE; + next(p) := TRUE; + +VAR q : boolean; + +ASSIGN init(q) := TRUE; + next(q) := FALSE; + +-- should pass +LTLSPEC X p | X q diff --git a/regression/ebmc/Buechi/or2.desc b/regression/ebmc/Buechi/or2.desc new file mode 100644 index 00000000..82e0c51a --- /dev/null +++ b/regression/ebmc/Buechi/or2.desc @@ -0,0 +1,9 @@ +CORE +or2.smv +--buechi --bound 2 +^\[.*\] X \(p \| q\): PROVED up to bound 2$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/Buechi/or2.smv b/regression/ebmc/Buechi/or2.smv new file mode 100644 index 00000000..b037a3c4 --- /dev/null +++ b/regression/ebmc/Buechi/or2.smv @@ -0,0 +1,14 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := FALSE; + next(p) := TRUE; + +VAR q : boolean; + +ASSIGN init(q) := TRUE; + next(q) := FALSE; + +-- should pass +LTLSPEC X (p | q) diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile index 3b1c3159..4f0122dd 100644 --- a/src/ebmc/Makefile +++ b/src/ebmc/Makefile @@ -15,6 +15,7 @@ SRC = \ ebmc_parse_options.cpp \ ebmc_properties.cpp \ ebmc_solver_factory.cpp \ + instrument_buechi.cpp \ k_induction.cpp \ liveness_to_safety.cpp \ live_signal.cpp \ diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index f2a30cec..0407bf75 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "ebmc_error.h" #include "ebmc_version.h" #include "ic3_engine.h" +#include "instrument_buechi.h" #include "liveness_to_safety.h" #include "neural_liveness.h" #include "property_checker.h" @@ -241,7 +242,14 @@ int ebmc_parse_optionst::doit() if(result != -1) return result; - // possibly apply liveness-to-safety + // LTL/SVA to Buechi? + if(cmdline.isset("buechi")) + instrument_buechi( + ebmc_base.transition_system, + ebmc_base.properties, + ui_message_handler); + + // Liveness to safety? if(cmdline.isset("liveness-to-safety")) liveness_to_safety(ebmc_base.transition_system, ebmc_base.properties); @@ -366,6 +374,7 @@ void ebmc_parse_optionst::help() " {y--systemverilog} \t force SystemVerilog instead of Verilog\n" " {y--reset} {uexpr} \t set up module reset\n" " {y--liveness-to-safety} \t translate liveness properties to safety properties\n" + " {y--buechi} \t translate LTL/SVA properties to Buechi acceptance\n" "\n" "Methods:\n" " {y--k-induction} \t do k-induction with k=bound\n" diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index d6abed1e..3673bf0d 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -48,7 +48,7 @@ class ebmc_parse_optionst:public parse_options_baset "(random-traces)(trace-steps):(random-seed):(traces):" "(random-trace)(random-waveform)" "(bmc-with-assumptions)" - "(liveness-to-safety)" + "(liveness-to-safety)(buechi)" "I:D:(preprocess)(systemverilog)(vl2smv-extensions)" "(warn-implicit-nets)", argc, diff --git a/src/ebmc/instrument_buechi.cpp b/src/ebmc/instrument_buechi.cpp new file mode 100644 index 00000000..78fe606f --- /dev/null +++ b/src/ebmc/instrument_buechi.cpp @@ -0,0 +1,46 @@ +/*******************************************************************\ + +Module: Buechi Automaton Instrumentation + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "instrument_buechi.h" + +#include +#include +#include + +void instrument_buechi( + transition_systemt &transition_system, + ebmc_propertiest &properties, + message_handlert &message_handler) +{ + for(auto &property : properties.properties) + { + if(!property.is_unknown()) + continue; + + // This is for LTL only. + if(!is_LTL(property.normalized_expr)) + continue; + + // But ignore Gp + if(is_Gp(property.normalized_expr)) + continue; + + messaget message(message_handler); + message.debug() << "Translating " << property.description << " to Buechi" + << messaget::eom; + + // make the automaton for the negation of the property + auto buechi = ltl_to_buechi( + not_exprt{property.normalized_expr}, "buechi::", message_handler); + + // add the automaton to the transition system + + // replace the normalized property expression + property.normalized_expr = G_exprt{F_exprt{buechi.liveness_signal}}; + } +} diff --git a/src/ebmc/instrument_buechi.h b/src/ebmc/instrument_buechi.h new file mode 100644 index 00000000..af200539 --- /dev/null +++ b/src/ebmc/instrument_buechi.h @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: Buechi Automaton Instrumentation + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +/// \file +/// Buechi Automaton Instrumentation + +#ifndef EBMC_BUECHI_AUTOMATON_INSTRUMENTATION_H +#define EBMC_BUECHI_AUTOMATON_INSTRUMENTATION_H + +#include + +#include "ebmc_properties.h" +#include "transition_system.h" + +void instrument_buechi( + transition_systemt &, + ebmc_propertiest &, + message_handlert &); + +#endif // EBMC_BUECHI_AUTOMATON_INSTRUMENTATION_H diff --git a/src/temporal-logic/Makefile b/src/temporal-logic/Makefile index 2cb1e020..22edfc33 100644 --- a/src/temporal-logic/Makefile +++ b/src/temporal-logic/Makefile @@ -1,4 +1,7 @@ -SRC = nnf.cpp \ +SRC = hoa.cpp \ + ltl_to_buechi.cpp \ + ltl_sva_to_string.cpp \ + nnf.cpp \ normalize_property.cpp \ temporal_logic.cpp \ trivial_sva.cpp \ diff --git a/src/temporal-logic/hoa.cpp b/src/temporal-logic/hoa.cpp new file mode 100644 index 00000000..7564f873 --- /dev/null +++ b/src/temporal-logic/hoa.cpp @@ -0,0 +1,530 @@ +/*******************************************************************\ + +Module: Hanoi Omega Automata (HOA) Format + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "hoa.h" + +#include + +#include + +#include +#include + +class hoa_tokenizert +{ +public: + explicit hoa_tokenizert(std::istream &_in) : in(_in) + { + } + + struct tokent + { + tokent() = default; + explicit tokent(char ch) : text(1, ch) + { + } + + std::string text, string; + bool is_string() const + { + return text.empty(); + } + bool is_state() const + { + return text == "State:"; + } + bool is_body() const + { + return text == "--BODY--"; + } + bool is_end() const + { + return text == "--END--"; + } + bool is_headername() const + { + // Headernames end on a colon, and are not quoted strings. + return !text.empty() && text.back() == ':'; + } + }; + + const tokent &peek() + { + if(!token_opt.has_value()) + token_opt = get_token(in); + return token_opt.value(); + } + + tokent consume() + { + if(token_opt.has_value()) + { + auto value = std::move(token_opt.value()); + token_opt = {}; + return value; + } + else + return get_token(in); + } + +protected: + std::istream ∈ + static tokent get_token(std::istream &); + std::optional token_opt; + static bool is_whitespace(char ch) + { + return ch == ' ' || ch == '\r' || ch == '\n' || ch == '\t'; + } +}; + +hoa_tokenizert::tokent hoa_tokenizert::get_token(std::istream &in) +{ + while(true) + { + char ch; + + if(!in.get(ch)) + throw ebmc_errort() << "EOF while reading HOA"; + + if(is_whitespace(ch)) + { + // ignore + } + else if(ch == '/') + { + if(in.peek() == '*') + { + // comment; these may be nested + in.get(ch); // eat * + std::size_t nesting = 1; + while(true) + { + if(!in.get(ch)) + throw ebmc_errort() << "EOF while reading HOA comment"; + if(ch == '*' && in.peek() == '/') + { + in.get(ch); // eat / + nesting--; + if(nesting == 0) + break; // done + } + else if(ch == '/' && in.peek() == '*') + { + in.get(ch); // eat * + nesting++; + } + } + } + else + { + // just a / + return tokent{ch}; + } + } + else if(ch == '"') + { + // quoted string + tokent token; + while(true) + { + if(!in.get(ch)) + throw ebmc_errort() << "EOF while reading HOA string"; + + if(ch == '"') + return token; + else + token.string += ch; + } + } + else if(isalnum(ch) || ch == '_' || ch == '@' || ch == '-') + { + // BOOLEAN, IDENTIFIER, ANAME, HEADERNAME, INT, --BODY--, --END-- + // Dots appear to be allowed in identifiers, in contrast to the definition. + tokent token; + token.text += ch; + auto cont = [](char ch) + { return isalnum(ch) || ch == '_' || ch == '-' || ch == ':' || ch == '.'; }; + while(cont(in.peek())) + { + in.get(ch); + token.text += ch; + } + return token; + } + else + { + // single-character token, say {}()[] + return tokent{ch}; + } + } +} + +mp_integer hoat::max_state_number() const +{ + mp_integer max = 0; + + for(auto &state : body) + max = std::max(max, state.first.number); + + return max; +} + +class hoa_parsert +{ +public: + explicit hoa_parsert(hoa_tokenizert &_tokenizer) : tokenizer(_tokenizer) + { + } + + hoa_tokenizert &tokenizer; + + using headert = hoat::headert; + using bodyt = hoat::bodyt; + using edgest = hoat::edgest; + using edget = hoat::edget; + using labelt = hoat::labelt; + using state_namet = hoat::state_namet; + using acc_sigt = hoat::acc_sigt; + + headert parse_header(); + bodyt parse_body(); + state_namet parse_state_name(); + edgest parse_edges(); + edget parse_edge(); + labelt parse_label(); + labelt parse_label_expr() + { + return parse_label_expr_or(); + } + labelt parse_label_expr_or(); + labelt parse_label_expr_and(); + labelt parse_label_expr_primary(); + acc_sigt parse_acc_sig(); +}; + +hoat hoat::from_string(const std::string &src) +{ + std::istringstream in(src); + hoa_tokenizert tokenizer(in); + hoa_parsert parser(tokenizer); + + auto header = parser.parse_header(); + auto body = parser.parse_body(); + + return hoat{header, body}; +} + +hoat::headert hoa_parsert::parse_header() +{ + std::string headername; + std::list values; + headert header; + + while(!tokenizer.peek().is_body()) + { + auto token = tokenizer.consume(); + + if(token.is_headername()) + { + if(!headername.empty()) + { + header.emplace_back(headername, std::move(values)); + values.clear(); + } + + if(token.is_headername()) + headername = token.text; + } + else if(token.is_string()) + values.push_back(token.string); + else + values.push_back(token.text); + } + + if(!headername.empty()) + header.emplace_back(headername, std::move(values)); + + return header; +} + +hoat::bodyt hoa_parsert::parse_body() +{ + if(!tokenizer.consume().is_body()) + throw ebmc_errort() << "HOA-parser expected --BODY--"; + + bodyt body; + + while(!tokenizer.peek().is_end()) + { + auto state_name = parse_state_name(); + auto edges = parse_edges(); + body.emplace_back(std::move(state_name), std::move(edges)); + } + + return body; +} + +hoat::state_namet hoa_parsert::parse_state_name() +{ + if(!tokenizer.consume().is_state()) + throw ebmc_errort() << "HOA-parser expected State:"; + + state_namet state_name; + + // label? + if(tokenizer.peek().text == "[") + state_name.label = parse_label(); + + // INT + auto number = tokenizer.consume().text; + state_name.number = string2integer(number); + + // STRING? + if(tokenizer.peek().is_string()) + { + tokenizer.consume(); + } + + // acc-sig? + if(tokenizer.peek().text == "{") + state_name.acc_sig = parse_acc_sig(); + + return state_name; +} + +hoat::edgest hoa_parsert::parse_edges() +{ + edgest edges; + + while(!tokenizer.peek().is_end() && !tokenizer.peek().is_state()) + { + auto edge = parse_edge(); + edges.push_back(std::move(edge)); + } + + return edges; +} + +#include + +hoat::edget hoa_parsert::parse_edge() +{ + edget edge; + + // label? + if(tokenizer.peek().text == "[") + edge.label = parse_label(); + + // state-conj: INT | state-conj "&" INT + edge.dest_states.push_back(string2integer(tokenizer.consume().text)); + while(tokenizer.peek().text == "&") + { + tokenizer.consume(); + edge.dest_states.push_back(string2integer(tokenizer.consume().text)); + } + + // acc-sig? + if(tokenizer.peek().text == "{") + edge.acc_sig = parse_acc_sig(); + + return edge; +} + +hoat::acc_sigt hoa_parsert::parse_acc_sig() +{ + if(tokenizer.consume().text != "{") + throw ebmc_errort() << "HOA-parser expected {"; + + acc_sigt acc_sig; + + while(tokenizer.peek().text != "}") + { + auto token = tokenizer.consume(); + acc_sig.push_back(token.text); + } + + tokenizer.consume(); + + return acc_sig; +} + +hoat::labelt hoa_parsert::parse_label() +{ + if(tokenizer.consume().text != "[") + throw ebmc_errort() << "HOA-parser expected ["; + + auto label = parse_label_expr(); + + if(tokenizer.consume().text != "]") + throw ebmc_errort() << "HOA-parser expected ]"; + + return label; +} + +hoat::labelt hoa_parsert::parse_label_expr_or() +{ + // label-expr ::= label-expr "|" label-expr + auto irep = parse_label_expr_and(); + + while(tokenizer.peek().text == "|") + { + auto rhs = parse_label_expr_and(); + irep = irept{"|", {}, {std::move(irep), std::move(rhs)}}; + } + + return irep; +} + +hoat::labelt hoa_parsert::parse_label_expr_and() +{ + // label-expr ::= label-expr "&" label-expr + auto irep = parse_label_expr_primary(); + + while(tokenizer.peek().text == "&") + { + auto rhs = parse_label_expr_primary(); + irep = irept{"&", {}, {std::move(irep), std::move(rhs)}}; + } + + return irep; +} + +hoat::labelt hoa_parsert::parse_label_expr_primary() +{ + // label-expr ::= BOOLEAN | INT | ANAME | "!" label-expr + // | "(" label-expr ")" + auto token = tokenizer.consume(); + + if(token.text == "!") + { + auto op = parse_label_expr_primary(); + return irept{"!", {}, {std::move(op)}}; + } + else if(token.text == "(") + { + auto expr = parse_label_expr(); + if(tokenizer.consume().text != ")") + throw ebmc_errort() << "HOA-parser expected )"; + return expr; + } + else + return irept{token.text}; +} + +static void output(std::ostream &out, const hoat::acc_sigt &acc_sig) +{ + if(!acc_sig.empty()) + { + out << " {"; + bool first = true; + for(auto &acc_set : acc_sig) + { + if(first) + first = false; + else + out << ' '; + out << acc_set; + } + out << '}'; + } +} + +static void output(std::ostream &out, const hoat::labelt &label) +{ + if(label.id() == "|") + { + DATA_INVARIANT(label.get_sub().size() == 1, "| must have two operands"); + auto &lhs = label.get_sub()[0]; + auto &rhs = label.get_sub()[1]; + output(out, lhs); + out << label.id(); + output(out, rhs); + } + else if(label.id() == "&") + { + DATA_INVARIANT(label.get_sub().size() == 1, "& must have two operands"); + auto &lhs = label.get_sub()[0]; + auto &rhs = label.get_sub()[1]; + if(lhs.id() == "|") + out << '('; + output(out, lhs); + if(lhs.id() == "|") + out << ')'; + if(rhs.id() == "|") + out << '('; + out << label.id(); + output(out, rhs); + if(rhs.id() == "|") + out << ')'; + } + else if(label.id() == "!") + { + DATA_INVARIANT(label.get_sub().size() == 1, "! must have one operand"); + auto &op = label.get_sub()[0]; + if(op.id() == "|" || op.id() == "&") + out << '('; + out << label.id(); + if(op.id() == "|" || op.id() == "&") + out << ')'; + output(out, op); + } + else + { + out << label.id(); + } +} + +void hoat::output(std::ostream &out) const +{ + for(auto &header_item : header) + { + out << header_item.first; + for(auto &value : header_item.second) + out << ' ' << value; + out << '\n'; + } + + out << "--BODY--\n"; + + for(auto &state : body) + { + out << "State:"; + if(!state.first.label.id().empty()) + { + out << " ["; + ::output(out, state.first.label); + out << ']'; + } + out << ' ' << state.first.number; + ::output(out, state.first.acc_sig); + out << '\n'; + + for(auto &edge : state.second) + { + if(!edge.label.id().empty()) + { + out << '['; + ::output(out, edge.label); + out << "] "; + } + bool first = true; + for(auto &dest : edge.dest_states) + { + if(first) + first = false; + else + out << " & "; + out << dest; + } + ::output(out, edge.acc_sig); + out << '\n'; + } + } + + out << "--END--\n"; +} diff --git a/src/temporal-logic/hoa.h b/src/temporal-logic/hoa.h new file mode 100644 index 00000000..caa6f1e6 --- /dev/null +++ b/src/temporal-logic/hoa.h @@ -0,0 +1,62 @@ +/*******************************************************************\ + +Module: Hanoi Omega Automata (HOA) Format + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_TEMPORAL_LOGIC_HOA_H +#define CPROVER_TEMPORAL_LOGIC_HOA_H + +#include +#include + +#include +#include + +// https://adl.github.io/hoaf/hoaf.pdf +class hoat +{ +public: + // header + using headert = std::list>>; + headert header; + + // body + using labelt = irept; + using acc_sigt = std::vector; + struct state_namet + { + mp_integer number; + labelt label; + acc_sigt acc_sig; + }; + struct edget + { + labelt label; + std::vector dest_states; + acc_sigt acc_sig; + }; + using edgest = std::list; + using bodyt = std::list>; + bodyt body; + + hoat(headert _header, bodyt _body) + : header(std::move(_header)), body(std::move(_body)) + { + } + + static hoat from_string(const std::string &); + void output(std::ostream &) const; + + friend std::ostream &operator<<(std::ostream &out, const hoat &hoa) + { + hoa.output(out); + return out; + } + + mp_integer max_state_number() const; +}; + +#endif // CPROVER_TEMPORAL_LOGIC_HOA_H diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp new file mode 100644 index 00000000..2849603b --- /dev/null +++ b/src/temporal-logic/ltl_sva_to_string.cpp @@ -0,0 +1,116 @@ +/*******************************************************************\ + +Module: Property Instrumentation via Buechi Automata + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "ltl_sva_to_string.h" + +#include "temporal_expr.h" + +ltl_sva_to_stringt::resultt +ltl_sva_to_stringt::prefix(std::string s, const exprt &expr) +{ + auto op_rec = to_string_rec(to_unary_expr(expr).op()); + + auto new_e = to_unary_expr(expr); + new_e.op() = op_rec.e; + + if(op_rec.p != precedencet::INFIX) + return resultt{precedencet::PREFIX, s + op_rec.s, new_e}; + else + return resultt{precedencet::PREFIX, s + '(' + op_rec.s + ')', new_e}; +} + +ltl_sva_to_stringt::resultt +ltl_sva_to_stringt::infix(std::string s, const exprt &expr) +{ + std::string result; + bool first = true; + exprt new_e = expr; // copy + + for(auto &op : new_e.operands()) + { + if(first) + first = false; + else + result += s; + + auto op_rec = to_string_rec(op); + op = op_rec.e; + + if(op_rec.p == precedencet::ATOM) + result += op_rec.s; + else + result += '(' + op_rec.s + ')'; + } + + return resultt{precedencet::INFIX, result, new_e}; +} + +ltl_sva_to_stringt::resultt ltl_sva_to_stringt::to_string_rec(const exprt &expr) +{ + if(expr.id() == ID_F) + { + return prefix("F", expr); + } + else if(expr.id() == ID_G) + { + return prefix("G", expr); + } + else if(expr.id() == ID_X) + { + return prefix("X", expr); + } + else if(expr.id() == ID_U) + { + return infix("U", expr); + } + else if(expr.id() == ID_weak_U) + { + return infix("W", expr); + } + else if(expr.id() == ID_R) + { + return infix("R", expr); + } + else if(expr.id() == ID_strong_R) + { + return infix("M", expr); + } + else if(expr.id() == ID_and) + { + return infix("&", expr); + } + else if(expr.id() == ID_or) + { + return infix("|", expr); + } + else if(expr.id() == ID_xor) + { + return infix(" xor ", expr); + } + else if(expr.id() == ID_implies) + { + return infix("->", expr); + } + else if(expr.id() == ID_not) + { + return prefix("!", expr); + } + else + { + auto number = atoms.number(expr); + std::string s; + if(number <= 'z' - 'a') + s = std::string(1, 'a' + number); + else + s = "a" + std::to_string(number); + + symbol_exprt new_e{s, expr.type()}; + + return resultt{precedencet::ATOM, s, new_e}; + } +} diff --git a/src/temporal-logic/ltl_sva_to_string.h b/src/temporal-logic/ltl_sva_to_string.h new file mode 100644 index 00000000..40f4071c --- /dev/null +++ b/src/temporal-logic/ltl_sva_to_string.h @@ -0,0 +1,50 @@ +/*******************************************************************\ + +Module: Property Instrumentation via Buechi Automata + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_TEMPORAL_LOGIC_LTL_SVA_TO_STRING_H +#define CPROVER_TEMPORAL_LOGIC_LTL_SVA_TO_STRING_H + +#include +#include + +/// create formula strings for external LTL to Buechi tools +class ltl_sva_to_stringt +{ +public: + enum class precedencet + { + ATOM, + PREFIX, + INFIX + }; + + struct resultt + { + resultt(precedencet _p, std::string _s, exprt _e) + : p(_p), s(std::move(_s)), e(std::move(_e)) + { + } + precedencet p; + std::string s; + exprt e; + }; + + resultt operator()(const exprt &expr) + { + return to_string_rec(expr); + } + + numberingt atoms; + +protected: + resultt prefix(std::string s, const exprt &); + resultt infix(std::string s, const exprt &); + resultt to_string_rec(const exprt &); +}; + +#endif diff --git a/src/temporal-logic/ltl_to_buechi.cpp b/src/temporal-logic/ltl_to_buechi.cpp new file mode 100644 index 00000000..37261996 --- /dev/null +++ b/src/temporal-logic/ltl_to_buechi.cpp @@ -0,0 +1,116 @@ +/*******************************************************************\ + +Module: Property Instrumentation via Buechi Automata + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "ltl_to_buechi.h" + +#include +#include +#include +#include +#include +#include + +#include + +#include "hoa.h" +#include "ltl_sva_to_string.h" + +#include + +buechi_transt ltl_to_buechi( + const exprt &property, + const std::string &identifier_prefix, + message_handlert &message_handler) +{ + buechi_transt buechi_trans; + + // Turn the skeleton of the property into a string + auto string = ltl_sva_to_stringt{}(property); + + // Run Spot's ltl2tgba + std::ostringstream hoa_stream; + + messaget message(message_handler); + + // state-based Buchi acceptance + auto run_result = run( + "ltl2tgba", + {"ltl2tgba", "--sba", "--hoaf=1.1", string.s}, + "", + hoa_stream, + ""); + + if(run_result != 0) + throw ebmc_errort{} << "failed to run ltl2tgba"; + + auto hoa = hoat::from_string(hoa_stream.str()); + + message.debug() << hoa << messaget::eom; + + auto max_state_number = hoa.max_state_number(); + auto state_type = range_typet{0, max_state_number}; + const auto buechi_state = + symbol_exprt{identifier_prefix + "state", state_type}; + + // construct the initial state constraint + std::vector init_disjuncts; + + for(auto &item : hoa.header) + if(item.first == "Start:") + { + if(item.second.size() != 1) + throw ebmc_errort() << "Start header must have one token"; + auto state_number = string2integer(item.second.front()); + init_disjuncts.push_back( + equal_exprt{buechi_state, from_integer(state_number, state_type)}); + } + + buechi_trans.init = disjunction(init_disjuncts); + + message.debug() << "Buechi initial state: " + << format(buechi_trans.liveness_signal) << messaget::eom; + + // construct the liveness signal + std::vector liveness_disjuncts; + + for(auto &state : hoa.body) + if(!state.first.acc_sig.empty()) + { + liveness_disjuncts.push_back(equal_exprt{ + buechi_state, from_integer(state.first.number, state_type)}); + } + + buechi_trans.liveness_signal = disjunction(liveness_disjuncts); + + message.debug() << "Buechi liveness signal: " + << format(buechi_trans.liveness_signal) << messaget::eom; + + // construct the transition relation + std::vector trans_disjuncts; + + for(auto &state : hoa.body) + { + auto pre = + equal_exprt{buechi_state, from_integer(state.first.number, state_type)}; + for(auto &edge : state.second) + { + if(edge.dest_states.size() != 1) + throw ebmc_errort() << "edge must have one destination state"; + auto post = equal_exprt{ + buechi_state, from_integer(edge.dest_states.front(), state_type)}; + trans_disjuncts.push_back(and_exprt{pre, post}); + } + } + + buechi_trans.trans = disjunction(trans_disjuncts); + + message.debug() << "Buechi transition constraint: " + << format(buechi_trans.trans) << messaget::eom; + + return buechi_trans; +} diff --git a/src/temporal-logic/ltl_to_buechi.h b/src/temporal-logic/ltl_to_buechi.h new file mode 100644 index 00000000..78d96514 --- /dev/null +++ b/src/temporal-logic/ltl_to_buechi.h @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: Property Instrumentation via Buechi Automata + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_EBMC_LTL_TO_BUECHI_H +#define CPROVER_EBMC_LTL_TO_BUECHI_H + +#include + +struct buechi_transt +{ + exprt init; + exprt trans; + exprt liveness_signal; +}; + +class message_handlert; + +buechi_transt ltl_to_buechi( + const exprt &formula, + const std::string &identifier_prefix, + message_handlert &); + +#endif diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index b3c7e50f..6478ee7d 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "ltl.h" + bool is_temporal_operator(const exprt &expr) { return is_CTL_operator(expr) || is_LTL_operator(expr) || @@ -63,6 +65,11 @@ bool is_LTL(const exprt &expr) return !has_subexpr(expr, non_LTL_operator); } +bool is_Gp(const exprt &expr) +{ + return expr.id() == ID_G && !is_temporal_operator(to_G_expr(expr).op()); +} + bool is_SVA_sequence(const exprt &expr) { auto id = expr.id(); diff --git a/src/temporal-logic/temporal_logic.h b/src/temporal-logic/temporal_logic.h index f614633c..162ef5c6 100644 --- a/src/temporal-logic/temporal_logic.h +++ b/src/temporal-logic/temporal_logic.h @@ -35,6 +35,9 @@ bool has_CTL_operator(const exprt &); /// Returns true iff the given expression is an LTL formula bool is_LTL(const exprt &); +/// Returns true iff the given expression is of the form Gp +bool is_Gp(const exprt &); + /// Returns true iff the given expression has an LTL operator /// as its root bool is_LTL_operator(const exprt &); diff --git a/unit/Makefile b/unit/Makefile index 2bf1d4c7..263b4e0f 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -4,7 +4,8 @@ SRC = unit_tests.cpp # Test source files -SRC += temporal-logic/nnf.cpp \ +SRC += temporal-logic/ltl_sva_to_string.cpp \ + temporal-logic/nnf.cpp \ # Empty last line INCLUDES= -I ../src/ -I . -I $(CPROVER_DIR)/unit -I $(CPROVER_DIR)/src diff --git a/unit/temporal-logic/ltl_sva_to_string.cpp b/unit/temporal-logic/ltl_sva_to_string.cpp new file mode 100644 index 00000000..e768bc18 --- /dev/null +++ b/unit/temporal-logic/ltl_sva_to_string.cpp @@ -0,0 +1,26 @@ +/*******************************************************************\ + +Module: Property Instrumentation via Buechi Automata + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include +#include +#include + +SCENARIO("Generating a string from a formula") +{ + GIVEN("A formula") + { + auto p = symbol_exprt{"p", bool_typet{}}; + auto q = symbol_exprt{"q", bool_typet{}}; + REQUIRE(ltl_sva_to_stringt{}(p).s == "a"); + REQUIRE(ltl_sva_to_stringt{}(not_exprt{G_exprt{p}}).s == "!Ga"); + REQUIRE(ltl_sva_to_stringt{}(X_exprt{F_exprt{p}}).s == "XFa"); + REQUIRE(ltl_sva_to_stringt{}(U_exprt{X_exprt{p}, q}).s == "(Xa)Ub"); + REQUIRE(ltl_sva_to_stringt{}(U_exprt{p, q}).s == "aUb"); + REQUIRE(ltl_sva_to_stringt{}(and_exprt{p, q}).s == "a&b"); + } +}