From 9c1d83cc834c3f336fb12386c216420be1f8e85f Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 19 Sep 2023 16:15:41 -0500 Subject: [PATCH] Allow second argument of shift operators to be non-constant --- src/lustre/lustreExpr.ml | 21 ++++--------------- src/lustre/lustreExpr.mli | 1 - src/lustre/lustreSimplify.ml | 9 -------- src/lustre/lustreTypeChecker.ml | 6 +----- src/lustre/lustreTypeChecker.mli | 1 - .../lustreTypeChecker/bv-sh-exception.lus | 8 ------- .../lustreTypeChecker/machine_integer_06.lus | 5 ----- tests/ounit/lustre/testLustreFrontend.ml | 8 ------- 8 files changed, 5 insertions(+), 54 deletions(-) delete mode 100644 tests/ounit/lustre/lustreTypeChecker/bv-sh-exception.lus delete mode 100644 tests/ounit/lustre/lustreTypeChecker/machine_integer_06.lus diff --git a/src/lustre/lustreExpr.ml b/src/lustre/lustreExpr.ml index bb96b8ee8..67405ec99 100644 --- a/src/lustre/lustreExpr.ml +++ b/src/lustre/lustreExpr.ml @@ -26,7 +26,6 @@ module VS = Var.VarSet (* Exceptions *) exception Type_mismatch -exception NonConstantShiftOperand (* A Lustre expression is a term *) type expr = Term.t @@ -2981,13 +2980,7 @@ let mk_bvor expr1 expr2 = mk_binary eval_bvor type_of_bvor expr1 expr2 (* Evaluate bitvector left shift *) -let eval_bvshl expr1 expr2 = - if ((Term.is_bitvector expr2) && (Type.is_ubitvector (Term.type_of_term expr2))) then - Term.mk_bvshl [expr1; expr2] - else - match Term.destruct expr1, Term.destruct expr2 with - | _ -> raise NonConstantShiftOperand - | exception Invalid_argument _ -> Term.mk_bvshl [expr1; expr2] +let eval_bvshl expr1 expr2 = Term.mk_bvshl [expr1; expr2] (* Type of bitvector left shift *) @@ -3002,17 +2995,11 @@ let mk_bvshl expr1 expr2 = mk_binary eval_bvshl type_of_bvshl expr1 expr2 (* Evaluate bitvector (logical or arithmetic) right shift *) -let eval_bvshr expr1 expr2 = - if ((Term.is_bitvector expr2) && (Type.is_ubitvector (Term.type_of_term expr2)) - && (Type.is_bitvector (Term.type_of_term expr1))) then +let eval_bvshr expr1 expr2 = + if (Type.is_bitvector (Term.type_of_term expr1)) then Term.mk_bvashr [expr1; expr2] - else if ((Term.is_bitvector expr2) && (Type.is_ubitvector (Term.type_of_term expr2)) - && (Type.is_ubitvector (Term.type_of_term expr1))) then - Term.mk_bvlshr [expr1; expr2] else - match Term.destruct expr1, Term.destruct expr2 with - | _ -> raise NonConstantShiftOperand - | exception Invalid_argument _ -> Term.mk_bvshl [expr1; expr2] + Term.mk_bvlshr [expr1; expr2] (* Type of bitvector logical right shift *) diff --git a/src/lustre/lustreExpr.mli b/src/lustre/lustreExpr.mli index ba031ec03..c5486ab35 100644 --- a/src/lustre/lustreExpr.mli +++ b/src/lustre/lustreExpr.mli @@ -55,7 +55,6 @@ (** Types of expressions do not match signature of operator *) exception Type_mismatch -exception NonConstantShiftOperand (** {1 Types} *) diff --git a/src/lustre/lustreSimplify.ml b/src/lustre/lustreSimplify.ml index 56b967cf9..b5c5c1d92 100644 --- a/src/lustre/lustreSimplify.ml +++ b/src/lustre/lustreSimplify.ml @@ -1590,15 +1590,6 @@ and eval_binary_ast_expr bounds ctx pos mk expr1 expr2 = A.pp_print_expr expr1 A.pp_print_expr expr2) - | E.NonConstantShiftOperand -> - - fail_at_position - pos - (Format.asprintf - "Second argument %a to shift operation - must be constant" - A.pp_print_expr expr2) - in (res, ctx) diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index 12f39c4cb..2b302d857 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/src/lustre/lustreTypeChecker.ml @@ -79,7 +79,6 @@ type error_kind = Unknown of string | ExpectedIntegerTypes of tc_type * tc_type | ExpectedNumberTypes of tc_type * tc_type | ExpectedMachineIntegerTypes of tc_type * tc_type - | ExpectedBitShiftConstant | ExpectedBitShiftConstantOfSameWidth of tc_type | ExpectedBitShiftMachineIntegerType of tc_type | InvalidConversion of tc_type * tc_type @@ -162,7 +161,6 @@ let error_message kind = match kind with ^ string_of_tc_type ty1 ^ " and " ^ string_of_tc_type ty2 | ExpectedMachineIntegerTypes (ty1, ty2) -> "Expected both arguments of operator to be of machine integer type but found " ^ string_of_tc_type ty1 ^ " and " ^ string_of_tc_type ty2 - | ExpectedBitShiftConstant -> "Expected argument of shift operator to be a constant" | ExpectedBitShiftConstantOfSameWidth ty -> "Expected second argument of shit opperator to be a constant of type " ^ "unsigned machine integer of the same width as first argument but found type " ^ string_of_tc_type ty | ExpectedBitShiftMachineIntegerType ty -> "Expected first argument of shit operator to be of type signed " @@ -786,9 +784,7 @@ and infer_type_binary_op: tc_context -> Lib.position if (LH.is_type_signed_machine_int ty1 || LH.is_type_unsigned_machine_int ty1) then (if (LH.is_type_unsigned_machine_int ty2 && LH.is_machine_type_of_associated_width (ty1, ty2)) - then if is_expr_of_consts ctx e2 - then R.ok ty1 - else type_error pos ExpectedBitShiftConstant + then R.ok ty1 else type_error pos (ExpectedBitShiftConstantOfSameWidth ty1)) else type_error pos (ExpectedBitShiftMachineIntegerType ty1) (** infers the type of binary operators *) diff --git a/src/lustre/lustreTypeChecker.mli b/src/lustre/lustreTypeChecker.mli index add3870ea..caca9adb8 100644 --- a/src/lustre/lustreTypeChecker.mli +++ b/src/lustre/lustreTypeChecker.mli @@ -64,7 +64,6 @@ type error_kind = Unknown of string | ExpectedIntegerTypes of tc_type * tc_type | ExpectedNumberTypes of tc_type * tc_type | ExpectedMachineIntegerTypes of tc_type * tc_type - | ExpectedBitShiftConstant | ExpectedBitShiftConstantOfSameWidth of tc_type | ExpectedBitShiftMachineIntegerType of tc_type | InvalidConversion of tc_type * tc_type diff --git a/tests/ounit/lustre/lustreTypeChecker/bv-sh-exception.lus b/tests/ounit/lustre/lustreTypeChecker/bv-sh-exception.lus deleted file mode 100644 index fd1dc5502..000000000 --- a/tests/ounit/lustre/lustreTypeChecker/bv-sh-exception.lus +++ /dev/null @@ -1,8 +0,0 @@ -node top (reset: bool) returns (OK: bool); -var i,j : uint8; -let - j = uint8 1; - i = (uint8 1) rsh j; - OK = i > (uint8 0); - --%PROPERTY OK; -tel diff --git a/tests/ounit/lustre/lustreTypeChecker/machine_integer_06.lus b/tests/ounit/lustre/lustreTypeChecker/machine_integer_06.lus deleted file mode 100644 index ac2b9c9be..000000000 --- a/tests/ounit/lustre/lustreTypeChecker/machine_integer_06.lus +++ /dev/null @@ -1,5 +0,0 @@ - -node top(x1, x2: uint8) returns (y: uint8); -let - y = x1 lsh x2; -tel \ No newline at end of file diff --git a/tests/ounit/lustre/testLustreFrontend.ml b/tests/ounit/lustre/testLustreFrontend.ml index 76a30d248..48b85cae4 100644 --- a/tests/ounit/lustre/testLustreFrontend.ml +++ b/tests/ounit/lustre/testLustreFrontend.ml @@ -395,10 +395,6 @@ let _ = run_test_tt_main ("frontend LustreTypeChecker error tests" >::: [ match load_file "./lustreTypeChecker/abstract_type.lus" with | Error (`LustreTypeCheckerError (_, ExpectedNumberTypes _)) -> true | _ -> false); - mk_test "test non constant bit shift" (fun () -> - match load_file "./lustreTypeChecker/bv-sh-exception.lus" with - | Error (`LustreTypeCheckerError (_, ExpectedBitShiftConstant)) -> true - | _ -> false); mk_test "test non-number (bool) cast to int" (fun () -> match load_file "./lustreTypeChecker/cast_01.lus" with | Error (`LustreTypeCheckerError (_, InvalidConversion _)) -> true @@ -471,10 +467,6 @@ let _ = run_test_tt_main ("frontend LustreTypeChecker error tests" >::: [ match load_file "./lustreTypeChecker/machine_integer_05.lus" with | Error (`LustreTypeCheckerError (_, ExpectedBitShiftMachineIntegerType _)) -> true | _ -> false); - mk_test "test machine int op 6" (fun () -> - match load_file "./lustreTypeChecker/machine_integer_06.lus" with - | Error (`LustreTypeCheckerError (_, ExpectedBitShiftConstant)) -> true - | _ -> false); mk_test "test merge case missing" (fun () -> match load_file "./lustreTypeChecker/merge_enum.lus" with | Error (`LustreTypeCheckerError (_, MergeCaseMissing _)) -> true