Merge pull request kind2-mc#1009 from daniel-larraz/non-const-shift-arg

Allow second argument of shift operators to be non-constant

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 *)

src/lustre/lustreExpr.mli

@@ -55,7 +55,6 @@
 
 (** Types of expressions do not match signature of operator *)
 exception Type_mismatch
-exception NonConstantShiftOperand
 
 (** {1 Types} *)
 

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)

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  *)

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

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