[ASL] Asl allow more atcs

asllib/Interpreter.ml

@@ -298,8 +298,10 @@ module Make (B : Backend.S) (C : Config) = struct
   (* Utils *)
   (* ----- *)
   let v_false = L_Bool false |> B.v_of_literal
-  let m_false = return v_false
+  let v_true = L_Bool true |> B.v_of_literal
   let v_zero = L_Int Z.zero |> B.v_of_literal
+  let m_false = return v_false
+  let m_true = return v_true
   let m_zero = return v_zero
 
   let sync_list ms =
@@ -563,36 +565,48 @@ module Make (B : Backend.S) (C : Config) = struct
 
   (* Begin ValOfType *)
   and is_val_of_type loc env v ty : bool B.m =
-    let value_m_to_bool_m m = choice m true false in
     let big_or = big_op m_false (B.binop BOR) in
-    match ty.desc with
-    | T_Int UnConstrained -> return true
-    | T_Int (UnderConstrained _) ->
-        (* This cannot happen, because:
-           1. Forgetting now about named types, or any kind of compound types,
-              you cannot ask: [expr as ty] if ty is the unconstrained integer
-              because there is no syntax for it.
-           2. You cannot construct a type that is an alias for the
-              underconstrained integer type.
-           3. You cannot put the underconstrained integer type in a compound
-              type.
-        *)
-        fatal_from loc Error.UnrespectedParserInvariant
-    | T_Bits (e, _) ->
-        let* v' = eval_expr_sef env e and* v_length = B.bitvector_length v in
-        B.binop EQ_OP v_length v' |> value_m_to_bool_m
-    | T_Int (WellConstrained constraints) ->
-        let map_constraint = function
-          | Constraint_Exact e ->
-              let* v' = eval_expr_sef env e in
-              B.binop EQ_OP v v'
-          | Constraint_Range (e1, e2) ->
-              let* v1 = eval_expr_sef env e1 and* v2 = eval_expr_sef env e2 in
-              let* c1 = B.binop LEQ v1 v and* c2 = B.binop LEQ v v2 in
-              B.binop BAND c1 c2
-        in
-        List.map map_constraint constraints |> big_or |> value_m_to_bool_m
-    | _ -> fatal_from loc TypeInferenceNeeded
+    let rec in_values v ty =
+      match ty.desc with
+      | T_Int UnConstrained -> m_true
+      | T_Int (UnderConstrained _) ->
+          (* This cannot happen, because:
+             1. Forgetting now about named types, or any kind of compound types,
+                you cannot ask: [expr as ty] if ty is the unconstrained integer
+                because there is no syntax for it.
+             2. You cannot construct a type that is an alias for the
+                underconstrained integer type.
+             3. You cannot put the underconstrained integer type in a compound
+                type.
+          *)
+          fatal_from loc Error.UnrespectedParserInvariant
+      | T_Bits (e, _) ->
+          let* v' = eval_expr_sef env e and* v_length = B.bitvector_length v in
+          B.binop EQ_OP v_length v'
+      | T_Int (WellConstrained constraints) ->
+          let map_constraint = function
+            | Constraint_Exact e ->
+                let* v' = eval_expr_sef env e in
+                B.binop EQ_OP v v'
+            | Constraint_Range (e1, e2) ->
+                let* v1 = eval_expr_sef env e1 and* v2 = eval_expr_sef env e2 in
+                let* c1 = B.binop LEQ v1 v and* c2 = B.binop LEQ v v2 in
+                B.binop BAND c1 c2
+          in
+          List.map map_constraint constraints |> big_or
+      | T_Tuple tys ->
+          let fold (i, prev) ty' =
+            let m =
+              let* v' = B.get_index i v in
+              let* here = in_values v' ty' in
+              prev >>= B.binop BAND here
+            in
+            (i + 1, m)
+          in
+          List.fold_left fold (0, m_true) tys |> snd
+      | _ -> fatal_from loc TypeInferenceNeeded
+    in
+    choice (in_values v ty) true false
   (* End *)
 
   (* Evaluation of Left-Hand-Side Expressions *)

asllib/Typing.ml

@@ -213,6 +213,7 @@ module Property (C : ANNOTATE_CONFIG) = struct
   let ok () = () [@@inline]
   let check_true b fail () = if b then () else fail () [@@inline]
   let check_true' b = check_true b assumption_failed [@@inline]
