From 0a8fc6a838ae95d1f7d5410e378765eb15ff2f0e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 13 Oct 2024 09:43:52 -0700 Subject: [PATCH] SVA: move rewrites for state-formula SVA into separate file Some of the SVA operators are not temporal operators, but state predicates only. This moves the rewrites for these operators into a separate file. --- src/temporal-logic/Makefile | 1 + src/temporal-logic/normalize_property.cpp | 112 ++++------------------ src/temporal-logic/normalize_property.h | 13 --- src/temporal-logic/trivial_sva.cpp | 94 ++++++++++++++++++ src/temporal-logic/trivial_sva.h | 32 +++++++ 5 files changed, 144 insertions(+), 108 deletions(-) create mode 100644 src/temporal-logic/trivial_sva.cpp create mode 100644 src/temporal-logic/trivial_sva.h diff --git a/src/temporal-logic/Makefile b/src/temporal-logic/Makefile index eb81d9f16..2cb1e0201 100644 --- a/src/temporal-logic/Makefile +++ b/src/temporal-logic/Makefile @@ -1,6 +1,7 @@ SRC = nnf.cpp \ normalize_property.cpp \ temporal_logic.cpp \ + trivial_sva.cpp \ #empty line include ../config.inc diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index 184304d18..237c91b22 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "temporal_expr.h" #include "temporal_logic.h" +#include "trivial_sva.h" exprt normalize_pre_not(not_exprt expr) { @@ -73,16 +74,6 @@ exprt normalize_pre_implies(implies_exprt expr) return or_exprt{not_exprt{expr.lhs()}, expr.rhs()}; } -exprt normalize_pre_sva_overlapped_implication( - sva_overlapped_implication_exprt expr) -{ - // Same as regular implication if lhs is not a sequence. - if(!is_SVA_sequence(expr.lhs())) - return or_exprt{not_exprt{expr.lhs()}, expr.rhs()}; - else - return std::move(expr); -} - exprt normalize_pre_sva_non_overlapped_implication( sva_non_overlapped_implication_exprt expr) { @@ -97,30 +88,6 @@ exprt normalize_pre_sva_non_overlapped_implication( return std::move(expr); } -exprt normalize_pre_sva_not(sva_not_exprt expr) -{ - // Same as regular 'not'. These do not apply to sequences. - return normalize_pre_not(not_exprt{expr.op()}); -} - -exprt normalize_pre_sva_and(sva_and_exprt expr) -{ - // Same as a ∧ b if lhs and rhs are not sequences. - if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs())) - return and_exprt{expr.lhs(), expr.rhs()}; - else - return std::move(expr); -} - -exprt normalize_pre_sva_or(sva_or_exprt expr) -{ - // Same as a ∧ b if lhs or rhs are not sequences. - if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs())) - return or_exprt{expr.lhs(), expr.rhs()}; - else - return std::move(expr); -} - exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr) { if(expr.is_unbounded()) @@ -143,37 +110,16 @@ exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr) return std::move(expr); } -exprt normalize_property(exprt expr) +exprt normalize_property_rec(exprt expr) { // pre-traversal if(expr.id() == ID_not) expr = normalize_pre_not(to_not_expr(expr)); else if(expr.id() == ID_implies) expr = normalize_pre_implies(to_implies_expr(expr)); - else if(expr.id() == ID_sva_cover) - expr = G_exprt{not_exprt{to_sva_cover_expr(expr).op()}}; - else if(expr.id() == ID_sva_overlapped_implication) - expr = normalize_pre_sva_overlapped_implication( - to_sva_overlapped_implication_expr(expr)); else if(expr.id() == ID_sva_non_overlapped_implication) expr = normalize_pre_sva_non_overlapped_implication( to_sva_non_overlapped_implication_expr(expr)); - else if(expr.id() == ID_sva_iff) - { - expr = - equal_exprt{to_sva_iff_expr(expr).lhs(), to_sva_iff_expr(expr).rhs()}; - } - else if(expr.id() == ID_sva_implies) - { - expr = implies_exprt{ - to_sva_implies_expr(expr).lhs(), to_sva_implies_expr(expr).rhs()}; - } - else if(expr.id() == ID_sva_and) - expr = normalize_pre_sva_and(to_sva_and_expr(expr)); - else if(expr.id() == ID_sva_not) - expr = normalize_pre_sva_not(to_sva_not_expr(expr)); - else if(expr.id() == ID_sva_or) - expr = normalize_pre_sva_or(to_sva_or_expr(expr)); else if(expr.id() == ID_sva_nexttime) { auto one = natural_typet{}.one_expr(); @@ -209,40 +155,6 @@ exprt normalize_property(exprt expr) { expr = sva_s_eventually_exprt{to_sva_cycle_delay_star_expr(expr).op()}; } - else if(expr.id() == ID_sva_sequence_concatenation) - { - auto &sequence_concatenation = to_sva_sequence_concatenation_expr(expr); - if(!is_SVA_sequence(sequence_concatenation.lhs())) - { - // a ##0 b --> a && b if a is not a sequence - expr = - and_exprt{sequence_concatenation.lhs(), sequence_concatenation.rhs()}; - } - } - else if(expr.id() == ID_sva_if) - { - auto &sva_if_expr = to_sva_if_expr(expr); - auto false_case = sva_if_expr.false_case().is_nil() - ? true_exprt{} - : sva_if_expr.false_case(); - expr = if_exprt{sva_if_expr.cond(), sva_if_expr.true_case(), false_case}; - } - else if(expr.id() == ID_sva_disable_iff) - { - auto &disable_iff_expr = to_sva_disable_iff_expr(expr); - expr = or_exprt{disable_iff_expr.lhs(), disable_iff_expr.rhs()}; - } - else if(expr.id() == ID_sva_accept_on || expr.id() == ID_sva_sync_accept_on) - { - auto &sva_abort_expr = to_sva_abort_expr(expr); - expr = or_exprt{sva_abort_expr.condition(), sva_abort_expr.property()}; - } - else if(expr.id() == ID_sva_reject_on || expr.id() == ID_sva_sync_reject_on) - { - auto &sva_abort_expr = to_sva_abort_expr(expr); - expr = and_exprt{ - not_exprt{sva_abort_expr.condition()}, sva_abort_expr.property()}; - } else if(expr.id() == ID_sva_strong) { expr = to_sva_strong_expr(expr).op(); @@ -251,16 +163,26 @@ exprt normalize_property(exprt expr) { expr = to_sva_weak_expr(expr).op(); } - else if(expr.id() == ID_sva_case) - { - expr = to_sva_case_expr(expr).lowering(); - } // normalize the operands for(auto &op : expr.operands()) - op = normalize_property(op); + op = normalize_property_rec(op); // recursive call // post-traversal return expr; } + +exprt normalize_property(exprt expr) +{ + // top-level only + if(expr.id() == ID_sva_cover) + expr = G_exprt{not_exprt{to_sva_cover_expr(expr).op()}}; + + expr = trivial_sva(expr); + + // now do recursion + expr = normalize_property_rec(expr); + + return expr; +} diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h index 02eda9ef4..bb9c20f70 100644 --- a/src/temporal-logic/normalize_property.h +++ b/src/temporal-logic/normalize_property.h @@ -21,30 +21,17 @@ Author: Daniel Kroening, dkr@amazon.com /// (a -> b) --> ¬a ∨ b /// /// -----SVA----- -/// a sva_iff b --> a <-> b -/// a sva_implies b --> a -> b -/// sva_not a --> ¬a -/// a sva_and b --> a ∧ b if a and b are not SVA sequences -/// a sva_or b --> a ∨ b if a and b are not SVA sequences -/// sva_overlapped_implication --> ¬a ∨ b if a is not an SVA sequence /// sva_non_overlapped_implication --> ¬a ∨ always[1:1] b if a is not an SVA sequence /// sva_nexttime φ --> sva_always[1:1] φ /// sva_nexttime[i] φ --> sva_always[i:i] φ /// sva_s_nexttime φ --> sva_always[1:1] φ /// sva_s_nexttime[i] φ --> sva_s_always[i:i] φ -/// sva_if --> ? : /// ##[0:$] φ --> s_eventually φ /// ##[i:$] φ --> s_nexttime[i] s_eventually φ /// ##[*] φ --> s_eventually φ /// ##[+] φ --> always[1:1] s_eventually φ /// strong(φ) --> φ /// weak(φ) --> φ -/// sva_case --> ? : -/// a sva_disable_iff b --> a ∨ b -/// a sva_accept_on b --> a ∨ b -/// a sva_reject_on b --> ¬a ∧ b -/// a sva_sync_accept_on b --> a ∨ b -/// a sva_sync_reject_on b --> ¬a ∧ b /// ¬ sva_s_eventually φ --> sva_always ¬φ /// ¬ sva_always φ --> sva_s_eventually ¬φ /// diff --git a/src/temporal-logic/trivial_sva.cpp b/src/temporal-logic/trivial_sva.cpp new file mode 100644 index 000000000..0864c87c3 --- /dev/null +++ b/src/temporal-logic/trivial_sva.cpp @@ -0,0 +1,94 @@ +/*******************************************************************\ + +Module: Trivial SVA + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "trivial_sva.h" + +#include + +#include "temporal_logic.h" + +exprt trivial_sva(exprt expr) +{ + // pre-traversal + if(expr.id() == ID_sva_overlapped_implication) + { + // Same as regular implication if lhs and rhs are not sequences. + auto &sva_implication = to_sva_overlapped_implication_expr(expr); + if( + !is_SVA_sequence(sva_implication.lhs()) && + !is_SVA_sequence(sva_implication.rhs())) + { + expr = implies_exprt{sva_implication.lhs(), sva_implication.rhs()}; + } + } + else if(expr.id() == ID_sva_iff) + { + auto &sva_iff = to_sva_iff_expr(expr); + expr = equal_exprt{sva_iff.lhs(), sva_iff.rhs()}; + } + else if(expr.id() == ID_sva_implies) + { + auto &sva_implies = to_sva_implies_expr(expr); + expr = implies_exprt{sva_implies.lhs(), sva_implies.rhs()}; + } + else if(expr.id() == ID_sva_and) + { + // Same as a ∧ b if lhs and rhs are not sequences. + auto &sva_and = to_sva_and_expr(expr); + if(!is_SVA_sequence(sva_and.lhs()) && !is_SVA_sequence(sva_and.rhs())) + expr = and_exprt{sva_and.lhs(), sva_and.rhs()}; + } + else if(expr.id() == ID_sva_or) + { + // Same as a ∧ b if lhs or rhs are not sequences. + auto &sva_or = to_sva_or_expr(expr); + if(!is_SVA_sequence(sva_or.lhs()) && !is_SVA_sequence(sva_or.rhs())) + expr = or_exprt{sva_or.lhs(), sva_or.rhs()}; + } + else if(expr.id() == ID_sva_not) + { + // Same as regular 'not'. These do not apply to sequences. + expr = not_exprt{to_sva_not_expr(expr).op()}; + } + else if(expr.id() == ID_sva_if) + { + auto &sva_if_expr = to_sva_if_expr(expr); + auto false_case = sva_if_expr.false_case().is_nil() + ? true_exprt{} + : sva_if_expr.false_case(); + expr = if_exprt{sva_if_expr.cond(), sva_if_expr.true_case(), false_case}; + } + else if(expr.id() == ID_sva_disable_iff) + { + auto &disable_iff_expr = to_sva_disable_iff_expr(expr); + expr = or_exprt{disable_iff_expr.lhs(), disable_iff_expr.rhs()}; + } + else if(expr.id() == ID_sva_accept_on || expr.id() == ID_sva_sync_accept_on) + { + auto &sva_abort_expr = to_sva_abort_expr(expr); + expr = or_exprt{sva_abort_expr.condition(), sva_abort_expr.property()}; + } + else if(expr.id() == ID_sva_reject_on || expr.id() == ID_sva_sync_reject_on) + { + auto &sva_abort_expr = to_sva_abort_expr(expr); + expr = and_exprt{ + not_exprt{sva_abort_expr.condition()}, sva_abort_expr.property()}; + } + else if(expr.id() == ID_sva_case) + { + expr = to_sva_case_expr(expr).lowering(); + } + + // rewrite the operands, recursively + for(auto &op : expr.operands()) + op = trivial_sva(op); + + // post-traversal + + return expr; +} diff --git a/src/temporal-logic/trivial_sva.h b/src/temporal-logic/trivial_sva.h new file mode 100644 index 000000000..33e2dd9cd --- /dev/null +++ b/src/temporal-logic/trivial_sva.h @@ -0,0 +1,32 @@ +/*******************************************************************\ + +Module: Trivial SVA + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_TEMPORAL_LOGIC_TRIVIAL_SVA_H +#define CPROVER_TEMPORAL_LOGIC_TRIVIAL_SVA_H + +#include + +/// This applies the following rewrites, removing SVA operators +/// that trivial in the sense that they are state predicates only. +/// +/// a sva_iff b --> a <-> b +/// a sva_implies b --> a -> b +/// sva_not a --> ¬a +/// a sva_and b --> a ∧ b if a and b are not sequences +/// a sva_or b --> a ∨ b if a and b are not sequences +/// sva_overlapped_implication --> a -> b if a and b are not sequences +/// sva_if --> ? : +/// sva_case --> ? : +/// a sva_disable_iff b --> a ∨ b +/// a sva_accept_on b --> a ∨ b +/// a sva_reject_on b --> ¬a ∧ b +/// a sva_sync_accept_on b --> a ∨ b +/// a sva_sync_reject_on b --> ¬a ∧ b +exprt trivial_sva(exprt); + +#endif