Merge pull request #799 from herd/asl-valid-types

Validates ASL types that are provided by the user.

asllib/AST.mli

@@ -174,7 +174,7 @@ and type_desc =
   | T_Bool
   | T_Enum of identifier list
   | T_Tuple of ty list
-  | T_Array of expr * ty
+  | T_Array of array_index * ty
   | T_Record of field list
   | T_Exception of field list
   | T_Named of identifier  (** A type variable. *)
@@ -208,6 +208,13 @@ and bitfield =
   | BitField_Type of identifier * slice list * ty
       (** A name, its corresponding slice and the type of the bitfield. *)
 
+(** The type of indexes for an array. *)
+and array_index =
+  | ArrayLength_Expr of expr
+      (** An integer expression giving the length of the array. *)
+  | ArrayLength_Enum of identifier * int
+      (** An enumeration name and its length. *)
+
 and field = identifier * ty
 (** A field of a record-like structure. *)
 

asllib/ASTUtils.ml

@@ -203,7 +203,8 @@ and use_ty acc t =
   | T_Int (WellConstrained cs) -> use_constraints acc cs
   | T_Tuple li -> List.fold_left use_ty acc li
   | T_Record fields | T_Exception fields -> fold_named_list use_ty acc fields
-  | T_Array (e, t') -> use_ty (use_e acc e) t'
+  | T_Array (ArrayLength_Expr e, t') -> use_ty (use_e acc e) t'
+  | T_Array (ArrayLength_Enum (s, _), t') -> use_ty (ISet.add s acc) t'
   | T_Bits (e, bit_fields) -> use_bitfields (use_e acc e) bit_fields
 
 and use_bitfields acc bitfields = List.fold_left use_bitfield acc bitfields
@@ -381,6 +382,14 @@ and constraint_equal eq c1 c2 =
 and constraints_equal eq cs1 cs2 =
   cs1 == cs2 || list_equal (constraint_equal eq) cs1 cs2
 
+and array_length_equal eq l1 l2 =
+  match (l1, l2) with
+  | ArrayLength_Expr e1, ArrayLength_Expr e2 -> expr_equal eq e1 e2
+  | ArrayLength_Enum (s1, _), ArrayLength_Enum (s2, _) -> String.equal s1 s2
+  | ArrayLength_Enum (_, _), ArrayLength_Expr _
+  | ArrayLength_Expr _, ArrayLength_Enum (_, _) ->
+      false
+
 and type_equal eq t1 t2 =
   t1.desc == t2.desc
   ||
@@ -397,7 +406,7 @@ and type_equal eq t1 t2 =
   | T_Bits (w1, bf1), T_Bits (w2, bf2) ->
       bitwidth_equal eq w1 w2 && bitfields_equal eq bf1 bf2
   | T_Array (l1, t1), T_Array (l2, t2) ->
-      expr_equal eq l1 l2 && type_equal eq t1 t2
+      array_length_equal eq l1 l2 && type_equal eq t1 t2
   | T_Named s1, T_Named s2 -> String.equal s1 s2
   | T_Enum li1, T_Enum li2 ->
       (* TODO: order of fields? *) list_equal String.equal li1 li2
@@ -542,20 +551,45 @@ let list_cross f li1 li2 =
 
 exception FailedConstraintOp
 
+let is_left_increasing = function
+  | MUL | DIV | DIVRM | MOD | SHL | SHR | POW | PLUS | MINUS -> true
+  | AND | BAND | BEQ | BOR | EOR | EQ_OP | GT | GEQ | IMPL | LT | LEQ | NEQ | OR
+  | RDIV ->
+      raise FailedConstraintOp
+
+let is_right_increasing = function
+  | MUL | SHL | SHR | POW | PLUS -> true
+  | DIV | DIVRM | MOD | MINUS -> false
+  | AND | BAND | BEQ | BOR | EOR | EQ_OP | GT | GEQ | IMPL | LT | LEQ | NEQ | OR
+  | RDIV ->
+      raise FailedConstraintOp
+
+let is_right_decreasing = function
+  | MINUS -> true
+  | DIV | DIVRM | MUL | SHL | SHR | POW | PLUS | MOD -> false
+  | AND | BAND | BEQ | BOR | EOR | EQ_OP | GT | GEQ | IMPL | LT | LEQ | NEQ | OR
+  | RDIV ->
+      raise FailedConstraintOp
+
 let constraint_binop op =
+  let righ_inc = is_right_increasing op
+  and righ_dec = is_right_decreasing op
+  and left_inc = is_left_increasing op in
   let do_op c1 c2 =
-    match (c1, c2, op) with
-    | Constraint_Exact e1, Constraint_Exact e2, _ ->
+    match (c1, c2) with
+    | Constraint_Exact e1, Constraint_Exact e2 ->
         Constraint_Exact (binop op e1 e2)
-    | Constraint_Exact e1, Constraint_Range (e21, e22), PLUS ->
+    | Constraint_Exact e1, Constraint_Range (e21, e22) when righ_inc ->
         Constraint_Range (binop op e1 e21, binop op e1 e22)
-    | Constraint_Exact e1, Constraint_Range (e21, e22), MINUS ->
+    | Constraint_Exact e1, Constraint_Range (e21, e22) when righ_dec ->
         Constraint_Range (binop op e1 e22, binop op e1 e21)
-    | Constraint_Range (e11, e12), Constraint_Exact e2, (PLUS | MINUS) ->
+    | Constraint_Range (e11, e12), Constraint_Exact e2 when left_inc ->
         Constraint_Range (binop op e11 e2, binop op e12 e2)
-    | Constraint_Range (e11, e12), Constraint_Range (e21, e22), PLUS ->
+    | Constraint_Range (e11, e12), Constraint_Range (e21, e22)
+      when left_inc && righ_inc ->
         Constraint_Range (binop op e11 e21, binop op e12 e22)
-    | Constraint_Range (e11, e12), Constraint_Range (e21, e22), MINUS ->
+    | Constraint_Range (e11, e12), Constraint_Range (e21, e22)
+      when left_inc && righ_dec ->
         Constraint_Range (binop op e11 e22, binop op e12 e21)
     | _ -> raise_notrace FailedConstraintOp
   in

asllib/Interpreter.ml

@@ -594,23 +594,26 @@ module Make (B : Backend.S) (C : Config) = struct
               let* v' = B.get_index i v in
               let* here = in_values v' ty' in
               and' prev here
-            and i = i + 1 in
-            (i, m)
+            in
+            (i + 1, m)
           in
           List.fold_left fold (0, m_true) tys |> snd
-      | T_Array (e, ty') ->
-          let* v = eval_expr_sef env e in
-          let n =
-            match B.v_to_int v with
-            | Some i -> i
-            | None -> fatal_from loc @@ Error.UnsupportedExpr e
+      | T_Array (index, ty') ->
+          let* length =
+            match index with
+            | ArrayLength_Enum (_, i) -> return i
+            | ArrayLength_Expr e -> (
+                let* v_length = eval_expr_sef env e in
+                match B.v_to_int v_length with
+                | Some i -> return i
+                | None -> fatal_from loc @@ Error.UnsupportedExpr e)
           in
           let rec loop i prev =
-            if i = n then prev
+            if i >= length then prev
             else
               let* v' = B.get_index i v in
               let* here = in_values v' ty' in
-              loop (succ i) (and' prev here)
+              loop (i + 1) (and' prev here)
           in
           loop 0 m_true
       | T_Named _ -> assert false
@@ -1340,21 +1343,18 @@ module Make (B : Backend.S) (C : Config) = struct
           (Error.NotYetImplemented "Base value of string types.")
     | T_Tuple li ->
         List.map (base_value env) li |> sync_list >>= B.create_vector
-    | T_Array (e_length, ty) ->
+    | T_Array (length, ty) ->
         let* v = base_value env ty in
-        let* length =
-          match e_length.desc with
-          | E_Var x when IMap.mem x env.global.static.declared_types ->
-              IMap.find x env.global.static.constants_values
-              |> B.v_of_literal |> return
-          | _ -> eval_expr_sef env e_length
+        let* i_length =
+          match length with
+          | ArrayLength_Enum (_, i) -> return i
+          | ArrayLength_Expr e -> (
+              let* length = eval_expr_sef env e in
+              match B.v_to_int length with
+              | None -> Error.fatal_from t (Error.UnsupportedExpr e)
+              | Some i -> return i)
         in
-        let length =
-          match B.v_to_int length with
-          | None -> Error.fatal_from t (Error.UnsupportedExpr e_length)
-          | Some i -> i
-        in
-        List.init length (Fun.const v) |> B.create_vector
+        List.init i_length (Fun.const v) |> B.create_vector
 
   (* Begin TopLevel *)
   let run_typed_env env (ast : AST.t) (static_env : StaticEnv.env) : B.value m =

asllib/Native.ml

@@ -316,8 +316,18 @@ module NativeBackend = struct
     let round_towards_zero = wrap_real_to_int "RoundTowardsZero" truncate
 
     let primitives =
+      let e_var x = E_Var x |> add_dummy_pos in
+      let eoi i = expr_of_int i in
+      let binop = ASTUtils.binop in
+      let minus_one e = binop MINUS e (eoi 1) in
+      let pow_2 = binop POW (eoi 2) in
+      let neg e = E_Unop (NEG, e) |> add_pos_from e in
       (* [t_bits "N"] is the bitvector type of length [N]. *)
-      let t_bits x = T_Bits (E_Var x |> add_dummy_pos, []) |> add_dummy_pos in
+      let t_bits x = T_Bits (e_var x, []) |> add_dummy_pos in
+      (* [t_int_ctnt e1 e2] is [integer {e1..e2}] *)
+      let t_int_ctnt e1 e2 =
+        T_Int (WellConstrained [ Constraint_Range (e1, e2) ]) |> add_dummy_pos
+      in
       (* [p ~parameters ~args ~returns name f] declares a primtive named [name]
          with body [f], and signature specified by [parameters] [args] and
          [returns]. *)
@@ -329,14 +339,22 @@ module NativeBackend = struct
         ({ name; parameters; args; body; return_type; subprogram_type }, f)
       in
       [
-        p
-          ~parameters:[ ("N", None) ]
-          ~args:[ ("x", t_bits "N") ]
-          ~returns:integer "UInt" uint;
-        p
-          ~parameters:[ ("N", None) ]
-          ~args:[ ("x", t_bits "N") ]
-          ~returns:integer "SInt" sint;
+        (let two_pow_n_minus_one = minus_one (pow_2 (e_var "N")) in
+         let returns = t_int_ctnt (eoi 0) two_pow_n_minus_one in
+         p
+           ~parameters:[ ("N", None) ]
+           ~args:[ ("x", t_bits "N") ]
+           ~returns "UInt" uint);
+        (let two_pow_n_minus_one = pow_2 (minus_one (e_var "N")) in
+         let minus_two_pow_n_minus_one = neg two_pow_n_minus_one
+         and two_pow_n_minus_one_minus_one = minus_one two_pow_n_minus_one in
+         let returns =
+           t_int_ctnt minus_two_pow_n_minus_one two_pow_n_minus_one_minus_one
+         in
+         p
+           ~parameters:[ ("N", None) ]
+           ~args:[ ("x", t_bits "N") ]
+           ~returns "SInt" sint);
         p ~args:[ ("x", integer) ] ~returns:string "DecStr" dec_str;
         p ~args:[ ("x", integer) ] ~returns:string "HexStr" hex_str;
         p ~args:[ ("x", integer) ] ~returns:string "AsciiStr" ascii_str;

asllib/PP.ml

@@ -174,8 +174,10 @@ and pp_ty f t =
         (pp_comma_list pp_print_string)
         enum_ty
   | T_Tuple ty_list -> fprintf f "@[(%a)@]" (pp_comma_list pp_ty) ty_list
-  | T_Array (e, elt_type) ->
+  | T_Array (ArrayLength_Expr e, elt_type) ->
       fprintf f "@[array [%a] of %a@]" pp_expr e pp_ty elt_type
+  | T_Array (ArrayLength_Enum (s, _), elt_type) ->
+      fprintf f "@[array [%s] of %a@]" s pp_ty elt_type
   | T_Record record_ty ->
       fprintf f "@[<hv 2>record {@ %a@;<1 -2>}@]" pp_fields record_ty
   | T_Exception record_ty ->

asllib/Parser.mly

@@ -376,12 +376,16 @@ let ty :=
     | STRING;                                           { T_String    }
     | BIT;                                              { t_bit       }
     | BITS; ~=pared(expr); ~=bitfields_opt;             < T_Bits      >
-    | ENUMERATION; l=braced(tclist(IDENTIFIER));        < T_Enum      >
     | l=plist(ty);                                      < T_Tuple     >
-    | ARRAY; e=bracketed(expr); OF; t=ty;               < T_Array     >
+    | name=IDENTIFIER;                                  < T_Named     >
+    | ARRAY; e=bracketed(expr); OF; t=ty;               { T_Array (ArrayLength_Expr e, t) }
+  )
+
+let ty_decl := ty |
+  annotated (
+    | ENUMERATION; l=braced(tclist(IDENTIFIER));        < T_Enum      >
     | RECORD; l=fields_opt;                             < T_Record    >
     | EXCEPTION; l=fields_opt;                          < T_Exception >
-    | name=IDENTIFIER;                                  < T_Named     >
   )
 
 (* Constructs on ty *)
@@ -568,8 +572,8 @@ let decl ==
         }
 
     | terminated_by(SEMI_COLON,
-      | TYPE; x=IDENTIFIER; OF; t=ty; ~=subtype_opt;  < D_TypeDecl           >
-      | TYPE; x=IDENTIFIER; s=annotated(subtype);     < make_ty_decl_subtype >
+      | TYPE; x=IDENTIFIER; OF; t=ty_decl; ~=subtype_opt; < D_TypeDecl           >
+      | TYPE; x=IDENTIFIER; s=annotated(subtype);         < make_ty_decl_subtype > 
 
       | keyword=storage_keyword; name=ignored_or_identifier;
         ty=ioption(as_ty); EQ; initial_value=some(expr);

asllib/Serialize.ml

@@ -170,8 +170,8 @@ and pp_ty =
     | T_Tuple li ->
         addb f "T_Tuple ";
         pp_list pp_ty f li
-    | T_Array (e, elt_type) ->
-        bprintf f "T_Array (%a, %a)" pp_expr e pp_ty elt_type
+    | T_Array (length, elt_type) ->
+        bprintf f "T_Array (%a, %a)" pp_array_length length pp_ty elt_type
     | T_Record li ->
         addb f "T_Record ";
         pp_id_assoc pp_ty f li
@@ -182,6 +182,10 @@ and pp_ty =
   in
   fun f s -> pp_annotated pp_desc f s
 
+and pp_array_length f = function
+  | ArrayLength_Expr e -> bprintf f "ArrayLength_Expr (%a)" pp_expr e
+  | ArrayLength_Enum (s, i) -> bprintf f "ArrayLength_Enum (%S, %i)" s i
+
 and pp_bitfield f = function
   | BitField_Simple (name, slices) ->
       bprintf f "BitField_Simple (%S, %a)" name pp_slice_list slices

asllib/StaticEnv.ml

@@ -174,6 +174,9 @@ let add_global_storage x ty gdk env =
   }
 
 let add_type x ty env =
+  let () =
+    if false then Format.eprintf "Adding type %s as %a.@." x PP.pp_ty ty
+  in
   {
     env with
     global =