+  let check_all2 li1 li2 f () = List.iter2 (fun x1 x2 -> f x1 x2 ()) li1 li2
 end
 
 (* -------------------------------------------------------------------------
@@ -871,6 +872,16 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
         t1 |: TypingRule.CheckUnop
   (* End *)
 
+  let rec check_atc ~fail env t1 t2 =
+    if Types.type_equal env t1 t2 then ok
+    else
+      match (t1.desc, t2.desc) with
+      | T_Int _, T_Int _ | T_Bits _, T_Bits _ -> ok
+      | T_Tuple l1, T_Tuple l2 when List.compare_lengths l1 l2 = 0 ->
+          check_all2 l1 l2 (check_atc ~fail env)
+      | T_Named _, _ | _, T_Named _ -> assert false
+      | _ -> fail
+
   let var_in_env ?(local = true) env x =
     (local && IMap.mem x env.local.storage_types)
     || IMap.mem x env.global.storage_types
@@ -1399,12 +1410,12 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
         let t_struct = Types.get_structure env t in
         let ty' = annotate_type ~loc env ty in
         let ty_struct = Types.get_structure env ty' in
-        (if Types.type_equal env t_struct ty_struct then (ty', e'')
-         else
-           match (t_struct.desc, ty_struct.desc) with
-           | T_Bits _, T_Bits _ | T_Int _, T_Int _ ->
-               (ty', E_ATC (e'', ty_struct) |> here)
-           | _ -> fatal_from e (BadATC (t, ty')))
+        let+ () =
+          check_atc env t_struct ty_struct ~fail:(fun () ->
+              fatal_from loc (BadATC (t, ty)))
+        in
+        (if Types.subtype_satisfies env t ty' then (ty', e'')
+         else (ty', E_ATC (e'', ty_struct) |> here))
         |: TypingRule.ATC
     (* End *)
     | E_Var x -> (

asllib/tests/atcs.t

@@ -64,9 +64,9 @@ ATCs on other types
   > end
 
   $ aslref atcs6.asl
-  File atcs6.asl, line 3, characters 11 to 33:
-  ASL Typing error: cannot perform Asserted Type Conversion on
-    (integer {42}, bits(4)) by myty.
+  File atcs6.asl, line 3, characters 11 to 25:
+  ASL Execution error: Mismatch type:
+    value [42, '0000'] does not belong to type (integer {0..10}, bits(4)).
   [1]
 
   $ cat > atcs7.asl <<EOF

asllib/tests/typing.t/HExample14.asl

@@ -0,0 +1,15 @@
+func Reverse{N}(word : bits(N), M : integer{1..N}) => bits(N)
+begin
+    return Zeros(N);
+end
+
+func main () => integer
+begin
+  let c = 8 << UInt (UNKNOWN: bits(2)); // integer {8, 16, 32, 64}
+  let bv = Zeros(c);
+  let res = Reverse(bv, 8);
+
+  return 0;
+end
+
+

asllib/tests/typing.t/HExample15.asl

@@ -0,0 +1,6 @@
+func HExample15(x: integer {4, 8}, y: integer {4, 8}, a: integer)
+begin
+  let d = x DIV y;
+  let - = a < d;
+end
+

asllib/tests/typing.t/HExample16.asl

@@ -0,0 +1,11 @@
+func Reverse{N}(word : bits(N), M : integer{1..N}) => bits(N)
+begin
+    return Zeros(N);
+end
+
+func HExemple16 (a: integer {8, 16, 32, 64}, b: integer {8, 16, 32, 64})
+begin
+  if a < b then Unreachable(); end
+  let bv = Zeros(a);
+  let -: bits(a) = Reverse(bv, b);
+end

asllib/tests/typing.t/HExample17.asl

@@ -0,0 +1,12 @@
+func Reverse{N}(word : bits(N), M : integer{1..N}) => bits(N)
+begin
+    return Zeros(N);
+end
+
+func HExemple17 (a: integer {8, 16, 32, 64})
+begin
+  if a != 64 then Unreachable(); end
+  let b = 32;
+  let bv = Zeros(a);
+  let -: bits(a) = Reverse(bv, b);
+end

asllib/tests/typing.t/HExample18.asl

@@ -0,0 +1,14 @@
+func Reverse{N}(word : bits(N), M : integer{1..N}) => bits(N)
+begin
+    return Zeros(N);
+end
+
+func HExemple18 (a: bits(2))
+begin
+  if a IN {'0x'} then Unreachable(); end
+  let a2 = 8 << UInt(a);
+  let bv = Zeros(a2);
+  let b = 16;
+  let -: bits(a2) = Reverse(bv, a2);
+end
+

asllib/tests/typing.t/KPositive01.asl

@@ -0,0 +1,3 @@
+type ty of integer{-1..2};
+let w : ty = 2;
+var x: bits(w) = '11'; 

asllib/tests/typing.t/run.t

@@ -12,6 +12,22 @@ H Examples
   $ aslref --no-exec HExample11.asl
   $ aslref --no-exec HExample12.asl
   $ aslref --no-exec HExample13.asl
+  $ aslref --no-exec HExample15.asl
+  $ aslref --no-exec HExample16.asl
+  File HExample16.asl, line 10, characters 19 to 33:
+  ASL Typing error: a subtype of integer {1..a} was expected,
+    provided integer {8, 16, 32, 64}.
+  [1]
+  $ aslref --no-exec HExample17.asl
+  File HExample17.asl, line 11, characters 19 to 33:
+  ASL Typing error: a subtype of integer {1..a} was expected,
+    provided integer {32}.
+  [1]
+  $ aslref --no-exec HExample18.asl
+  File HExample18.asl, line 12, characters 20 to 35:
+  ASL Typing error: a subtype of integer {1..a2} was expected,
+    provided integer {8, 16, 32, 64}.
+  [1]
 
 T Tests
   $ aslref --no-exec TPositive1.asl
@@ -102,6 +118,7 @@ Named types
   ASL Typing error: a subtype of MyOtherSizes was expected,
     provided MyBitsSizes.
   [1]
+  $ aslref --no-exec KPositive01.asl
 
 Loops
   $ aslref --no-exec TPositive8.asl