Expose details of failed lexp bounds checks

Allows ASL-to-Sail translation to automatically patch lexp bounds check
errors.

4 files changed, 25 insertions, 15 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index e318a423..ac5da907 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -438,8 +438,6 @@ let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
 let nc_lt n1 n2 = NC_aux (NC_bounded_lt (n1, n2), Parse_ast.Unknown)
 let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown)
 let nc_gt n1 n2 = NC_aux (NC_bounded_gt (n1, n2), Parse_ast.Unknown)
-let nc_lt n1 n2 = nc_lteq (nsum n1 (nint 1)) n2
-let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nint 1))
 let nc_var kid = mk_nc (NC_var kid)
 let nc_true = mk_nc NC_true
 let nc_false = mk_nc NC_false
diff --git a/src/type_check.ml b/src/type_check.ml
index 3b047040..f11b955a 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -102,6 +102,7 @@ type type_error =
   | Err_no_casts of unit exp * typ * typ * type_error * type_error list
   | Err_no_overloading of id * (id * type_error) list
   | Err_unresolved_quants of id * quant_item list * (mut * typ) Bindings.t * n_constraint list
+  | Err_lexp_bounds of n_constraint * (mut * typ) Bindings.t * n_constraint list
   | Err_subtype of typ * typ * n_constraint list * Ast.l KBindings.t
   | Err_no_num_ident of id
   | Err_other of string
@@ -3642,15 +3643,20 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
           let inferred_exp2 = infer_exp env exp2 in
           let nexp1, env = bind_numeric l (typ_of inferred_exp1) env in
           let nexp2, env = bind_numeric l (typ_of inferred_exp2) env in
-          begin match ord with
-          | Ord_aux (Ord_inc, _) when !opt_no_lexp_bounds_check || prove __POS__ env (nc_lteq nexp1 nexp2) ->
-             let len = nexp_simp (nsum (nminus nexp2 nexp1) (nint 1)) in
-             annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (bitvector_typ len ord)
-          | Ord_aux (Ord_dec, _) when !opt_no_lexp_bounds_check || prove __POS__ env (nc_gteq nexp1 nexp2) ->
-             let len = nexp_simp (nsum (nminus nexp1 nexp2) (nint 1)) in
-             annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (bitvector_typ len ord)
-          | _ -> typ_error env l ("Could not infer length of vector slice assignment " ^ string_of_lexp lexp)
-          end
+          let (len, check) = match ord with
+            | Ord_aux (Ord_inc, _) ->
+               (nexp_simp (nsum (nminus nexp2 nexp1) (nint 1)),
+                nc_lteq nexp1 nexp2)
+            | Ord_aux (Ord_dec, _) ->
+               (nexp_simp (nsum (nminus nexp1 nexp2) (nint 1)),
+                nc_gteq nexp1 nexp2)
+            | Ord_aux (Ord_var _, _) ->
+               typ_error env l "Slice assignment to bitvector with variable indexing order unsupported"
+          in
+          if !opt_no_lexp_bounds_check || prove __POS__ env check then
+            annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (bitvector_typ len ord)
+          else
+            typ_raise env l (Err_lexp_bounds (check, Env.get_locals env, Env.get_constraints env))
        | _ -> typ_error env l "Cannot assign slice of non vector type"
      end
   | LEXP_vector (v_lexp, exp) ->
@@ -3662,18 +3668,20 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
             when Id.compare id (mk_id "vector") = 0 ->
           let inferred_exp = infer_exp env exp in
           let nexp, env = bind_numeric l (typ_of inferred_exp) env in
-          if !opt_no_lexp_bounds_check || prove __POS__ env (nc_and (nc_lteq (nint 0) nexp) (nc_lteq nexp (nexp_simp (nminus len (nint 1))))) then
+          let bounds_check = nc_and (nc_lteq (nint 0) nexp) (nc_lt nexp len) in
+          if !opt_no_lexp_bounds_check || prove __POS__ env bounds_check then
             annot_lexp (LEXP_vector (inferred_v_lexp, inferred_exp)) elem_typ
           else
-            typ_error env l ("Vector assignment not provably in bounds " ^ string_of_lexp lexp)
+            typ_raise env l (Err_lexp_bounds (bounds_check, Env.get_locals env, Env.get_constraints env))
        | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_order ord, _)])
             when Id.compare id (mk_id "bitvector") = 0 ->
           let inferred_exp = infer_exp env exp in
           let nexp, env = bind_numeric l (typ_of inferred_exp) env in
-          if !opt_no_lexp_bounds_check || prove __POS__ env (nc_and (nc_lteq (nint 0) nexp) (nc_lteq nexp (nexp_simp (nminus len (nint 1))))) then
+          let bounds_check = nc_and (nc_lteq (nint 0) nexp) (nc_lt nexp len) in
+          if !opt_no_lexp_bounds_check || prove __POS__ env bounds_check then
             annot_lexp (LEXP_vector (inferred_v_lexp, inferred_exp)) bit_typ
           else
-            typ_error env l ("Vector assignment not provably in bounds " ^ string_of_lexp lexp)
+            typ_raise env l (Err_lexp_bounds (bounds_check, Env.get_locals env, Env.get_constraints env))
        | Typ_id id when !opt_new_bitfields ->
           begin match exp with
           | E_aux (E_id field, _) ->
diff --git a/src/type_check.mli b/src/type_check.mli
index 76b38557..fba5575a 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -89,6 +89,7 @@ type type_error =
   | Err_no_casts of unit exp * typ * typ * type_error * type_error list
   | Err_no_overloading of id * (id * type_error) list
   | Err_unresolved_quants of id * quant_item list * (mut * typ) Bindings.t * n_constraint list
+  | Err_lexp_bounds of n_constraint * (mut * typ) Bindings.t * n_constraint list
   | Err_subtype of typ * typ * n_constraint list * Ast.l KBindings.t
   | Err_no_num_ident of id
   | Err_other of string
diff --git a/src/type_error.ml b/src/type_error.ml
index 6205302e..1ac771bf 100644
--- a/src/type_error.ml
+++ b/src/type_error.ml
@@ -120,6 +120,9 @@ let message_of_type_error =
        Seq [Line ("Could not resolve quantifiers for " ^ string_of_id id);
             Line (bullet ^ " " ^ Util.string_of_list ("\n" ^ bullet ^ " ") string_of_quant_item quants)]
 
+    | Err_lexp_bounds (check, locals, ncs) ->
+       Line ("Bounds check failed for l-expression: " ^ string_of_n_constraint check)
+
     | Err_subtype (typ1, typ2, _, vars) ->
        let vars = KBindings.bindings vars in
        let vars = List.filter (fun (v, _) -> KidSet.mem v (KidSet.union (tyvars_of_typ typ1) (tyvars_of_typ typ2))) vars in