From 49923bb93052d0239e57789e11551f893f77250e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 17 Jun 2025 21:23:35 +0900 Subject: [PATCH] SVA: strengthen typing of sva_sequence_concatenation_exprt The RHS of a sva_sequence_concatenation_exprt is always a sva_cycle_delay expression. This strengthens the typing of the rhs() method accordingly. --- src/temporal-logic/ltl_sva_to_string.cpp | 76 +++++++++++------------- src/verilog/sva_expr.h | 71 +++++++++++++--------- 2 files changed, 77 insertions(+), 70 deletions(-) diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp index cad963a3..4a843473 100644 --- a/src/temporal-logic/ltl_sva_to_string.cpp +++ b/src/temporal-logic/ltl_sva_to_string.cpp @@ -337,56 +337,50 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) // f ##1 g --> f ; g // f ##n g --> f ; 1[*n-1] ; b auto &concatenation = to_sva_sequence_concatenation_expr(expr); - if(concatenation.rhs().id() == ID_sva_cycle_delay) - { - auto &delay = to_sva_cycle_delay_expr(concatenation.rhs()); + auto &delay = concatenation.rhs(); - auto new_expr = concatenation; - new_expr.rhs() = delay.op(); + binary_exprt new_expr = concatenation; + new_expr.rhs() = delay.op(); - if(delay.is_range()) - { - auto from = numeric_cast_v(delay.from()); + if(delay.is_range()) + { + auto from = numeric_cast_v(delay.from()); - if(from == 0) - { - // requires treatment of empty sequences on lhs - throw ebmc_errort{} - << "cannot convert 0.. ranged sequence concatenation to Buechi"; - } - else if(delay.is_unbounded()) - { - return infix( - " ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode); - } - else - { - auto to = numeric_cast_v(delay.to()); - PRECONDITION(to >= 0); - return infix( - " ; 1[*" + integer2string(from - 1) + ".." + - integer2string(to - 1) + "] ; ", - new_expr, - mode); - } + if(from == 0) + { + // requires treatment of empty sequences on lhs + throw ebmc_errort{} + << "cannot convert 0.. ranged sequence concatenation to Buechi"; + } + else if(delay.is_unbounded()) + { + return infix( + " ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode); } else { - auto n = numeric_cast_v(delay.from()); - PRECONDITION(n >= 0); - if(n == 0) - return infix(" : ", new_expr, mode); - else if(n == 1) - return infix(" ; ", new_expr, mode); - else - { - return infix( - " ; 1[*" + integer2string(n - 1) + "] ; ", new_expr, mode); - } + auto to = numeric_cast_v(delay.to()); + PRECONDITION(to >= 0); + return infix( + " ; 1[*" + integer2string(from - 1) + ".." + integer2string(to - 1) + + "] ; ", + new_expr, + mode); } } else - return infix(":", expr, mode); + { + auto n = numeric_cast_v(delay.from()); + PRECONDITION(n >= 0); + if(n == 0) + return infix(" : ", new_expr, mode); + else if(n == 1) + return infix(" ; ", new_expr, mode); + else + { + return infix(" ; 1[*" + integer2string(n - 1) + "] ; ", new_expr, mode); + } + } } else if(expr.id() == ID_sva_cycle_delay) { diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 43600534..2442bc1e 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -861,35 +861,6 @@ static inline sva_and_exprt &to_sva_and_expr(exprt &expr) return static_cast(expr); } -class sva_sequence_concatenation_exprt : public binary_exprt -{ -public: - explicit sva_sequence_concatenation_exprt(exprt op0, exprt op1) - : binary_exprt( - std::move(op0), - ID_sva_sequence_concatenation, - std::move(op1), - verilog_sva_sequence_typet{}) - { - } -}; - -static inline const sva_sequence_concatenation_exprt & -to_sva_sequence_concatenation_expr(const exprt &expr) -{ - PRECONDITION(expr.id() == ID_sva_sequence_concatenation); - sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT); - return static_cast(expr); -} - -static inline sva_sequence_concatenation_exprt & -to_sva_sequence_concatenation_expr(exprt &expr) -{ - PRECONDITION(expr.id() == ID_sva_sequence_concatenation); - sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT); - return static_cast(expr); -} - class sva_iff_exprt : public binary_predicate_exprt { public: @@ -1084,6 +1055,48 @@ static inline sva_cycle_delay_exprt &to_sva_cycle_delay_expr(exprt &expr) return static_cast(expr); } +class sva_sequence_concatenation_exprt : public binary_exprt +{ +public: + // The lhs is a sequence, the rhs is a sva_cycle_delay expression + explicit sva_sequence_concatenation_exprt( + exprt __lhs, + sva_cycle_delay_exprt __rhs) + : binary_exprt( + std::move(__lhs), + ID_sva_sequence_concatenation, + std::move(__rhs), + verilog_sva_sequence_typet{}) + { + } + + const sva_cycle_delay_exprt &rhs() const + { + return static_cast(binary_exprt::rhs()); + } + + sva_cycle_delay_exprt &rhs() + { + return static_cast(binary_exprt::rhs()); + } +}; + +static inline const sva_sequence_concatenation_exprt & +to_sva_sequence_concatenation_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_sequence_concatenation); + sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline sva_sequence_concatenation_exprt & +to_sva_sequence_concatenation_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_sequence_concatenation); + sva_sequence_concatenation_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + class sva_cycle_delay_plus_exprt : public unary_exprt { public: