From 2e08a04578e28ba8935047584e1de9bafea1b769 Mon Sep 17 00:00:00 2001 From: Tobias Reiher Date: Mon, 24 Oct 2022 20:14:15 +0200 Subject: [PATCH] Add conversion of expressions to TAC Ref. #1204 --- rflx/expression.py | 306 ++++++++++++++++++++++++++- tests/unit/expression_test.py | 386 +++++++++++++++++++++++++++++++++- 2 files changed, 685 insertions(+), 7 deletions(-) diff --git a/rflx/expression.py b/rflx/expression.py index 2f7d3b80b..cff625496 100644 --- a/rflx/expression.py +++ b/rflx/expression.py @@ -6,7 +6,7 @@ import itertools import operator from abc import abstractmethod -from collections.abc import Callable, Iterable, Mapping, Sequence +from collections.abc import Callable, Generator, Iterable, Mapping, Sequence from concurrent.futures import ProcessPoolExecutor from copy import copy from dataclasses import dataclass @@ -18,7 +18,7 @@ import z3 -from rflx import ada, typing_ as rty +from rflx import ada, tac, typing_ as rty from rflx.common import Base, indent, indent_next, unique from rflx.contract import DBC, invariant, require from rflx.error import Location, RecordFluxError, Severity, Subsystem @@ -260,6 +260,10 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + @abstractmethod + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + def check(self, facts: Optional[Sequence[Expr]] = None) -> Proof: return Proof(self, facts) @@ -338,6 +342,10 @@ def z3expr(self) -> z3.BoolRef: raise Z3TypeError("negating non-boolean term") return z3.Not(z3expr) + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + inner_stmts, inner_expr = _to_tac_basic_bool(self.expr, variable_id) + return [*inner_stmts, tac.Assign(target, tac.Not(inner_expr))] + class BinExpr(Expr): def __init__( @@ -602,6 +610,33 @@ def neutral_element(self) -> int: def symbol(self) -> str: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + if len(self.terms) == 0: + return [tac.Assign(target, tac.BoolVal(True))] + + if len(self.terms) == 1: + first_stmts, first_expr = _to_tac_basic_bool(self.terms[0], variable_id) + return [*first_stmts, tac.Assign(target, first_expr)] + + if len(self.terms) == 2: + left_stmts, left_expr = _to_tac_basic_bool(self.terms[0], variable_id) + right_stmts, right_expr = _to_tac_basic_bool(self.terms[1], variable_id) + return [ + *left_stmts, + *right_stmts, + tac.Assign(target, getattr(tac, self.__class__.__name__)(left_expr, right_expr)), + ] + + right_id = next(variable_id) + left_stmts, left_expr = _to_tac_basic_bool(self.terms[0], variable_id) + return [ + *(self.__class__(*self.terms[1:]).to_tac(right_id, variable_id)), + *left_stmts, + tac.Assign( + target, getattr(tac, self.__class__.__name__)(left_expr, tac.BoolVar(right_id)) + ), + ] + class And(BoolAssExpr): def __neg__(self) -> Expr: @@ -805,6 +840,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ArithRef: return z3.IntVal(self.value) + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + return [tac.Assign(target, tac.IntVal(self.value))] + class MathAssExpr(AssExpr): def __init__(self, *terms: Expr, location: Location = None) -> None: @@ -818,6 +856,33 @@ def _check_type_subexpr(self) -> RecordFluxError: error += t.check_type_instance(rty.AnyInteger) return error + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + if len(self.terms) == 0: + return [tac.Assign(target, tac.IntVal(0))] + + if len(self.terms) == 1: + first_stmts, first_expr = _to_tac_basic_int(self.terms[0], variable_id) + return [*first_stmts, tac.Assign(target, first_expr)] + + if len(self.terms) == 2: + left_stmts, left_expr = _to_tac_basic_int(self.terms[0], variable_id) + right_stmts, right_expr = _to_tac_basic_int(self.terms[1], variable_id) + return [ + *left_stmts, + *right_stmts, + tac.Assign(target, getattr(tac, self.__class__.__name__)(left_expr, right_expr)), + ] + + right_id = next(variable_id) + left_stmts, left_expr = _to_tac_basic_int(self.terms[0], variable_id) + return [ + *(self.__class__(*self.terms[1:]).to_tac(right_id, variable_id)), + *left_stmts, + tac.Assign( + target, getattr(tac, self.__class__.__name__)(left_expr, tac.IntVar(right_id)) + ), + ] + class Add(MathAssExpr): def _update_str(self) -> None: @@ -919,6 +984,15 @@ def _check_type_subexpr(self) -> RecordFluxError: return error + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + left_stmts, left_expr = _to_tac_basic_int(self.left, variable_id) + right_stmts, right_expr = _to_tac_basic_int(self.right, variable_id) + return [ + *left_stmts, + *right_stmts, + tac.Assign(target, getattr(tac, self.__class__.__name__)(left_expr, right_expr)), + ] + class Sub(MathBinExpr): @property @@ -1137,6 +1211,14 @@ def z3expr(self) -> z3.ExprRef: return z3.BoolVal(False) return z3.Int(self.name) + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + if self.identifier == ID("True"): + return [tac.Assign(target, tac.BoolVal(True))] + if self.identifier == ID("False"): + return [tac.Assign(target, tac.BoolVal(False))] + assert self.type_ != rty.BOOLEAN + return [tac.Assign(target, tac.IntVar(self.name))] + def copy( self, identifier: StrID = None, @@ -1202,6 +1284,18 @@ def z3expr(self) -> z3.ExprRef: return -z3.Int(self.name) return z3.Int(self.name) + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + assert not isinstance(self.type_, rty.Undefined) + if self.type_ == rty.BOOLEAN: + return [tac.Assign(target, tac.BoolVar(self.name))] + if isinstance(self.type_, rty.Integer): + return [tac.Assign(target, tac.IntVar(self.name, self.negative))] + if isinstance(self.type_, rty.Message): + return [tac.Assign(target, tac.MsgVar(self.name))] + if isinstance(self.type_, rty.Sequence): + return [tac.Assign(target, tac.SeqVar(self.name))] + assert False + def copy( self, identifier: StrID = None, @@ -1273,10 +1367,16 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: if not isinstance(self.prefix, (Variable, Literal, Selected)): raise Z3TypeError("illegal prefix of attribute") - name = f"{self.prefix}'{self.__class__.__name__}" if self.negative: - return -z3.Int(name) - return z3.Int(name) + return -z3.Int(self.representation) + return z3.Int(self.representation) + + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + assert not isinstance(self.type_, rty.Undefined) + assert isinstance(self.prefix, (Variable, Literal, Selected)) + if self.type_ == rty.BOOLEAN: + return [tac.Assign(target, tac.BoolVar(self.representation))] + return [tac.Assign(target, tac.IntVar(self.representation, self.negative))] class Size(Attribute): @@ -1491,6 +1591,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + class Selected(Name): def __init__( @@ -1502,6 +1605,7 @@ def __init__( type_: rty.Type = rty.Undefined(), location: Location = None, ) -> None: + assert not prefix.negative if isinstance(prefix, Name) else True self.prefix = prefix self.selector = ID(selector) super().__init__(negative, immutable, type_, location) @@ -1574,6 +1678,24 @@ def z3expr(self) -> z3.ExprRef: return -z3.Int(self.representation) return z3.Int(self.representation) + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + assert not isinstance(self.type_, rty.Undefined) + stmts, msg = _to_tac_basic_expr(self.prefix, variable_id) + assert isinstance(msg, tac.MsgVar) + if self.type_ == rty.BOOLEAN: + return [ + *stmts, + tac.Assign(target, tac.BoolFieldAccess(msg.identifier, self.selector)), + ] + if isinstance(self.type_, rty.Integer): + return [ + *stmts, + tac.Assign( + target, tac.IntFieldAccess(msg.identifier, self.selector, self.negative) + ), + ] + assert False + def copy( self, prefix: Expr = None, @@ -1667,6 +1789,27 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + arguments_stmts = [] + arguments_exprs = [] + + for a in self.args: + a_stmts, a_expr = _to_tac_basic_expr(a, variable_id) + arguments_stmts.extend(a_stmts) + arguments_exprs.append(a_expr) + + if self.type_ is rty.BOOLEAN: + return [ + *arguments_stmts, + tac.Assign(target, tac.BoolCall(self.identifier, *arguments_exprs)), + ] + + assert isinstance(self.type_, rty.AnyInteger) + return [ + *arguments_stmts, + tac.Assign(target, tac.IntCall(self.identifier, *arguments_exprs)), + ] + def variables(self) -> list[Variable]: result = [Variable(self.identifier, location=self.location)] for t in self.args: @@ -1721,6 +1864,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + class UndefinedExpr(Name): @property @@ -1739,6 +1885,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + UNDEFINED = UndefinedExpr() @@ -1796,6 +1945,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: return z3.BoolVal(False) + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + class String(Aggregate): def __init__(self, data: str, location: Location = None) -> None: @@ -1867,6 +2019,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + class Relation(BinExpr): def __init__(self, left: Expr, right: Expr, location: Location = None) -> None: @@ -1899,6 +2054,16 @@ def _simplified(self, relation_operator: Callable[[Expr, Expr], bool]) -> Expr: def precedence(self) -> Precedence: return Precedence.RELATIONAL_OPERATOR + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + left_stmts, left_expr = _to_tac_basic_int(self.left, variable_id) + right_stmts, right_expr = _to_tac_basic_int(self.right, variable_id) + return [ + *left_stmts, + *right_stmts, + # pylint: disable-next = abstract-class-instantiated + tac.Assign(target, getattr(tac, self.__class__.__name__)(left_expr, right_expr)), + ] + class Less(Relation): def __neg__(self) -> Expr: @@ -2081,6 +2246,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.BoolRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + class NotIn(Relation): def __neg__(self) -> Expr: @@ -2101,6 +2269,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.BoolRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + class IfExpr(Expr): def __init__( @@ -2201,6 +2372,38 @@ def z3expr(self) -> z3.ExprRef: self.else_expression.z3expr(), ) + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + assert len(self.condition_expressions) == 1 + assert self.else_expression is not None + + condition = self.condition_expressions[0][0] + condition_stmts, condition_expr = _to_tac_basic_bool(condition, variable_id) + + assert condition.type_ is rty.BOOLEAN + + then_expression = self.condition_expressions[0][1] + + if then_expression.type_ is rty.BOOLEAN and self.else_expression.type_ is rty.BOOLEAN: + then_bool_stmts, then_bool_expr = _to_tac_basic_bool(then_expression, variable_id) + else_bool_stmts, else_bool_expr = _to_tac_basic_bool(self.else_expression, variable_id) + return [ + *condition_stmts, + *then_bool_stmts, + *else_bool_stmts, + tac.Assign(target, tac.BoolIfExpr(condition_expr, then_bool_expr, else_bool_expr)), + ] + + assert isinstance(then_expression.type_, rty.AnyInteger) + assert isinstance(self.else_expression.type_, rty.AnyInteger) + then_int_stmts, then_int_expr = _to_tac_basic_int(then_expression, variable_id) + else_int_stmts, else_int_expr = _to_tac_basic_int(self.else_expression, variable_id) + return [ + *condition_stmts, + *then_int_stmts, + *else_int_stmts, + tac.Assign(target, tac.IntIfExpr(condition_expr, then_int_expr, else_int_expr)), + ] + class QuantifiedExpr(Expr): def __init__( @@ -2270,6 +2473,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + def substituted( self, func: Callable[[Expr], Expr] = None, mapping: Mapping[Name, Expr] = None ) -> Expr: @@ -2375,6 +2581,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + class Conversion(Expr): def __init__( @@ -2473,6 +2682,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + def variables(self) -> list[Variable]: return self.argument.variables() @@ -2512,6 +2724,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ArithRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + class Comprehension(Expr): def __init__( @@ -2591,6 +2806,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + def variables(self) -> list[Variable]: return [ v @@ -2740,6 +2958,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + def variables(self) -> list[Variable]: result = [] for v in self.field_values.values(): @@ -2870,6 +3091,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + def variables(self) -> list[Variable]: result = [] for v in self.field_values.values(): @@ -2945,6 +3169,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + def variables(self) -> list[Variable]: return self.simplified().variables() @@ -3260,6 +3487,9 @@ def ada_expr(self) -> ada.Expr: def z3expr(self) -> z3.ExprRef: raise NotImplementedError + def to_tac(self, target: StrID, variable_id: Generator[ID, None, None]) -> list[tac.Stmt]: + raise NotImplementedError + def variables(self) -> list[Variable]: simplified = self.simplified() assert isinstance(simplified, CaseExpr) @@ -3292,3 +3522,69 @@ def _similar_field_names( ) ] return [] + + +def var_id_gen() -> Generator[ID, None, None]: + i = 0 + while True: + yield ID(f"T_{i}") + i += 1 + + +def _to_tac_basic_int( + expression: Expr, variable_id: Generator[ID, None, None] +) -> tuple[list[tac.Stmt], tac.BasicIntExpr]: + result_id = next(variable_id) + result_stmts = expression.to_tac(result_id, variable_id) + if ( + len(result_stmts) == 1 + and isinstance(result_stmts[0], tac.Assign) + and isinstance(result_stmts[0].expression, tac.BasicExpr) + ): + assert isinstance(result_stmts[0].expression, tac.BasicIntExpr) + result_expr = result_stmts[0].expression + result_stmts = [] + else: + result_expr = tac.IntVar(result_id) + return (result_stmts, result_expr) + + +def _to_tac_basic_bool( + expression: Expr, variable_id: Generator[ID, None, None] +) -> tuple[list[tac.Stmt], tac.BasicBoolExpr]: + result_id = next(variable_id) + result_stmts = expression.to_tac(result_id, variable_id) + if ( + len(result_stmts) == 1 + and isinstance(result_stmts[0], tac.Assign) + and isinstance(result_stmts[0].expression, tac.BasicExpr) + ): + assert isinstance(result_stmts[0].expression, tac.BasicBoolExpr) + result_expr = result_stmts[0].expression + result_stmts = [] + else: + result_expr = tac.BoolVar(result_id) + return (result_stmts, result_expr) + + +def _to_tac_basic_expr( + expression: Expr, variable_id: Generator[ID, None, None] +) -> tuple[list[tac.Stmt], tac.BasicExpr]: + result_id = next(variable_id) + result_stmts = expression.to_tac(result_id, variable_id) + if ( + len(result_stmts) == 1 + and isinstance(result_stmts[0], tac.Assign) + and isinstance(result_stmts[0].expression, tac.BasicExpr) + ): + result_expr = result_stmts[0].expression + result_stmts = [] + else: + assign = result_stmts[-1] + assert isinstance(assign, tac.Assign) + if isinstance(assign.expression, tac.BoolExpr): + result_expr = tac.BoolVar(result_id) + else: + assert isinstance(assign.expression, tac.IntExpr) + result_expr = tac.IntVar(result_id) + return (result_stmts, result_expr) diff --git a/tests/unit/expression_test.py b/tests/unit/expression_test.py index 9d3d12ffb..df5e4e8db 100644 --- a/tests/unit/expression_test.py +++ b/tests/unit/expression_test.py @@ -8,7 +8,7 @@ import pytest import z3 -from rflx import ada, typing_ as rty +from rflx import ada, tac, typing_ as rty from rflx.error import FatalError, Location, RecordFluxError from rflx.expression import ( FALSE, @@ -71,6 +71,7 @@ ValueRange, Variable, Z3TypeError, + var_id_gen, ) from rflx.identifier import ID, StrID from rflx.model import RangeInteger @@ -111,6 +112,12 @@ def test_true_z3expr() -> None: assert TRUE.z3expr() == z3.BoolVal(True) +def test_true_to_tac() -> None: + assert TRUE.to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.BoolVal(True)), + ] + + def test_false_type() -> None: assert_type( FALSE, @@ -130,6 +137,12 @@ def test_false_z3expr() -> None: assert FALSE.z3expr() == z3.BoolVal(False) +def test_false_to_tac() -> None: + assert FALSE.to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.BoolVal(False)), + ] + + def test_not_type() -> None: assert_type( Not(Variable("X", type_=rty.BOOLEAN)), @@ -215,6 +228,19 @@ def test_not_z3expr() -> None: Not(Variable("X")).z3expr() +def test_not_to_tac() -> None: + assert Not(TRUE).to_tac("R", var_id_gen()) == [tac.Assign("R", tac.Not(tac.BoolVal(True)))] + assert Not(Variable("X", type_=rty.BOOLEAN)).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.Not(tac.BoolVar("X"))) + ] + assert Not( + Less(Variable("X", type_=rty.Integer("I")), Variable("Y", type_=rty.Integer("I"))) + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.Less(tac.IntVar("X"), tac.IntVar("Y"))), + tac.Assign("R", tac.Not(tac.BoolVar("T_0"))), + ] + + def test_bin_expr_findall() -> None: assert Less(Variable("X"), Number(1)).findall(lambda x: isinstance(x, Number)) == [Number(1)] @@ -461,6 +487,33 @@ def test_and_z3expr() -> None: assert_equal(And(TRUE, TRUE).z3expr(), z3.And(z3.BoolVal(True), z3.BoolVal(True))) +def test_and_to_tac() -> None: + assert And().to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.BoolVal(True)), + ] + assert And(Variable("X", type_=rty.BOOLEAN)).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.BoolVar("X")), + ] + assert And( + Variable("X", type_=rty.BOOLEAN), + Variable("Y", type_=rty.BOOLEAN), + Variable("Z", type_=rty.BOOLEAN), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.And(tac.BoolVar("Y"), tac.BoolVar("Z"))), + tac.Assign("R", tac.And(tac.BoolVar("X"), tac.BoolVar("T_0"))), + ] + assert And( + And( + Variable("X", type_=rty.BOOLEAN), + Variable("Y", type_=rty.BOOLEAN), + ), + Variable("Z", type_=rty.BOOLEAN), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.And(tac.BoolVar("X"), tac.BoolVar("Y"))), + tac.Assign("R", tac.And(tac.BoolVar("T_0"), tac.BoolVar("Z"))), + ] + + def test_and_str() -> None: assert str(And(Variable("X"), Variable("Y"))) == "X\nand Y" assert str(And()) == "True" @@ -508,6 +561,33 @@ def test_or_z3expr() -> None: assert_equal(Or(TRUE, TRUE).z3expr(), z3.Or(z3.BoolVal(True), z3.BoolVal(True))) +def test_or_to_tac() -> None: + assert Or().to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.BoolVal(True)), + ] + assert Or(Variable("X", type_=rty.BOOLEAN)).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.BoolVar("X")), + ] + assert Or( + Variable("X", type_=rty.BOOLEAN), + Variable("Y", type_=rty.BOOLEAN), + Variable("Z", type_=rty.BOOLEAN), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.Or(tac.BoolVar("Y"), tac.BoolVar("Z"))), + tac.Assign("R", tac.Or(tac.BoolVar("X"), tac.BoolVar("T_0"))), + ] + assert Or( + Or( + Variable("X", type_=rty.BOOLEAN), + Variable("Y", type_=rty.BOOLEAN), + ), + Variable("Z", type_=rty.BOOLEAN), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.Or(tac.BoolVar("X"), tac.BoolVar("Y"))), + tac.Assign("R", tac.Or(tac.BoolVar("T_0"), tac.BoolVar("Z"))), + ] + + def test_or_str() -> None: assert str(Or(Variable("X"), Variable("Y"))) == "X\nor Y" assert str(Or()) == "False" @@ -721,6 +801,33 @@ def test_add_z3expr() -> None: ) +def test_add_to_tac() -> None: + assert Add().to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.IntVal(0)), + ] + assert Add(Variable("X", type_=rty.Integer("I"))).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.IntVar("X")), + ] + assert Add( + Variable("X", type_=rty.Integer("I")), + Variable("Y", type_=rty.Integer("I")), + Variable("Z", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.Add(tac.IntVar("Y"), tac.IntVar("Z"))), + tac.Assign("R", tac.Add(tac.IntVar("X"), tac.IntVar("T_0"))), + ] + assert Add( + Add( + Variable("X", type_=rty.Integer("I")), + Variable("Y", type_=rty.Integer("I")), + ), + Variable("Z", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.Add(tac.IntVar("X"), tac.IntVar("Y"))), + tac.Assign("R", tac.Add(tac.IntVar("T_0"), tac.IntVar("Z"))), + ] + + def test_add_str() -> None: assert str(Add(Number(1), Call("Test", []))) == "1 + Test" assert str(Add(Number(1), -Call("Test", []))) == "1 - Test" @@ -749,6 +856,33 @@ def test_mul_z3expr() -> None: ) +def test_mul_to_tac() -> None: + assert Mul().to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.IntVal(0)), + ] + assert Mul(Variable("X", type_=rty.Integer("I"))).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.IntVar("X")), + ] + assert Mul( + Variable("X", type_=rty.Integer("I")), + Variable("Y", type_=rty.Integer("I")), + Variable("Z", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.Mul(tac.IntVar("Y"), tac.IntVar("Z"))), + tac.Assign("R", tac.Mul(tac.IntVar("X"), tac.IntVar("T_0"))), + ] + assert Mul( + Mul( + Variable("X", type_=rty.Integer("I")), + Variable("Y", type_=rty.Integer("I")), + ), + Variable("Z", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.Mul(tac.IntVar("X"), tac.IntVar("Y"))), + tac.Assign("R", tac.Mul(tac.IntVar("T_0"), tac.IntVar("Z"))), + ] + + def test_sub_neg() -> None: assert -Sub(Number(1), Variable("X")) == Sub(Number(-1), Variable("X")) @@ -775,6 +909,25 @@ def test_sub_z3expr() -> None: assert Sub(Number(12), Number(20)).z3expr() == z3.IntVal(12) - z3.IntVal(20) +def test_sub_to_tac() -> None: + assert Sub( + Variable("X", type_=rty.Integer("I")), + Variable("Y", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.Sub(tac.IntVar("X"), tac.IntVar("Y"))), + ] + assert Sub( + Sub( + Variable("X", type_=rty.Integer("I")), + Variable("Y", type_=rty.Integer("I")), + ), + Variable("Z", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.Sub(tac.IntVar("X"), tac.IntVar("Y"))), + tac.Assign("R", tac.Sub(tac.IntVar("T_0"), tac.IntVar("Z"))), + ] + + def test_div_neg() -> None: assert -Div(Variable("X"), Number(1)) == Div(Variable("X", negative=True), Number(1)) @@ -793,6 +946,25 @@ def test_div_z3expr() -> None: assert Div(Number(6), Number(3)).z3expr() == z3.IntVal(6) / z3.IntVal(3) +def test_div_to_tac() -> None: + assert Div( + Variable("X", type_=rty.Integer("I")), + Variable("Y", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.Div(tac.IntVar("X"), tac.IntVar("Y"))), + ] + assert Div( + Div( + Variable("X", type_=rty.Integer("I")), + Variable("Y", type_=rty.Integer("I")), + ), + Variable("Z", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.Div(tac.IntVar("X"), tac.IntVar("Y"))), + tac.Assign("R", tac.Div(tac.IntVar("T_0"), tac.IntVar("Z"))), + ] + + def test_pow_simplified() -> None: assert Pow(Variable("X"), Number(1)).simplified() == Pow(Variable("X"), Number(1)) assert Pow(Variable("X"), Add(Number(1), Number(1))).simplified() == Pow( @@ -809,6 +981,25 @@ def test_pow_z3expr() -> None: assert Pow(Number(6), Number(2)).z3expr() == z3.IntVal(6) ** z3.IntVal(2) +def test_pow_to_tac() -> None: + assert Pow( + Variable("X", type_=rty.Integer("I")), + Variable("Y", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.Pow(tac.IntVar("X"), tac.IntVar("Y"))), + ] + assert Pow( + Pow( + Variable("X", type_=rty.Integer("I")), + Variable("Y", type_=rty.Integer("I")), + ), + Variable("Z", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.Pow(tac.IntVar("X"), tac.IntVar("Y"))), + tac.Assign("R", tac.Pow(tac.IntVar("T_0"), tac.IntVar("Z"))), + ] + + def test_mod_simplified() -> None: assert Mod(Variable("X"), Number(1)).simplified() == Mod(Variable("X"), Number(1)) assert Mod(Variable("X"), Add(Number(1), Number(1))).simplified() == Mod( @@ -831,6 +1022,25 @@ def test_mod_z3expr_error() -> None: Mod(Pow(Variable("X"), Number(2)), Number(5)).z3expr() +def test_mod_to_tac() -> None: + assert Mod( + Variable("X", type_=rty.Integer("I")), + Variable("Y", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.Mod(tac.IntVar("X"), tac.IntVar("Y"))), + ] + assert Mod( + Mod( + Variable("X", type_=rty.Integer("I")), + Variable("Y", type_=rty.Integer("I")), + ), + Variable("Z", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.Mod(tac.IntVar("X"), tac.IntVar("Y"))), + tac.Assign("R", tac.Mod(tac.IntVar("T_0"), tac.IntVar("Z"))), + ] + + def test_term_simplified() -> None: assert_equal( Add( @@ -840,6 +1050,12 @@ def test_term_simplified() -> None: ) +def test_literal_to_tac() -> None: + assert Literal("X", type_=rty.Integer("I")).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.IntVar("X")) + ] + + def test_variable_invalid_name() -> None: with pytest.raises(FatalError): Variable("Foo (Bar)") @@ -898,6 +1114,24 @@ def test_variable_z3expr() -> None: assert z3.simplify(Sub(Variable("X"), Variable("X")).z3expr()) == z3.IntVal(0) +def test_variable_to_tac() -> None: + assert Variable("X", type_=rty.BOOLEAN).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.BoolVar("X")), + ] + assert Variable("X", type_=rty.Integer("I")).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.IntVar("X")) + ] + assert Variable("X", type_=rty.Integer("I"), negative=True).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.IntVar("X", negative=True)) + ] + assert Variable("X", type_=rty.Message("S")).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.MsgVar("X")) + ] + assert Variable("X", type_=rty.Sequence("S", rty.Integer("I"))).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.SeqVar("X")) + ] + + def test_attribute() -> None: assert isinstance(Size("X"), Attribute) assert isinstance(Length("X"), Attribute) @@ -1064,6 +1298,32 @@ def test_attribute_z3expr_error() -> None: First(Call("X")).z3expr() +@pytest.mark.parametrize( + "attribute, tac_name", + [ + (Size("X"), "X'Size"), + (Length("X"), "X'Length"), + (First("X"), "X'First"), + (Last("X"), "X'Last"), + ], +) +def test_attribute_to_tac_int(attribute: Expr, tac_name: str) -> None: + assert attribute.to_tac("R", var_id_gen()) == [tac.Assign("R", tac.IntVar(tac_name))] + + +@pytest.mark.parametrize( + "attribute, tac_name", + [ + (ValidChecksum("X"), "X'Valid_Checksum"), + (Valid("X"), "X'Valid"), + (Present("X"), "X'Present"), + (HasData("X"), "X'Has_Data"), + ], +) +def test_attribute_to_tac_bool(attribute: Expr, tac_name: str) -> None: + assert attribute.to_tac("R", var_id_gen()) == [tac.Assign("R", tac.BoolVar(tac_name))] + + def test_val_substituted() -> None: assert_equal( Val("X", Variable("Y")).substituted( @@ -1308,6 +1568,12 @@ def test_less_z3expr() -> None: assert Less(Number(1), Number(100)).z3expr() == (z3.IntVal(1) < z3.IntVal(100)) +def test_less_to_tac() -> None: + assert Less(Variable("X", type_=rty.Integer("I")), Number(10)).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.Less(tac.IntVar("X"), tac.IntVal(10))), + ] + + def test_less_equal_neg() -> None: assert -LessEqual(Variable("X"), Number(1)) == Greater(Variable("X"), Number(1)) @@ -1322,6 +1588,14 @@ def test_less_equal_z3expr() -> None: assert LessEqual(Number(1), Number(100)).z3expr() == (z3.IntVal(1) <= z3.IntVal(100)) +def test_less_equal_to_tac() -> None: + assert LessEqual(Variable("X", type_=rty.Integer("I")), Number(10)).to_tac( + "R", var_id_gen() + ) == [ + tac.Assign("R", tac.LessEqual(tac.IntVar("X"), tac.IntVal(10))), + ] + + def test_equal_neg() -> None: assert -Equal(Variable("X"), Number(1)) == NotEqual(Variable("X"), Number(1)) @@ -1336,6 +1610,12 @@ def test_equal_z3expr() -> None: assert Equal(Number(100), Number(100)).z3expr() == (z3.IntVal(100) == z3.IntVal(100)) +def test_equal_to_tac() -> None: + assert Equal(Variable("X", type_=rty.Integer("I")), Number(10)).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.Equal(tac.IntVar("X"), tac.IntVal(10))), + ] + + def test_greater_equal_neg() -> None: assert -GreaterEqual(Variable("X"), Number(1)) == Less(Variable("X"), Number(1)) @@ -1350,6 +1630,14 @@ def test_greater_equal_z3expr() -> None: assert GreaterEqual(Number(100), Number(1)).z3expr() == (z3.IntVal(100) >= z3.IntVal(1)) +def test_greater_equal_to_tac() -> None: + assert GreaterEqual(Variable("X", type_=rty.Integer("I")), Number(10)).to_tac( + "R", var_id_gen() + ) == [ + tac.Assign("R", tac.GreaterEqual(tac.IntVar("X"), tac.IntVal(10))), + ] + + def test_greater_neg() -> None: assert -Greater(Variable("X"), Number(1)) == LessEqual(Variable("X"), Number(1)) @@ -1364,6 +1652,12 @@ def test_greater_z3expr() -> None: assert Greater(Number(100), Number(1)).z3expr() == (z3.IntVal(100) > z3.IntVal(1)) +def test_greater_to_tac() -> None: + assert Greater(Variable("X", type_=rty.Integer("I")), Number(10)).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.Greater(tac.IntVar("X"), tac.IntVal(10))), + ] + + def test_not_equal_neg() -> None: assert -NotEqual(Variable("X"), Number(1)) == Equal(Variable("X"), Number(1)) @@ -1378,6 +1672,14 @@ def test_not_equal_z3expr() -> None: assert NotEqual(Number(100), Number(1)).z3expr() == (z3.IntVal(100) != z3.IntVal(1)) +def test_not_equal_to_tac() -> None: + assert NotEqual(Variable("X", type_=rty.Integer("I")), Number(10)).to_tac( + "R", var_id_gen() + ) == [ + tac.Assign("R", tac.NotEqual(tac.IntVar("X"), tac.IntVal(10))), + ] + + def test_in_neg() -> None: assert -In(Number(1), Variable("X")) == NotIn(Number(1), Variable("X")) @@ -1457,7 +1759,7 @@ def test_if_expr_ada_expr() -> None: ) -def test_if_expr_z3() -> None: +def test_if_expr_z3expr() -> None: assert IfExpr([(TRUE, Variable("Y"))], Variable("Z")).z3expr() == z3.If( z3.BoolVal(True), z3.Int("Y"), z3.Int("Z") ) @@ -1471,6 +1773,35 @@ def test_if_expr_z3() -> None: IfExpr([(Variable("X"), Variable("Y"))], Variable("Z")).z3expr() +def test_if_expr_to_tac() -> None: + assert IfExpr( + [(Variable("X", type_=rty.BOOLEAN), Variable("Y", type_=rty.BOOLEAN))], + Variable("Z", type_=rty.BOOLEAN), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.BoolIfExpr(tac.BoolVar("X"), tac.BoolVar("Y"), tac.BoolVar("Z"))), + ] + assert IfExpr( + [(Variable("X", type_=rty.BOOLEAN), Variable("Y", type_=rty.Integer("I")))], + Variable("Z", type_=rty.Integer("I")), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.IntIfExpr(tac.BoolVar("X"), tac.IntVar("Y"), tac.IntVar("Z"))), + ] + assert IfExpr( + [ + ( + And(Variable("X", type_=rty.BOOLEAN), TRUE), + Add(Variable("Y", type_=rty.Integer("I")), Number(1)), + ) + ], + Sub(Variable("Z", type_=rty.Integer("I")), Number(2)), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.And(tac.BoolVar("X"), tac.BoolVal(True))), + tac.Assign("T_3", tac.Add(tac.IntVar("Y"), tac.IntVal(1))), + tac.Assign("T_6", tac.Sub(tac.IntVar("Z"), tac.IntVal(2))), + tac.Assign("R", tac.IntIfExpr(tac.BoolVar("T_0"), tac.IntVar("T_3"), tac.IntVar("T_6"))), + ] + + def test_value_range_type() -> None: assert_type( ValueRange(Number(1), Number(42)), @@ -1771,6 +2102,10 @@ def test_number_z3expr() -> None: assert Number(42).z3expr() == z3.IntVal(42) +def test_number_to_tac() -> None: + assert Number(42).to_tac("R", var_id_gen()) == [tac.Assign("R", tac.IntVal(42))] + + def test_number_str() -> None: assert str(Number(15)) == "15" @@ -1916,6 +2251,24 @@ def test_selected_z3expr() -> None: assert Selected(Variable("X"), "Y", negative=True).z3expr() == -z3.Int("X.Y") +def test_selected_to_tac() -> None: + assert Selected(Variable("X", type_=rty.Message("M")), "Y", type_=rty.BOOLEAN).to_tac( + "R", var_id_gen() + ) == [ + tac.Assign("R", tac.BoolFieldAccess("X", "Y")), + ] + assert Selected(Variable("X", type_=rty.Message("M")), "Y", type_=rty.Integer("I")).to_tac( + "R", var_id_gen() + ) == [ + tac.Assign("R", tac.IntFieldAccess("X", "Y")), + ] + assert Selected( + Variable("X", type_=rty.Message("M")), "Y", negative=True, type_=rty.Integer("I") + ).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.IntFieldAccess("X", "Y", negative=True)), + ] + + def test_in_variables() -> None: result = In(Variable("A"), Variable("B")).variables() expected = [Variable("A"), Variable("B")] @@ -1978,6 +2331,35 @@ def test_call_str() -> None: assert str(-Call("Test", [])) == "(-Test)" +def test_call_to_tac() -> None: + assert Call( + "X", + [Variable("Y", type_=rty.BOOLEAN), Variable("Z", type_=rty.Integer("I"))], + type_=rty.Integer("I"), + ).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.IntCall("X", tac.BoolVar("Y"), tac.IntVar("Z"))), + ] + assert Call( + "X", + [Variable("Y", type_=rty.BOOLEAN), Variable("Z", type_=rty.BOOLEAN)], + type_=rty.BOOLEAN, + ).to_tac("R", var_id_gen()) == [ + tac.Assign("R", tac.BoolCall("X", tac.BoolVar("Y"), tac.BoolVar("Z"))), + ] + assert Call( + "X", + [ + And(Variable("X", type_=rty.BOOLEAN), TRUE), + Add(Variable("Y", type_=rty.Integer("I")), Number(1)), + ], + type_=rty.BOOLEAN, + ).to_tac("R", var_id_gen()) == [ + tac.Assign("T_0", tac.And(tac.BoolVar("X"), tac.BoolVal(True))), + tac.Assign("T_3", tac.Add(tac.IntVar("Y"), tac.IntVal(1))), + tac.Assign("R", tac.BoolCall("X", tac.BoolVar("T_0"), tac.IntVar("T_3"))), + ] + + def test_conversion_type() -> None: assert_type( Conversion(