Skip to content

Commit

Permalink
Remove Util.failwith (#872)
Browse files Browse the repository at this point in the history 
Using specific exceptions to unsupported features and unifying use of Fmt.failwith
  • Loading branch information
@Stevendeo
Stevendeo authored Oct 12, 2023
1 parent c85766a commit 21479bf
Show file tree
Hide file tree
Showing 6 changed files with 37 additions and 43 deletions.
4 changes: 2 additions & 2 deletions src/bin/common/solving_loop.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -530,7 +530,7 @@ let main () =
| Simple name -> name
| _ ->
let loc = DStd.Loc.loc file_loc loc in
Util.failwith "%a: internal error: goal name should be simple"
Fmt.failwith "%a: internal error: goal name should be simple"
DStd.Loc.fmt loc
in
let contents =
Expand All @@ -539,7 +539,7 @@ let main () =
| `Solve ([], [t]) -> `Goal t
| _ ->
let loc = DStd.Loc.loc file_loc loc in
Util.failwith "%a: internal error: unknown statement"
Fmt.failwith "%a: internal error: unknown statement"
DStd.Loc.fmt loc
in
let stmt = { Typer_Pipe.id; contents; loc ; attrs } in
Expand Down
64 changes: 31 additions & 33 deletions src/lib/frontend/d_cnf.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,11 @@ module DT = DE.Ty
module Id = DStd.Id
module B = DStd.Builtin

let unsupported msg =
Fmt.kstr
(fun str -> Errors.(run_error (Unsupported_feature str)))
msg

module Shared = struct
(* Shared constants to avoid allocations*)

Expand All @@ -62,7 +67,7 @@ let get_basename = function
| DStd.Path.Local { name; }
| Absolute { name; path = []; } -> name
| Absolute { name; path; } ->
Util.failwith
Fmt.failwith
"Expected an empty path to the basename: \"%s\" but got: [%a]."
name (fun fmt l ->
match l with
Expand Down Expand Up @@ -91,7 +96,7 @@ module Cache = struct
match find_sy ind with
| Sy.Var v -> v
| sym ->
Util.failwith
Fmt.failwith
"Internal error: Expected to find a variable symbol,\
instead found (%a)"
Sy.print sym
Expand Down Expand Up @@ -477,7 +482,7 @@ let rec dty_to_ty ?(update = false) ?(is_var = false) dty =
if update then
Cache.store_tyvl ~is_var tyvl;
aux ty
| _ -> Util.failwith "Unsupported Type %a" DE.Ty.print dty
| _ -> unsupported "Type %a" DE.Ty.print dty

and handle_ty_app ?(update = false) ty_c l =
(* Applies the substitutions in [tysubsts] to each encountered type
Expand Down Expand Up @@ -550,7 +555,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
let pty = dty_to_ty id_ty in
(pn, pty) :: acc
| _ ->
Util.failwith
Fmt.failwith
"Unexpected null label for some field of the record type %a"
DE.Ty.Const.print ty_c

Expand Down Expand Up @@ -647,7 +652,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
let pty = dty_to_ty id_ty in
(pn, pty) :: acc
| _ ->
Util.failwith
Fmt.failwith
"Unexpected null label for some field of the record type %a"
DE.Ty.Const.print ty_c
) [] dstrs
Expand Down Expand Up @@ -766,7 +771,7 @@ let handle_patt_var name (DE.{ term_descr; _ } as term) =
v, n, ty

| _ ->
Util.failwith
Fmt.failwith
"Expected a variable in a case match but got %a"
DE.Term.print term

Expand All @@ -791,7 +796,7 @@ let mk_pattern DE.{ term_descr; _ } =
| _ -> assert false
) [] dstrs
| _ ->
Util.failwith
Fmt.failwith
"Expected a constructor for an algebraic data type but got\
something else for the definition of: %a"
DE.Ty.Const.print adt
Expand Down Expand Up @@ -826,8 +831,7 @@ let mk_pattern DE.{ term_descr; _ } =
let arith_ty = function
| `Int -> Ty.Tint
| `Real -> Ty.Treal
| `Rat ->
Util.failwith "rationals are not currently supported"
| `Rat -> unsupported "rationals"

(* Parse a semantic bound [x `b` y] and returns a tuple [(sort, lb, ub)] where:
Expand All @@ -850,7 +854,7 @@ let parse_semantic_bound ?(loc = Loc.dummy) ~var b x y =
| B.Gt t -> `Gt, t
| B.Geq t -> `Ge, t
| _ ->
Util.failwith
Fmt.failwith
"%aInternal error: invalid semantic bound"
Loc.report loc
in
Expand All @@ -861,7 +865,7 @@ let parse_semantic_bound ?(loc = Loc.dummy) ~var b x y =
Sy.ValBnd (Numbers.Q.from_string s)
| Var v -> Sy.VarBnd (Cache.find_var v)
| _ ->
Util.failwith
Fmt.failwith
"%aInternal error: invalid semantic bound"
Loc.report loc
in
Expand Down Expand Up @@ -966,8 +970,7 @@ let rec mk_expr
let sy = Sy.Op (Sy.Constr (Hstring.make name)) in
E.mk_term sy [] ty

| _ ->
Util.failwith "Unsupported constant term %a" DE.Term.print term
| _ -> unsupported "Constant term %a" DE.Term.print term
end

| Var ({ id_ty; _ } as ty_v) ->
Expand Down Expand Up @@ -1015,13 +1018,13 @@ let rec mk_expr
in
E.mk_term sy [e] ty
| _ ->
Util.failwith
Fmt.failwith
"Adt Destructor error: Can't find %dth field of %dth \
case of the type %a."
field case DE.Ty.Const.print adt
end
| None | Some Abstract ->
Util.failwith
Fmt.failwith
"Can't find the adt %a to which the destructor %a belongs"
DE.Ty.Const.print adt DE.Term.print app_term
end
Expand Down Expand Up @@ -1069,7 +1072,7 @@ let rec mk_expr
| [] -> None
| [ var, value ] -> Some (var, value)
| _ ->
Util.failwith
Fmt.failwith
"%asemantic trigger should have at most one bound variable"
Loc.report loc
in
Expand All @@ -1088,7 +1091,7 @@ let rec mk_expr
match E.type_info t with
| Tbitv m ->
if m <= i then
Util.failwith
Fmt.failwith
"%alength of bitvector extraction exceeds the length\
of its argument."
Loc.report loc
Expand Down Expand Up @@ -1347,7 +1350,7 @@ let rec mk_expr
let l = List.map (fun t -> aux_mk_expr t) args in
E.mk_term (Sy.Op Sy.Record) l ty
| _ ->
Util.failwith
Fmt.failwith
"Constructor error: %a does not belong to a record nor an\
algebraic data type"
DE.Term.print app_term
Expand All @@ -1356,9 +1359,7 @@ let rec mk_expr
| B.Coercion, [ x ] ->
begin match DT.view (DE.Term.ty x), DT.view term_ty with
| `Int, `Real -> op Real_of_int
| _ ->
Util.failwith "Unsupported coercion: %a"
DE.Term.print term
| _ -> unsupported "coercion: %a" DE.Term.print term
end
| Float, _ -> op Float
| Integer_round, _ -> op Integer_round
Expand All @@ -1379,9 +1380,7 @@ let rec mk_expr
| Not_theory_constant, _ -> op Not_theory_constant
| Is_theory_constant, _ -> op Is_theory_constant
| Linear_dependency, _ -> op Linear_dependency

| _, _ ->
Util.failwith "Unsupported Application Term %a" DE.Term.print term
| _, _ -> unsupported "Application Term %a" DE.Term.print term
end

| Match (t, pats) ->
Expand Down Expand Up @@ -1494,8 +1493,7 @@ let rec mk_expr
end
in
mk name loc binders triggers qbody ~toplevel ~decl_kind

| _ -> Util.failwith "Unsupported Term %a" DE.Term.print term
| _ -> unsupported "Term %a" DE.Term.print term
in
match DStd.Tag.get root_tags DE.Tags.named with
| Some s ->
Expand All @@ -1509,7 +1507,7 @@ let rec mk_expr
match destruct_app t with
| Some (cst, args) -> cst, args
| None ->
Util.failwith
Fmt.failwith
"invalid semantic trigger: %a"
DE.Term.print t
in
Expand All @@ -1526,7 +1524,7 @@ let rec mk_expr
let e2 = aux_mk_expr y in
E.mk_term sy [e2] Ty.Tbool
| _ ->
Util.failwith
Fmt.failwith
"%aMaps_to: expected a variable but got: %a"
Loc.report loc DE.Term.print x
end
Expand Down Expand Up @@ -1570,12 +1568,12 @@ let rec mk_expr
in
E.mk_term (Sy.mk_in lb ub) [aux_mk_expr main_expr] Ty.Tbool
| _ ->
Util.failwith "%aInvalid semantic trigger: %a"
Fmt.failwith "%aInvalid semantic trigger: %a"
Loc.report loc DE.Term.print t
end

| _ ->
Util.failwith "%aInvalid semantic trigger: %a"
Fmt.failwith "%aInvalid semantic trigger: %a"
Loc.report loc DE.Term.print t

in aux_mk_expr ~toplevel dt
Expand Down Expand Up @@ -1867,7 +1865,7 @@ let make dloc_file acc stmt =
let name = match name.name with
| Simple name -> name
| _ ->
Util.failwith
Fmt.failwith
"Internal error: invalid theory extension: %a"
print name
in
Expand All @@ -1879,7 +1877,7 @@ let make dloc_file acc stmt =
Errors.typing_error (ThExtError name) aloc
end
| _ ->
Util.failwith
Fmt.failwith
"Internal error: invalid base theory name: %a"
print extends
in
Expand All @@ -1890,7 +1888,7 @@ let make dloc_file acc stmt =
| [] -> None
| [name, extends] -> Some (name, extends)
| _ ->
Util.failwith
Fmt.failwith
"%a: Internal error: multiple theories."
DStd.Loc.fmt dloc
in
Expand Down
2 changes: 1 addition & 1 deletion src/lib/reasoners/records.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -257,7 +257,7 @@ module Shostak (X : ALIEN) = struct
let record = is_mine (Record (flds, tyr)) in
record, (left_abs_xe2, record) :: acc
| ty ->
Util.failwith
Fmt.failwith
"Not a record type: `%a" Ty.print_full ty
in
let abs_access = normalize (Access (field, embed abs_right_xe, ty)) in
Expand Down
6 changes: 3 additions & 3 deletions src/lib/structures/expr.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -704,12 +704,12 @@ let print_list fmt = print_list_sep "," fmt
let lit_view t =
let { f; xs; ty; _ } = t in
if ty != Ty.Tbool then
Util.failwith "Calling lit_view on a non boolean expression %a"
Fmt.failwith "Calling lit_view on a non boolean expression %a"
print t
else
match f with
| Sy.Form _ ->
Util.failwith "Calling lit_view on a formula %a" print t
Fmt.failwith "Calling lit_view on a formula %a" print t
| Sy.Lit lit ->
begin match lit, xs with
| (Sy.L_eq | Sy.L_neg_eq), ([] | [_]) -> assert false
Expand All @@ -726,7 +726,7 @@ let lit_view t =
let form_view t =
let { f; xs; bind; _ } = t in
if t.ty != Ty.Tbool then
Util.failwith "Term %a is not a formula" print t
Fmt.failwith "Term %a is not a formula" print t
else
match f, xs, bind with
| Sy.Form (Sy.F_Unit _), [a;b], _ -> Unit (a, b)
Expand Down
2 changes: 0 additions & 2 deletions src/lib/util/util.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,5 @@ let rec print_list_pp ~sep ~pp fmt = function
Format.fprintf fmt "%a %a" pp x sep ();
print_list_pp ~sep ~pp fmt l

let failwith msg = Format.kasprintf failwith msg

let internal_error msg =
Format.kasprintf (fun s -> raise (Internal_error s)) msg
2 changes: 0 additions & 2 deletions src/lib/util/util.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,6 +118,4 @@ val print_list_pp:
pp:(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a list -> unit

val failwith: ('a, Format.formatter, unit, 'b) format4 -> 'a

val internal_error : ('a, Format.formatter, unit, 'b) format4 -> 'a

0 comments on commit 21479bf

Please sign in to comment.