From affa45c1150c1fcefff3759fc94590cece84b65b Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Fri, 3 May 2024 17:06:33 +0200 Subject: [PATCH 1/4] Unify traces between interpreter and runtime This is a first step into unifying trace handling. This patch only affects the interpreter, by delegating trace recording to the already existing runtime functions. At end of interpretation, it recovers the registered trace from the runtime, and prints it. NOTE: there are some limitations due to this approach, as runtime values going through this interface have to be converted to the "runtime embedded" type. In particular, functions can no longer be printed (which makes full sense if we want it to happen in the same way in compiled code) ; some information, like types, is lost, but it didn't appear to be used. Also, a specific printer had to be added for runtime values (but it's very simple so that shouldn't be a problem). @denismerigoux I'd like your input on how well this goes for your use-cases. Further work should probably be cleanup and unification of the runtime logging interfaces ; there is already code for re-structuring the traces, printing to JSON, etc. which could be common to runtime and interpreter. --- compiler/shared_ast/interpreter.ml | 143 ++++++++++++++++++++----- tests/scope/good/scope_call3.catala_en | 10 +- 2 files changed, 120 insertions(+), 33 deletions(-) diff --git a/compiler/shared_ast/interpreter.ml b/compiler/shared_ast/interpreter.ml index 0c1a2ccc..369657e3 100644 --- a/compiler/shared_ast/interpreter.ml +++ b/compiler/shared_ast/interpreter.ml @@ -34,30 +34,88 @@ let is_empty_error : type a. (a, 'm) gexpr -> bool = let indent_str = ref "" (** {1 Evaluation} *) -let print_log lang entry infos pos e = - if Global.options.trace then - match entry with - | VarDef _ -> - Message.log "%s%a %a: @{%s@}" !indent_str Print.log_entry entry - Print.uid_list infos - (Message.unformat (fun ppf -> - (if Global.options.debug then Print.expr ~debug:true () - else Print.UserFacing.expr lang) - ppf e)) - | PosRecordIfTrueBool -> ( - match pos <> Pos.no_pos, Mark.remove e with - | true, ELit (LBool true) -> - Message.log "%s@[%a@{Definition applied@}:@,%a@]" !indent_str - Print.log_entry entry Pos.format_loc_text pos - | _ -> ()) - | BeginCall -> - Message.log "%s%a %a" !indent_str Print.log_entry entry Print.uid_list - infos; - indent_str := !indent_str ^ " " - | EndCall -> - indent_str := String.sub !indent_str 0 (String.length !indent_str - 2); - Message.log "%s%a %a" !indent_str Print.log_entry entry Print.uid_list - infos + +let rec format_runtime_value lang ppf = function + | Runtime.Unit -> Print.UserFacing.unit lang ppf () + | Runtime.Bool b -> Print.UserFacing.bool lang ppf b + | Runtime.Money m -> Print.UserFacing.money lang ppf m + | Runtime.Integer i -> Print.UserFacing.integer lang ppf i + | Runtime.Decimal d -> Print.UserFacing.decimal lang ppf d + | Runtime.Date t -> Print.UserFacing.date lang ppf t + | Runtime.Duration dt -> Print.UserFacing.duration lang ppf dt + | Runtime.Enum (name, (constr, v)) -> + Format.fprintf ppf "@[%s.%s@ (%a)@]" name constr + (format_runtime_value lang) + v + | Runtime.Struct (name, fields) -> + Format.fprintf ppf "@[%s {@ %a@;<1 -2>}@]" name + (Format.pp_print_list ~pp_sep:Format.pp_print_space (fun ppf (fld, v) -> + Format.fprintf ppf "@[-- %s:@ %a@]" fld + (format_runtime_value lang) + v)) + fields + | Runtime.Array elts -> + Format.fprintf ppf "@[[@,@[%a@]@;<0 -2>]@]" + (Format.pp_print_list + ~pp_sep:(fun ppf () -> Format.fprintf ppf ";@ ") + (format_runtime_value lang)) + (Array.to_list elts) + | Runtime.Unembeddable -> Format.pp_print_string ppf "" + +let print_log lang entry = + let pp_infos = + Format.( + pp_print_list + ~pp_sep:(fun ppf () -> Format.fprintf ppf ".@,") + pp_print_string) + in + match entry with + | Runtime.BeginCall infos -> + Message.log "%s%a %a" !indent_str Print.log_entry BeginCall pp_infos infos; + indent_str := !indent_str ^ " " + | Runtime.EndCall infos -> + indent_str := String.sub !indent_str 0 (String.length !indent_str - 2); + Message.log "%s%a %a" !indent_str Print.log_entry EndCall pp_infos infos + | Runtime.VariableDefinition (infos, io, value) -> + Message.log "%s%a %a: @{%s@}" !indent_str Print.log_entry + (VarDef + { + log_typ = TAny; + log_io_input = io.Runtime.io_input; + log_io_output = io.Runtime.io_output; + }) + pp_infos infos + (Message.unformat (fun ppf -> format_runtime_value lang ppf value)) + | Runtime.DecisionTaken rtpos -> + let pos = Expr.runtime_to_pos rtpos in + Message.log "%s@[%a@{Definition applied@}:@,%a@]" !indent_str + Print.log_entry PosRecordIfTrueBool Pos.format_loc_text pos + +let rec value_to_runtime_embedded = function + | ELit LUnit -> Runtime.Unit + | ELit (LBool b) -> Runtime.Bool b + | ELit (LMoney m) -> Runtime.Money m + | ELit (LInt i) -> Runtime.Integer i + | ELit (LRat r) -> Runtime.Decimal r + | ELit (LDate d) -> Runtime.Date d + | ELit (LDuration dt) -> Runtime.Duration dt + | EInj { name; cons; e } -> + Runtime.Enum + ( EnumName.to_string name, + ( EnumConstructor.to_string cons, + value_to_runtime_embedded (Mark.remove e) ) ) + | EStruct { name; fields } -> + Runtime.Struct + ( StructName.to_string name, + List.map + (fun (f, e) -> + StructField.to_string f, value_to_runtime_embedded (Mark.remove e)) + (StructField.Map.bindings fields) ) + | EArray el -> + Runtime.Array + (Array.of_list + (List.map (fun e -> value_to_runtime_embedded (Mark.remove e)) el)) + | _ -> Runtime.Unembeddable (* Todo: this should be handled early when resolving overloads. Here we have proper structural equality, but the OCaml backend for example uses the @@ -147,9 +205,22 @@ let rec evaluate_operator match op, args with | Length, [(EArray es, _)] -> ELit (LInt (Runtime.integer_of_int (List.length es))) - | Log (entry, infos), [e'] -> - print_log lang entry infos pos e'; - Mark.remove e' + | Log (entry, infos), [(e, _)] when Global.options.trace -> ( + let rtinfos = List.map Uid.MarkedString.to_string infos in + match entry with + | BeginCall -> Runtime.log_begin_call rtinfos e + | EndCall -> Runtime.log_end_call rtinfos e + | PosRecordIfTrueBool -> + (match e with + | ELit (LBool b) -> + Runtime.log_decision_taken (Expr.pos_to_runtime pos) b |> ignore + | _ -> ()); + e + | VarDef def -> + Runtime.log_variable_definition rtinfos + { Runtime.io_input = def.log_io_input; io_output = def.log_io_output } + value_to_runtime_embedded e) + | Log _, [(e', _)] -> e' | (FromClosureEnv | ToClosureEnv), [e'] -> (* [FromClosureEnv] and [ToClosureEnv] are just there to bypass the need for existential types when typing code after closure conversion. There are @@ -840,6 +911,22 @@ and partially_evaluate_expr_for_assertion_failure_message : Mark.get e ) | _ -> evaluate_expr ctx lang e +let evaluate_expr_trace : + type d e. + decl_ctx -> + Global.backend_lang -> + ((d, e, yes) interpr_kind, 't) gexpr -> + ((d, e, yes) interpr_kind, 't) gexpr = + fun ctx lang e -> + Fun.protect + (fun () -> evaluate_expr ctx lang e) + ~finally:(fun () -> + if Global.options.trace then + let trace = Runtime.retrieve_log () in + List.iter (print_log lang) trace + (* TODO: [Runtime.pp_events ~is_first_call:true Format.err_formatter + (Runtime.EventParser.parse_raw_events trace)] fais here, check why *)) + let evaluate_expr_safe : type d e. decl_ctx -> @@ -847,7 +934,7 @@ let evaluate_expr_safe : ((d, e, yes) interpr_kind, 't) gexpr -> ((d, e, yes) interpr_kind, 't) gexpr = fun ctx lang e -> - try evaluate_expr ctx lang e + try evaluate_expr_trace ctx lang e with Runtime.Error (err, rpos) -> Message.error ~extra_pos:(List.map (fun rp -> "", Expr.runtime_to_pos rp) rpos) diff --git a/tests/scope/good/scope_call3.catala_en b/tests/scope/good/scope_call3.catala_en index c43a290c..42bd9798 100644 --- a/tests/scope/good/scope_call3.catala_en +++ b/tests/scope/good/scope_call3.catala_en @@ -44,7 +44,7 @@ $ catala Interpret -t -s HousingComputation --debug [DEBUG] Translating to default calculus... [DEBUG] Typechecking again... [DEBUG] Starting interpretation... -[LOG] ≔ HousingComputation.f: λ (x_67: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨(let result_68 : RentComputation = (#{→ RentComputation.direct} (λ (RentComputation_in_69: RentComputation_in) → let g_70 : integer → integer = #{≔ RentComputation.g} (λ (x1_71: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_71 +! 1⟩⟩ | false ⊢ ∅ ⟩) in let f_72 : integer → integer = #{≔ RentComputation.f} (λ (x1_73: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} g_70) #{≔ RentComputation.g.input0} (x1_73 +! 1)⟩⟩ | false ⊢ ∅ ⟩) in { RentComputation f = f_72; })) #{≔ RentComputation.direct.input} {RentComputation_in} in let result1_74 : RentComputation = { RentComputation f = λ (param0_75: integer) → #{← RentComputation.f} #{≔ RentComputation.f.output} (#{→ RentComputation.f} result_68.f) #{≔ RentComputation.f.input0} param0_75; } in #{← RentComputation.direct} #{≔ RentComputation.direct.output} if #{☛ RentComputation.direct.output} true then result1_74 else result1_74).f x_67⟩⟩ | false ⊢ ∅ ⟩ +[LOG] ≔ HousingComputation.f: [LOG] ☛ Definition applied: ─➤ tests/scope/good/scope_call3.catala_en:8.14-8.20: │ @@ -58,15 +58,15 @@ $ catala Interpret -t -s HousingComputation --debug 7 │ definition f of x equals (output of RentComputation).f of x │ ‾ [LOG] → RentComputation.direct -[LOG] ≔ RentComputation.direct.input: {RentComputation_in} -[LOG] ≔ RentComputation.g: λ (x_76: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x_76 +! 1⟩⟩ | false ⊢ ∅ ⟩ -[LOG] ≔ RentComputation.f: λ (x_77: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} (λ (x1_78: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_78 +! 1⟩⟩ | false ⊢ ∅ ⟩)) #{≔ RentComputation.g.input0} (x_77 +! 1)⟩⟩ | false ⊢ ∅ ⟩ +[LOG] ≔ RentComputation.direct.input: RentComputation_in { } +[LOG] ≔ RentComputation.g: +[LOG] ≔ RentComputation.f: [LOG] ☛ Definition applied: ─➤ tests/scope/good/scope_call3.catala_en:7.29-7.54: │ 7 │ definition f of x equals (output of RentComputation).f of x │ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾ -[LOG] ≔ RentComputation.direct.output: { RentComputation f = λ (param0_79: integer) → #{← RentComputation.f} #{≔ RentComputation.f.output} (#{→ RentComputation.f} { RentComputation f = λ (x_80: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨#{← RentComputation.g} #{≔ RentComputation.g.output} (#{→ RentComputation.g} (λ (x1_81: integer) → error_empty ⟨ ⟨#{☛ } true ⊢ ⟨x1_81 +! 1⟩⟩ | false ⊢ ∅ ⟩)) #{≔ RentComputation.g.input0} (x_80 +! 1)⟩⟩ | false ⊢ ∅ ⟩; }.f) #{≔ RentComputation.f.input0} param0_79; } +[LOG] ≔ RentComputation.direct.output: RentComputation { -- f: } [LOG] ← RentComputation.direct [LOG] → RentComputation.f [LOG] ≔ RentComputation.f.input0: 1 From 1efdf4262d148e8989de2d99ce6e5140784049b0 Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Wed, 8 May 2024 12:23:35 +0200 Subject: [PATCH 2/4] Clerk: fix finalisation on exit We have temporary files to remove upon `ninja` completion so it's not a good idea to `exec` without fork. This patch ensures `/tmp/clerk_*.ninja` files aren't left in `/tmp`. --- build_system/clerk_driver.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/build_system/clerk_driver.ml b/build_system/clerk_driver.ml index 55a0ed32..f377c377 100644 --- a/build_system/clerk_driver.ml +++ b/build_system/clerk_driver.ml @@ -935,7 +935,16 @@ let ninja_cmdline ninja_flags nin_file targets = let run_ninja ~clean_up_env cmdline = let cmd = List.hd cmdline in let env = if clean_up_env then cleaned_up_env () else Unix.environment () in - Unix.execvpe cmd (Array.of_list cmdline) env + let npid = + Unix.create_process_env cmd (Array.of_list cmdline) env Unix.stdin + Unix.stdout Unix.stderr + in + let return_code = + match Unix.waitpid [] npid with + | _, Unix.WEXITED n -> n + | _, (Unix.WSIGNALED n | Unix.WSTOPPED n) -> 128 - n + in + raise (Catala_utils.Cli.Exit_with return_code) open Cmdliner From 1cf34d9123736398b74a66384c2c26ffda102d14 Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Wed, 8 May 2024 12:35:11 +0200 Subject: [PATCH 3/4] Fix formatting of syntax error messages --- compiler/surface/parser_driver.ml | 7 ++++--- tests/default/bad/typing_or_logical_error.catala_en | 2 +- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/compiler/surface/parser_driver.ml b/compiler/surface/parser_driver.ml index 4244ae1d..b1474823 100644 --- a/compiler/surface/parser_driver.ml +++ b/compiler/surface/parser_driver.ml @@ -79,7 +79,7 @@ let raise_parser_error | None -> "Error token", error_loc | Some last_good_loc -> "Last good token", last_good_loc); ] - "Syntax error at %a@\n%t" + "@[Syntax error at %a:@ %t@]" (fun ppf string -> Format.fprintf ppf "@{\"%s\"@}" string) token msg @@ -131,10 +131,11 @@ module ParserAux (LocalisedLexer : Lexer_common.LocalisedLexer) = struct (match Parser_errors.message (state env) with | exception Not_found -> Format.fprintf ppf "@{unexpected token@}" | msg -> - Format.fprintf ppf "@{@<1>»@} @[%a@]" Format.pp_print_text + Format.fprintf ppf "@{@<1>%s@} @[%a@]" "»" + Format.pp_print_text (String.trim (String.uncapitalize_ascii msg))); if acceptable_tokens <> [] then - Format.fprintf ppf "@,@[Those are valid at this point:@ %a@]" + Format.fprintf ppf "@\n@[Those are valid at this point:@ %a@]" (Format.pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf ",@ ") (fun ppf string -> Format.fprintf ppf "@{\"%s\"@}" string)) diff --git a/tests/default/bad/typing_or_logical_error.catala_en b/tests/default/bad/typing_or_logical_error.catala_en index 699f337d..ea830470 100644 --- a/tests/default/bad/typing_or_logical_error.catala_en +++ b/tests/default/bad/typing_or_logical_error.catala_en @@ -13,7 +13,7 @@ scope A: $ catala test-scope A ┌─[ERROR]─ │ -│ Syntax error at "=" +│ Syntax error at "=": │ » expected 'under condition' followed by a condition, 'equals' followed by │ the definition body, or the rest of the variable qualified name │ Those are valid at this point: "of", "state", "equals", "under condition", From 5f289307a0c9c46ab6b244db5c165de25cc0d9ab Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Wed, 15 May 2024 10:24:18 +0200 Subject: [PATCH 4/4] Runtime value printer: use on non-printable entitites --- compiler/shared_ast/interpreter.ml | 2 +- tests/scope/good/scope_call3.catala_en | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/compiler/shared_ast/interpreter.ml b/compiler/shared_ast/interpreter.ml index 369657e3..5e73afa3 100644 --- a/compiler/shared_ast/interpreter.ml +++ b/compiler/shared_ast/interpreter.ml @@ -60,7 +60,7 @@ let rec format_runtime_value lang ppf = function ~pp_sep:(fun ppf () -> Format.fprintf ppf ";@ ") (format_runtime_value lang)) (Array.to_list elts) - | Runtime.Unembeddable -> Format.pp_print_string ppf "" + | Runtime.Unembeddable -> Format.pp_print_string ppf "" let print_log lang entry = let pp_infos = diff --git a/tests/scope/good/scope_call3.catala_en b/tests/scope/good/scope_call3.catala_en index 42bd9798..2cd17652 100644 --- a/tests/scope/good/scope_call3.catala_en +++ b/tests/scope/good/scope_call3.catala_en @@ -44,7 +44,7 @@ $ catala Interpret -t -s HousingComputation --debug [DEBUG] Translating to default calculus... [DEBUG] Typechecking again... [DEBUG] Starting interpretation... -[LOG] ≔ HousingComputation.f: +[LOG] ≔ HousingComputation.f: [LOG] ☛ Definition applied: ─➤ tests/scope/good/scope_call3.catala_en:8.14-8.20: │ @@ -59,14 +59,15 @@ $ catala Interpret -t -s HousingComputation --debug │ ‾ [LOG] → RentComputation.direct [LOG] ≔ RentComputation.direct.input: RentComputation_in { } -[LOG] ≔ RentComputation.g: -[LOG] ≔ RentComputation.f: +[LOG] ≔ RentComputation.g: +[LOG] ≔ RentComputation.f: [LOG] ☛ Definition applied: ─➤ tests/scope/good/scope_call3.catala_en:7.29-7.54: │ 7 │ definition f of x equals (output of RentComputation).f of x │ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾ -[LOG] ≔ RentComputation.direct.output: RentComputation { -- f: } +[LOG] ≔ RentComputation.direct. + output: RentComputation { -- f: } [LOG] ← RentComputation.direct [LOG] → RentComputation.f [LOG] ≔ RentComputation.f.input0: 1