Merge pull request #834 from HadrienRenaud/asl-new-ctcs

[ASL] New Asserted Type Conversions

asllib/AST.mli

@@ -113,7 +113,7 @@ type literal =
 type expr_desc =
   | E_Literal of literal
   | E_Var of identifier
-  | E_CTC of expr * ty
+  | E_ATC of expr * ty  (** Asserted type conversion *)
   | E_Binop of binop * expr * expr
   | E_Unop of unop * expr
   | E_Call of identifier * expr list * (identifier * expr) list

asllib/ASTUtils.ml

@@ -168,7 +168,7 @@ let fold_named_list folder acc list =
 let rec use_e acc e =
   match e.desc with
   | E_Literal _ -> acc
-  | E_CTC (e, ty) -> use_e (use_ty acc ty) e
+  | E_ATC (e, ty) -> use_e (use_ty acc ty) e
   | E_Var x -> ISet.add x acc
   | E_GetArray (e1, e2) | E_Binop (_, e1, e2) -> use_e (use_e acc e2) e1
   | E_Unop (_op, e) -> use_e acc e
@@ -350,8 +350,8 @@ let rec expr_equal eq e1 e2 =
   | E_Literal _, _ | _, E_Literal _ -> false
   | E_Tuple li1, E_Tuple li2 -> list_equal (expr_equal eq) li1 li2
   | E_Tuple _, _ | _, E_Tuple _ -> false
-  | E_CTC (e1, t1), E_CTC (e2, t2) -> expr_equal eq e1 e2 && type_equal eq t1 t2
-  | E_CTC _, _ | _, E_CTC _ -> false
+  | E_ATC (e1, t1), E_ATC (e2, t2) -> expr_equal eq e1 e2 && type_equal eq t1 t2
+  | E_ATC _, _ | _, E_ATC _ -> false
   | E_Unop (o1, e1), E_Unop (o2, e2) -> o1 = o2 && expr_equal eq e1 e2
   | E_Unop _, _ | _, E_Unop _ -> false
   | E_Unknown _, _ | _, E_Unknown _ -> false
@@ -619,7 +619,7 @@ let rec subst_expr substs e =
       E_Record (t, List.map (fun (x, e) -> (x, tr e)) fields)
   | E_Slice (e, slices) -> E_Slice (tr e, slices)
   | E_Tuple es -> E_Tuple (List.map tr es)
-  | E_CTC (e, t) -> E_CTC (tr e, t)
+  | E_ATC (e, t) -> E_ATC (tr e, t)
   | E_Unknown _ -> e.desc
   | E_Unop (op, e) -> E_Unop (op, tr e)
 
@@ -643,7 +643,7 @@ let rec is_simple_expr e =
   | E_Var _ | E_Literal _ | E_Unknown _ -> true
   | E_GetArray (e1, e2) | E_Binop (_, e1, e2) ->
       is_simple_expr e1 && is_simple_expr e2
-  | E_CTC (e, _)
+  | E_ATC (e, _)
   | E_GetFields (e, _)
   | E_GetField (e, _)
   | E_Unop (_, e)
@@ -681,7 +681,7 @@ let rename_locals map_name ast =
     map_desc_st' e @@ function
     | E_Literal _ | E_Unknown _ -> e.desc
     | E_Var x -> E_Var (map_name x)
-    | E_CTC (e', t) -> E_CTC (map_e e', map_t t)
+    | E_ATC (e', t) -> E_ATC (map_e e', map_t t)
     | E_Binop (op, e1, e2) -> E_Binop (op, map_e e1, map_e e2)
     | E_Unop (op, e') -> E_Unop (op, map_e e')
     | E_Call (name, args, nargs) -> E_Call (name, map_es args, map_names nargs)

asllib/Interpreter.ml

@@ -293,8 +293,6 @@ module Make (B : Backend.S) (C : Config) = struct
 
   (* Utils *)
   (* ----- *)
-  let v_true = L_Bool true |> B.v_of_literal
-  let m_true = return v_true
   let v_false = L_Bool false |> B.v_of_literal
   let m_false = return v_false
   let v_zero = L_Int Z.zero |> B.v_of_literal
