From b3f4646aa94713b8c8800f1812516c69919d0f28 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 2 May 2025 19:35:04 -0700 Subject: [PATCH] extract SVA_to_LTL(exprt) into a separate file --- src/temporal-logic/Makefile | 1 + src/temporal-logic/sva_to_ltl.cpp | 359 ++++++++++++++++++++++++++ src/temporal-logic/temporal_logic.cpp | 345 ------------------------- 3 files changed, 360 insertions(+), 345 deletions(-) create mode 100644 src/temporal-logic/sva_to_ltl.cpp diff --git a/src/temporal-logic/Makefile b/src/temporal-logic/Makefile index 119b3b472..3a58d5b48 100644 --- a/src/temporal-logic/Makefile +++ b/src/temporal-logic/Makefile @@ -2,6 +2,7 @@ SRC = ctl.cpp \ ltl.cpp \ nnf.cpp \ normalize_property.cpp \ + sva_to_ltl.cpp \ temporal_logic.cpp \ trivial_sva.cpp \ #empty line diff --git a/src/temporal-logic/sva_to_ltl.cpp b/src/temporal-logic/sva_to_ltl.cpp new file mode 100644 index 000000000..9b993e40c --- /dev/null +++ b/src/temporal-logic/sva_to_ltl.cpp @@ -0,0 +1,359 @@ +/*******************************************************************\ + +Module: SVA to LTL + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include + +#include + +#include "ltl.h" +#include "temporal_logic.h" + +static exprt n_Xes(mp_integer n, exprt op) +{ + PRECONDITION(n >= 0); + if(n == 0) + return op; + else + return n_Xes(n - 1, X_exprt{std::move(op)}); +} + +// Returns a set of match conditions (given as LTL formula) +struct ltl_sequence_matcht +{ + ltl_sequence_matcht(exprt __cond, mp_integer __length) + : cond(std::move(__cond)), length(std::move(__length)) + { + PRECONDITION(length >= 0); + } + + exprt cond; // LTL + mp_integer length; // match_end - match_start + 1 + + bool empty() const + { + return length == 0; + } +}; + +std::vector LTL_sequence_matches(const exprt &sequence) +{ + if(!is_SVA_sequence_operator(sequence)) + { + // atomic proposition + return {{sequence, 1}}; + } + else if(sequence.id() == ID_sva_sequence_concatenation) + { + auto &concatenation = to_sva_sequence_concatenation_expr(sequence); + auto matches_lhs = LTL_sequence_matches(concatenation.lhs()); + auto matches_rhs = LTL_sequence_matches(concatenation.rhs()); + + if(matches_lhs.empty() || matches_rhs.empty()) + return {}; + + std::vector result; + // cross product + for(auto &match_lhs : matches_lhs) + for(auto &match_rhs : matches_rhs) + { + // Concatenation is overlapping, hence deduct one from + // the length. + auto delay = match_lhs.length - 1; + auto rhs_delayed = n_Xes(delay, match_rhs.cond); + result.emplace_back( + and_exprt{match_lhs.cond, rhs_delayed}, + match_lhs.length + match_rhs.length - 1); + } + return result; + } + else if(sequence.id() == ID_sva_cycle_delay) + { + auto &delay = to_sva_cycle_delay_expr(sequence); + auto matches = LTL_sequence_matches(delay.op()); + auto from_int = numeric_cast_v(delay.from()); + + if(matches.empty()) + return {}; + + if(delay.to().is_nil()) + { + for(auto &match : matches) + { + // delay as instructed + match.length += from_int; + match.cond = n_Xes(from_int, match.cond); + } + return matches; + } + else if(delay.to().id() == ID_infinity) + { + return {}; // can't encode + } + else if(delay.to().is_constant()) + { + auto to_int = numeric_cast_v(to_constant_expr(delay.to())); + std::vector new_matches; + + for(mp_integer i = from_int; i <= to_int; ++i) + { + for(const auto &match : matches) + { + // delay as instructed + auto new_match = match; + new_match.length += from_int; + new_match.cond = n_Xes(i, match.cond); + new_matches.push_back(std::move(new_match)); + } + } + + return new_matches; + } + else + return {}; + } + else + { + return {}; // unsupported + } +} + +/// takes an SVA property as input, and returns an equivalent LTL property, +/// or otherwise {}. +std::optional SVA_to_LTL(exprt expr) +{ + // Some SVA is directly mappable to LTL + if(expr.id() == ID_sva_always) + { + auto rec = SVA_to_LTL(to_sva_always_expr(expr).op()); + if(rec.has_value()) + return G_exprt{rec.value()}; + else + return {}; + } + else if(expr.id() == ID_sva_ranged_always) + { + auto &ranged_always = to_sva_ranged_always_expr(expr); + auto rec = SVA_to_LTL(ranged_always.op()); + if(rec.has_value()) + { + // always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op) + auto lower_int = numeric_cast_v(ranged_always.lower()); + + // Is there an upper end of the range? + if(ranged_always.upper().is_constant()) + { + // upper end set + auto upper_int = + numeric_cast_v(to_constant_expr(ranged_always.upper())); + PRECONDITION(upper_int >= lower_int); + auto diff = upper_int - lower_int; + + exprt::operandst conjuncts; + + for(auto i = 0; i <= diff; i++) + conjuncts.push_back(n_Xes(i, rec.value())); + + return n_Xes(lower_int, conjunction(conjuncts)); + } + else if(ranged_always.upper().id() == ID_infinity) + { + // always [l:$] op ---> X ... X G op + return n_Xes(lower_int, G_exprt{rec.value()}); + } + else + PRECONDITION(false); + } + else + return {}; + } + else if(expr.id() == ID_sva_s_always) + { + auto &ranged_always = to_sva_s_always_expr(expr); + auto rec = SVA_to_LTL(ranged_always.op()); + if(rec.has_value()) + { + // s_always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op) + auto lower_int = numeric_cast_v(ranged_always.lower()); + auto upper_int = numeric_cast_v(ranged_always.upper()); + PRECONDITION(upper_int >= lower_int); + auto diff = upper_int - lower_int; + + exprt::operandst conjuncts; + + for(auto i = 0; i <= diff; i++) + conjuncts.push_back(n_Xes(i, rec.value())); + + return n_Xes(lower_int, conjunction(conjuncts)); + } + else + return {}; + } + else if(expr.id() == ID_sva_s_eventually) + { + auto rec = SVA_to_LTL(to_sva_s_eventually_expr(expr).op()); + if(rec.has_value()) + return F_exprt{rec.value()}; + else + return {}; + } + else if(expr.id() == ID_sva_s_nexttime) + { + auto rec = SVA_to_LTL(to_sva_s_nexttime_expr(expr).op()); + if(rec.has_value()) + return X_exprt{rec.value()}; + else + return {}; + } + else if(expr.id() == ID_sva_nexttime) + { + auto rec = SVA_to_LTL(to_sva_nexttime_expr(expr).op()); + if(rec.has_value()) + return X_exprt{rec.value()}; + else + return {}; + } + else if( + expr.id() == ID_sva_overlapped_implication || + expr.id() == ID_sva_non_overlapped_implication) + { + auto &implication = to_sva_implication_base_expr(expr); + auto matches = LTL_sequence_matches(implication.sequence()); + + if(matches.empty()) + return {}; + + // All matches must be followed + // by the property being true + exprt::operandst conjuncts; + + auto property_rec = SVA_to_LTL(implication.property()); + + if(!property_rec.has_value()) + return {}; + + for(auto &match : matches) + { + const auto overlapped = expr.id() == ID_sva_overlapped_implication; + if(match.empty() && overlapped) + { + // ignore the empty match + } + else + { + auto delay = match.length + (overlapped ? 0 : 1) - 1; + auto delayed_property = n_Xes(delay, property_rec.value()); + conjuncts.push_back(implies_exprt{match.cond, delayed_property}); + } + } + + return conjunction(conjuncts); + } + else if( + expr.id() == ID_sva_nonoverlapped_followed_by || + expr.id() == ID_sva_overlapped_followed_by) + { + auto &followed_by = to_sva_followed_by_expr(expr); + auto matches = LTL_sequence_matches(followed_by.sequence()); + + if(matches.empty()) + return {}; + + // There must be at least one match that is followed + // by the property being true + exprt::operandst disjuncts; + + auto property_rec = SVA_to_LTL(followed_by.property()); + + if(!property_rec.has_value()) + return {}; + + for(auto &match : matches) + { + const auto overlapped = expr.id() == ID_sva_overlapped_followed_by; + if(match.empty() && overlapped) + { + // ignore the empty match + } + else + { + auto delay = match.length + (overlapped ? 0 : 1) - 1; + auto delayed_property = n_Xes(delay, property_rec.value()); + disjuncts.push_back(and_exprt{match.cond, delayed_property}); + } + } + + return disjunction(disjuncts); + } + else if(expr.id() == ID_sva_sequence_property) + { + // should have been turned into sva_implicit_weak or sva_implicit_strong + PRECONDITION(false); + } + else if( + expr.id() == ID_sva_weak || expr.id() == ID_sva_strong || + expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong) + { + auto &sequence = to_sva_sequence_property_expr_base(expr).sequence(); + + // evaluates to true if there's at least one non-empty match of the sequence + auto matches = LTL_sequence_matches(sequence); + + if(matches.empty()) + return {}; + + exprt::operandst disjuncts; + + for(auto &match : matches) + { + if(!match.empty()) + disjuncts.push_back(match.cond); + } + + return disjunction(disjuncts); + } + else if(expr.id() == ID_sva_s_until) + { + auto &until = to_sva_s_until_expr(expr); + auto rec_lhs = SVA_to_LTL(until.lhs()); + auto rec_rhs = SVA_to_LTL(until.rhs()); + if(rec_lhs.has_value() && rec_rhs.has_value()) + return U_exprt{rec_lhs.value(), rec_rhs.value()}; + else + return {}; + } + else if(expr.id() == ID_sva_s_until_with) + { + // This is release with swapped operands + auto &until_with = to_sva_s_until_with_expr(expr); + auto rec_lhs = SVA_to_LTL(until_with.lhs()); + auto rec_rhs = SVA_to_LTL(until_with.rhs()); + if(rec_lhs.has_value() && rec_rhs.has_value()) + return R_exprt{rec_rhs.value(), rec_lhs.value()}; // swapped + else + return {}; + } + else if(!has_temporal_operator(expr)) + { + return expr; + } + else if( + expr.id() == ID_and || expr.id() == ID_implies || expr.id() == ID_or || + expr.id() == ID_not) + { + for(auto &op : expr.operands()) + { + auto rec = SVA_to_LTL(op); + if(!rec.has_value()) + return {}; + op = rec.value(); + } + return expr; + } + else + return {}; +} diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index 2c889fb8e..614c642d8 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -214,348 +214,3 @@ std::optional LTL_to_CTL(exprt expr) else return {}; } - -static exprt n_Xes(mp_integer n, exprt op) -{ - PRECONDITION(n >= 0); - if(n == 0) - return op; - else - return n_Xes(n - 1, X_exprt{std::move(op)}); -} - -// Returns a set of match conditions (given as LTL formula) -struct ltl_sequence_matcht -{ - ltl_sequence_matcht(exprt __cond, mp_integer __length) - : cond(std::move(__cond)), length(std::move(__length)) - { - PRECONDITION(length >= 0); - } - - exprt cond; // LTL - mp_integer length; // match_end - match_start + 1 - - bool empty() const - { - return length == 0; - } -}; - -std::vector LTL_sequence_matches(const exprt &sequence) -{ - if(!is_SVA_sequence_operator(sequence)) - { - // atomic proposition - return {{sequence, 1}}; - } - else if(sequence.id() == ID_sva_sequence_concatenation) - { - auto &concatenation = to_sva_sequence_concatenation_expr(sequence); - auto matches_lhs = LTL_sequence_matches(concatenation.lhs()); - auto matches_rhs = LTL_sequence_matches(concatenation.rhs()); - - if(matches_lhs.empty() || matches_rhs.empty()) - return {}; - - std::vector result; - // cross product - for(auto &match_lhs : matches_lhs) - for(auto &match_rhs : matches_rhs) - { - // Concatenation is overlapping, hence deduct one from - // the length. - auto delay = match_lhs.length - 1; - auto rhs_delayed = n_Xes(delay, match_rhs.cond); - result.emplace_back( - and_exprt{match_lhs.cond, rhs_delayed}, - match_lhs.length + match_rhs.length - 1); - } - return result; - } - else if(sequence.id() == ID_sva_cycle_delay) - { - auto &delay = to_sva_cycle_delay_expr(sequence); - auto matches = LTL_sequence_matches(delay.op()); - auto from_int = numeric_cast_v(delay.from()); - - if(matches.empty()) - return {}; - - if(delay.to().is_nil()) - { - for(auto &match : matches) - { - // delay as instructed - match.length += from_int; - match.cond = n_Xes(from_int, match.cond); - } - return matches; - } - else if(delay.to().id() == ID_infinity) - { - return {}; // can't encode - } - else if(delay.to().is_constant()) - { - auto to_int = numeric_cast_v(to_constant_expr(delay.to())); - std::vector new_matches; - - for(mp_integer i = from_int; i <= to_int; ++i) - { - for(const auto &match : matches) - { - // delay as instructed - auto new_match = match; - new_match.length += from_int; - new_match.cond = n_Xes(i, match.cond); - new_matches.push_back(std::move(new_match)); - } - } - - return new_matches; - } - else - return {}; - } - else - { - return {}; // unsupported - } -} - -/// takes an SVA property as input, and returns an equivalent LTL property, -/// or otherwise {}. -std::optional SVA_to_LTL(exprt expr) -{ - // Some SVA is directly mappable to LTL - if(expr.id() == ID_sva_always) - { - auto rec = SVA_to_LTL(to_sva_always_expr(expr).op()); - if(rec.has_value()) - return G_exprt{rec.value()}; - else - return {}; - } - else if(expr.id() == ID_sva_ranged_always) - { - auto &ranged_always = to_sva_ranged_always_expr(expr); - auto rec = SVA_to_LTL(ranged_always.op()); - if(rec.has_value()) - { - // always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op) - auto lower_int = numeric_cast_v(ranged_always.lower()); - - // Is there an upper end of the range? - if(ranged_always.upper().is_constant()) - { - // upper end set - auto upper_int = - numeric_cast_v(to_constant_expr(ranged_always.upper())); - PRECONDITION(upper_int >= lower_int); - auto diff = upper_int - lower_int; - - exprt::operandst conjuncts; - - for(auto i = 0; i <= diff; i++) - conjuncts.push_back(n_Xes(i, rec.value())); - - return n_Xes(lower_int, conjunction(conjuncts)); - } - else if(ranged_always.upper().id() == ID_infinity) - { - // always [l:$] op ---> X ... X G op - return n_Xes(lower_int, G_exprt{rec.value()}); - } - else - PRECONDITION(false); - } - else - return {}; - } - else if(expr.id() == ID_sva_s_always) - { - auto &ranged_always = to_sva_s_always_expr(expr); - auto rec = SVA_to_LTL(ranged_always.op()); - if(rec.has_value()) - { - // s_always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op) - auto lower_int = numeric_cast_v(ranged_always.lower()); - auto upper_int = numeric_cast_v(ranged_always.upper()); - PRECONDITION(upper_int >= lower_int); - auto diff = upper_int - lower_int; - - exprt::operandst conjuncts; - - for(auto i = 0; i <= diff; i++) - conjuncts.push_back(n_Xes(i, rec.value())); - - return n_Xes(lower_int, conjunction(conjuncts)); - } - else - return {}; - } - else if(expr.id() == ID_sva_s_eventually) - { - auto rec = SVA_to_LTL(to_sva_s_eventually_expr(expr).op()); - if(rec.has_value()) - return F_exprt{rec.value()}; - else - return {}; - } - else if(expr.id() == ID_sva_s_nexttime) - { - auto rec = SVA_to_LTL(to_sva_s_nexttime_expr(expr).op()); - if(rec.has_value()) - return X_exprt{rec.value()}; - else - return {}; - } - else if(expr.id() == ID_sva_nexttime) - { - auto rec = SVA_to_LTL(to_sva_nexttime_expr(expr).op()); - if(rec.has_value()) - return X_exprt{rec.value()}; - else - return {}; - } - else if( - expr.id() == ID_sva_overlapped_implication || - expr.id() == ID_sva_non_overlapped_implication) - { - auto &implication = to_sva_implication_base_expr(expr); - auto matches = LTL_sequence_matches(implication.sequence()); - - if(matches.empty()) - return {}; - - // All matches must be followed - // by the property being true - exprt::operandst conjuncts; - - auto property_rec = SVA_to_LTL(implication.property()); - - if(!property_rec.has_value()) - return {}; - - for(auto &match : matches) - { - const auto overlapped = expr.id() == ID_sva_overlapped_implication; - if(match.empty() && overlapped) - { - // ignore the empty match - } - else - { - auto delay = match.length + (overlapped ? 0 : 1) - 1; - auto delayed_property = n_Xes(delay, property_rec.value()); - conjuncts.push_back(implies_exprt{match.cond, delayed_property}); - } - } - - return conjunction(conjuncts); - } - else if( - expr.id() == ID_sva_nonoverlapped_followed_by || - expr.id() == ID_sva_overlapped_followed_by) - { - auto &followed_by = to_sva_followed_by_expr(expr); - auto matches = LTL_sequence_matches(followed_by.sequence()); - - if(matches.empty()) - return {}; - - // There must be at least one match that is followed - // by the property being true - exprt::operandst disjuncts; - - auto property_rec = SVA_to_LTL(followed_by.property()); - - if(!property_rec.has_value()) - return {}; - - for(auto &match : matches) - { - const auto overlapped = expr.id() == ID_sva_overlapped_followed_by; - if(match.empty() && overlapped) - { - // ignore the empty match - } - else - { - auto delay = match.length + (overlapped ? 0 : 1) - 1; - auto delayed_property = n_Xes(delay, property_rec.value()); - disjuncts.push_back(and_exprt{match.cond, delayed_property}); - } - } - - return disjunction(disjuncts); - } - else if(expr.id() == ID_sva_sequence_property) - { - // should have been turned into sva_implicit_weak or sva_implicit_strong - PRECONDITION(false); - } - else if( - expr.id() == ID_sva_weak || expr.id() == ID_sva_strong || - expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong) - { - auto &sequence = to_sva_sequence_property_expr_base(expr).sequence(); - - // evaluates to true if there's at least one non-empty match of the sequence - auto matches = LTL_sequence_matches(sequence); - - if(matches.empty()) - return {}; - - exprt::operandst disjuncts; - - for(auto &match : matches) - { - if(!match.empty()) - disjuncts.push_back(match.cond); - } - - return disjunction(disjuncts); - } - else if(expr.id() == ID_sva_s_until) - { - auto &until = to_sva_s_until_expr(expr); - auto rec_lhs = SVA_to_LTL(until.lhs()); - auto rec_rhs = SVA_to_LTL(until.rhs()); - if(rec_lhs.has_value() && rec_rhs.has_value()) - return U_exprt{rec_lhs.value(), rec_rhs.value()}; - else - return {}; - } - else if(expr.id() == ID_sva_s_until_with) - { - // This is release with swapped operands - auto &until_with = to_sva_s_until_with_expr(expr); - auto rec_lhs = SVA_to_LTL(until_with.lhs()); - auto rec_rhs = SVA_to_LTL(until_with.rhs()); - if(rec_lhs.has_value() && rec_rhs.has_value()) - return R_exprt{rec_rhs.value(), rec_lhs.value()}; // swapped - else - return {}; - } - else if(!has_temporal_operator(expr)) - { - return expr; - } - else if( - expr.id() == ID_and || expr.id() == ID_implies || expr.id() == ID_or || - expr.id() == ID_not) - { - for(auto &op : expr.operands()) - { - auto rec = SVA_to_LTL(op); - if(!rec.has_value()) - return {}; - op = rec.value(); - } - return expr; - } - else - return {}; -}