From 7b19876a57d886fad01b7a8c9c4f66952e6046b9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Dac=C3=ADk?= Date: Tue, 18 Feb 2025 10:27:51 +0100 Subject: [PATCH] [Solver] WIP: simplify context and internal error handling --- astral/main.ml | 9 +++++- src/solver/Exceptions.ml | 30 +++++++++++++++++++ src/solver/Exceptions.mli | 22 ++++++++++++++ src/solver/SolverUtils.ml | 3 -- src/solver/context.ml | 5 +--- src/solver/engine.ml | 16 +++++++--- .../location_encoding/LocationBuilder.ml | 6 ++-- src/translation/translation.ml | 13 ++++---- 8 files changed, 83 insertions(+), 21 deletions(-) create mode 100644 src/solver/Exceptions.ml create mode 100644 src/solver/Exceptions.mli delete mode 100644 src/solver/SolverUtils.ml diff --git a/astral/main.ml b/astral/main.ml index bf4bd7a..271702d 100644 --- a/astral/main.ml +++ b/astral/main.ml @@ -2,7 +2,7 @@ * * Author: Tomas Dacik (idacik@fit.vut.cz), 2021 *) -let () = +let run () = Astral.Profiler.add "Start"; let input_file = Astral.Options.parse () in Astral.Debug.init (); (* Debug initialisation needs to be called after options' parsing *) @@ -21,3 +21,10 @@ let () = Reporter.report result; Checker.check result + +let () = + try run () + with + | Astral.Exceptions.InternalError (reason, details) -> + Astral.Exceptions.pretty_internal_error reason details + | Astral.Exceptions.CmdOptionError _ -> () diff --git a/src/solver/Exceptions.ml b/src/solver/Exceptions.ml new file mode 100644 index 0000000..e4fec26 --- /dev/null +++ b/src/solver/Exceptions.ml @@ -0,0 +1,30 @@ +(* Representation of internal exceptions used by solver. + * + * Author: Tomas Dacik (idacik00@fit.vut.cz), 2025 *) + +exception UnknownResult of string * string + +exception UnsupportedFragment of string * string + +exception CmdOptionError of string + +exception InternalError of string * string + +let unsupported_fragment ~reason ?(details="") = + raise @@ UnsupportedFragment (reason, details) + +let unknown_result ~reason ?(details="") = + raise @@ UnknownResult (reason, details) + +let internal_error ~reason ?(details="") = + raise @@ InternalError (reason, details) + + +(** Pretty printers *) +let pretty_internal_error reason details = + Format.eprintf "%s[Internal error]%s %s\n" Colors.red Colors.white reason; + (*if backtrace then begin + Format.eprintf "\nBacktrace:\n%s" + (Printexc.raw_backtrace_to_string stack) + end;*) + if true then Format.fprintf Format.err_formatter "\n%s\n" details diff --git a/src/solver/Exceptions.mli b/src/solver/Exceptions.mli new file mode 100644 index 0000000..fa98861 --- /dev/null +++ b/src/solver/Exceptions.mli @@ -0,0 +1,22 @@ +(* Representation of solver's internal error. + * + * Author: Tomas Dacik (idacik00@fit.vut.cz), 2025 *) + +exception UnsupportedFragment of string * string +(** This exception is raised when unsupported fragment is detected. *) + +exception UnknownResult of string * string + +exception InternalError of string * string +(** This exception represents an internal error. It should not + be catched inside Astral library. *) + +exception CmdOptionError of string + +val unknown_result : reason:string -> ?details:string -> _ + +val unsupported_fragment : reason:string -> ?details:string -> _ + +val internal_error : reason:string -> ?details:string -> _ + +val pretty_internal_error : string -> string -> unit diff --git a/src/solver/SolverUtils.ml b/src/solver/SolverUtils.ml deleted file mode 100644 index 7b997bf..0000000 --- a/src/solver/SolverUtils.ml +++ /dev/null @@ -1,3 +0,0 @@ -exception UnsupportedFragment of string -(** This exception is raised by various functions which detect formula in - unsupported fragmen. *) diff --git a/src/solver/context.ml b/src/solver/context.ml index 1e97624..03c8c34 100644 --- a/src/solver/context.ml +++ b/src/solver/context.ml @@ -34,7 +34,6 @@ type t = { status : status option; model : StackHeapModel.t option; unsat_core : SL.t list option; - reason_unknown : string option; } let init input = { @@ -55,7 +54,6 @@ let init input = { status = None; model = None; unsat_core = None; - reason_unknown = None; } let (let*) f ctx = match ctx.status with @@ -80,12 +78,11 @@ let set_preprocessed input phi vars = {input with phi = phi; vars = vars} let set_size input size = {input with size = Some size} -let set_result status ?(model=None) ?(unsat_core=None) ?(reason=None) input = +let set_result status ?model ?unsat_core input = {input with status = Some status; model = model; unsat_core = unsat_core; - reason_unknown = reason; } diff --git a/src/solver/engine.ml b/src/solver/engine.ml index e6b9d0d..c8c9f52 100644 --- a/src/solver/engine.ml +++ b/src/solver/engine.ml @@ -23,15 +23,14 @@ let debug_info input = match SL.classify_fragment input.phi with | Positive -> Logger.debug "Solving as positive formula\n" | Arbitrary -> Logger.debug "Solving as arbitrary formula\n" -let solve (raw_input : ParserContext.t) = +let solve (input : Context.t) = SID.init (); - let input = Context.init raw_input in let input = Preprocessor.first_phase input in SID.preprocess_user_definitions PredicatePreprocessing.normalise; let sl_graph = SL_graph.compute input.phi in if SL_graph.has_contradiction sl_graph then - Context.set_result `Unsat ~unsat_core:(Some []) input + Context.set_result `Unsat ~unsat_core:[] input else match FragmentChecker.check input with | Error reason -> Context.set_result (`Unknown reason) input | Ok () -> @@ -71,4 +70,13 @@ let solve (raw_input : ParserContext.t) = let res' = Context.apply_model_adapter res in (match res'.model with None -> () | Some sh -> Debug.model sh); res' - else Context.set_result (`Unknown "dry run") ~reason:(Some "dry run") input + else Context.set_result (`Unknown "dry run") input + +(* TODO: Do not return just input in case of exception. *) +let solve input = + let ctx = Context.init input in + try solve ctx with + | Exceptions.UnknownResult (reason, _) -> + Context.set_result (`Unknown reason) ctx + | Exceptions.UnsupportedFragment (reason, _) -> + Context.set_result (`Unknown ("Unsupported fragment" ^ reason)) ctx diff --git a/src/translation/location_encoding/LocationBuilder.ml b/src/translation/location_encoding/LocationBuilder.ml index 6217323..e91b551 100644 --- a/src/translation/location_encoding/LocationBuilder.ml +++ b/src/translation/location_encoding/LocationBuilder.ml @@ -27,9 +27,9 @@ module Make (Locations : LOCATIONS_BASE) = struct | Some (_, mapper) -> SMT.Array.mk_select mapper locs.null | None ->*) locs.null - let internal_error self msg_prefix = - let msg = Format.asprintf "%s in location encoding:\n%s" msg_prefix (show self) - in Utils.internal_error msg + let internal_error self reason = + let details = Format.asprintf "Location encoding:\n%s" (show self) in + Exceptions.internal_error ~reason ~details let get_encoding locs sort = try Sort.Map.find sort locs.sort_encoding diff --git a/src/translation/translation.ml b/src/translation/translation.ml index 810d305..452c8e8 100644 --- a/src/translation/translation.ml +++ b/src/translation/translation.ml @@ -353,7 +353,7 @@ module Make (Encoding : Translation_sig.ENCODING) (Backend : Backend_sig.BACKEND if ctx.can_skolemise then translate_septraction_skolemised ctx domain witness_heap phi psi1 psi2 - else raise @@ SolverUtils.UnsupportedFragment "magic wand/negative septraction" + else Exceptions.unsupported_fragment ~reason:"magic wand/negative septraction" ~details:"" and translate_septraction_skolemised ctx domain witness_heap phi psi1 psi2 = let fp1 = formula_footprint ctx psi1 in @@ -668,18 +668,19 @@ let translate_phi (ctx : Context.t) ssl_phi = | SMT_Sat (Some (smt_model, backend_model)) -> let smt_model = SetEncoding.rewrite_back translated1 smt_model in let _ = Debug.smt_model smt_model in - let sh = translate_model ctx smt_model in - Input.set_result `Sat ~model:(Some sh) input + let model = translate_model ctx smt_model in + Input.set_result `Sat ~model input (* TODO: unsat cores *) - | SMT_Unsat unsat_core -> Input.set_result `Unsat ~unsat_core:(Some []) input + | SMT_Unsat unsat_core -> Input.set_result `Unsat ~unsat_core:[] input (* TODO: remove duplicit reason *) - | SMT_Unknown reason -> Input.set_result (`Unknown reason) ~reason:(Some reason) input + | SMT_Unknown reason -> Input.set_result (`Unknown reason) input - let solve input = + (*let solve input = try solve input with SolverUtils.UnsupportedFragment str -> let reason = "unsupported SL fragment: " ^ str in Input.set_result (`Unknown reason) ~reason:(Some reason) input + *) end