@@ -373,13 +371,13 @@ module Make (B : Backend.S) (C : Config) = struct
     (* Begin Lit *)
     | E_Literal v -> return_normal (B.v_of_literal v, env) |: SemanticsRule.Lit
     (* End *)
-    (* Begin CTC *)
-    | E_CTC (e1, t) ->
+    (* Begin ATC *)
+    | E_ATC (e1, t) ->
         let** v, new_env = eval_expr env e1 in
         let* b = is_val_of_type e1 env v t in
         (if b then return_normal (v, new_env)
          else fatal_from e1 (Error.MismatchType (B.debug_value v, [ t.desc ])))
-        |: SemanticsRule.CTC
+        |: SemanticsRule.ATC
     (* End *)
     | E_Var x -> (
         match IEnv.find x env with
@@ -552,78 +550,36 @@ module Make (B : Backend.S) (C : Config) = struct
 
   (* Begin ValOfType *)
   and is_val_of_type loc env v ty : bool B.m =
-    let and' prev here = prev >>= B.binop BAND here in
-    let or' prev here = prev >>= B.binop BOR here in
-    let rec in_values v ty =
-      match (Types.get_structure (IEnv.to_static env) ty).desc with
-      | T_Real | T_Bool | T_Enum _ | T_String | T_Int UnConstrained -> m_true
-      | T_Int (UnderConstrained _) ->
-          (* This cannot happen, because:
-             1. Forgetting now about named types, or any kind of compound type,
-                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.
-          *)
-          failwith "Cannot perform a CTC on the under-constrained type."
-      | 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 fold prev = function
-            | Constraint_Exact e ->
-                let* v' = eval_expr_sef env e in
-                let* here = B.binop EQ_OP v v' in
-                or' prev here
-            | Constraint_Range (e1, e2) ->
-                let* v1 = eval_expr_sef env e1 and* v2 = eval_expr_sef env e2 in
-                let* here =
-                  let* c1 = B.binop LEQ v1 v and* c2 = B.binop LEQ v v2 in
-                  B.binop BAND c1 c2
-                in
-                or' prev here
-          in
-          List.fold_left fold m_false constraints
-      | T_Record fields | T_Exception fields ->
-          let fold prev (field_name, field_type) =
-            let* v' = B.get_field field_name v in
-            let* here = in_values v' field_type in
-            and' prev here
-          in
-          List.fold_left fold m_true fields
-      | 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
-              and' prev here
-            in
-            (i + 1, m)
-          in
-          List.fold_left fold (0, m_true) tys |> snd
-      | 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 >= length then prev
-            else
-              let* v' = B.get_index i v in
-              let* here = in_values v' ty' in
-              loop (i + 1) (and' prev here)
-          in
-          loop 0 m_true
-      | T_Named _ -> assert false
-    in
-    choice (in_values v ty) true false
+    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
   (* End *)
 
   (* Evaluation of Left-Hand-Side Expressions *)

asllib/Native.ml

@@ -219,7 +219,7 @@ module NativeBackend = struct
           mismatch_type bv
             [
               T_Bits
-                ( E_CTC
+                ( E_ATC
                     ( E_Var "-" |> add_dummy_pos,
                       T_Int
                         (WellConstrained

asllib/PP.ml

@@ -110,7 +110,7 @@ let rec pp_expr f e =
   match e.desc with
   | E_Literal v -> pp_literal f v
   | E_Var x -> pp_print_string f x
-  | E_CTC (e, ty) -> fprintf f "@[%a@ as %a@]" pp_expr e pp_ty ty
+  | E_ATC (e, ty) -> fprintf f "@[%a@ as %a@]" pp_expr e pp_ty ty
   | E_Binop (b, e1, e2) ->
       fprintf f "(@[<hov 2>%a@ %s %a@])" pp_expr e1 (binop_to_string b) pp_expr
         e2

asllib/Parser.mly

@@ -302,8 +302,8 @@ let make_expr(sub_expr) ==
     | e=sub_expr; DOT; x=IDENTIFIER;                              < E_GetField           >
     | e=sub_expr; DOT; fs=bracketed(nclist(IDENTIFIER));          < E_GetFields          >
     | ~=bracketed(nclist(expr));                                  < E_Concat             >
-    | ~=sub_expr; AS; ~=ty;                                       < E_CTC              >
-    | ~=sub_expr; AS; ~=implicit_t_int;                           < E_CTC              >
+    | ~=sub_expr; AS; ~=ty;                                       < E_ATC              >
+    | ~=sub_expr; AS; ~=implicit_t_int;                           < E_ATC              >
 
     | ~=sub_expr; IN; ~=pattern_set;                              < E_Pattern            >
     | e=sub_expr; IN; m=MASK_LIT;                                 { E_Pattern (e, Pattern_Mask m) }

asllib/Serialize.ml

@@ -98,7 +98,7 @@ let rec pp_expr =
   let pp_desc f = function
     | E_Literal v -> bprintf f "E_Literal (%a)" pp_literal v
     | E_Var x -> bprintf f "E_Var %S" x
-    | E_CTC (e, t) -> bprintf f "E_CTC (%a, %a)" pp_expr e pp_ty t
+    | E_ATC (e, t) -> bprintf f "E_ATC (%a, %a)" pp_expr e pp_ty t
     | E_Binop (op, e1, e2) ->
         bprintf f "E_Binop (%s, %a, %a)" (pp_binop op) pp_expr e1 pp_expr e2
     | E_Unop (op, e) -> bprintf f "E_Unop (%s, %a)" (pp_unop op) pp_expr e

asllib/Typing.ml

@@ -1232,31 +1232,19 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
     (* Begin ELit *)
     | E_Literal v -> (annotate_literal v |> here, e) |: TypingRule.ELit
     (* End *)
-    (* Begin CTC *)
-    | E_CTC (e', ty) ->
+    (* Begin ATC *)
+    | E_ATC (e', ty) ->
         let t, e'' = annotate_expr env e' in
-        (* - If type-checking determines that the expression
-             type-satisfies the required type, then no further
-             check is required.
-           - If the expression only fails to type-satisfy the
-             required type because the domain of its type is
-             not a subset of the domain of the required type,
-             an execution-time check that the expression evaluates
-             to a value in the domain of the required type is
-             required. *)
+        let t_struct = Types.get_structure env t in
         let ty' = annotate_type ~loc env ty in
-        best_effort
-          (ty', E_CTC (e'', ty') |> here)
-          (fun res ->
-            if Types.structural_subtype_satisfies env t ty' then
-              if Types.domain_subtype_satisfies env t ty' then
-                (* disabling the optimization here as long as the type
-                   system is not sound. *)
-                (* (t', e'') *)
-                res
-              else res
-            else conflict e [ ty'.desc ] t)
-        |: TypingRule.CTC
+        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')))
+        |: TypingRule.ATC
     (* End *)
     | E_Var x -> (
         let () = if false then Format.eprintf "Looking at %S.@." x in

asllib/carpenter/ASTEnums.ml

@@ -145,7 +145,7 @@ module Make (C : Config.S) = struct
       let make_unop (op, expr) = E_Unop (op, expr) in
       unops ** exprs |> map make_unop
     and e_ctc =
-      let make_e_ctc (e, s) = E_CTC (e, t_named s) in
+      let make_e_ctc (e, s) = E_ATC (e, t_named s) in
       exprs ** names |> map make_e_ctc
     and e_binops =
       let make_binop (op, (e1, e2)) = E_Binop (op, e1, e2) in

asllib/carpenter/RandomAST.ml

@@ -464,7 +464,7 @@ module Typed (C : Config.S) = struct
       | T_Int _ ->
           Some
             (let+ e' = expr (env, T_Int UnConstrained |> annot, n) in
-             E_CTC (e', ty) |> annot)
+             E_ATC (e', ty) |> annot)
       | T_Named _ when Types.is_singular env ty_anon ->
           Some (expr (env, ty_anon, n - 1))
       | _ -> None