From bf444f548fa205a99d025e9d6b4bbe21e3bc3fbc Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Thu, 13 Jan 2022 10:46:23 +0100 Subject: [PATCH] Error message pretty-printing and sat solving example [skip ci] --- compiler/verification/z3encoding.ml | 94 +++++++++++-------- .../output/no_vars-conflict.catala_en.Proof | 13 ++- .../bad/output/no_vars-empty.catala_en.Proof | 13 ++- .../bad/output/sat_solving.catala_en.Proof | 35 +++++++ tests/test_proof/bad/sat_solving.catala_en | 39 ++++++++ .../good/output/functions.catala_en.Proof | 8 +- .../good/output/no_vars.catala_en.Proof | 4 +- .../good/output/simple_vars.catala_en.Proof | 12 +-- 8 files changed, 151 insertions(+), 67 deletions(-) create mode 100644 tests/test_proof/bad/output/sat_solving.catala_en.Proof create mode 100644 tests/test_proof/bad/sat_solving.catala_en diff --git a/compiler/verification/z3encoding.ml b/compiler/verification/z3encoding.ml index bf044196..97b0d1b5 100644 --- a/compiler/verification/z3encoding.ml +++ b/compiler/verification/z3encoding.ml @@ -61,21 +61,26 @@ let unique_name (v : Var.t) : string = lost during the translation (e.g., by translating a date to an integer) **) let print_model (ctx : context) (model : Model.model) : string = let decls = Model.get_decls model in - List.fold_left - (fun acc d -> - match Model.get_const_interp model d with - (* TODO: Better handling of this case *) - | None -> failwith "[Z3 model]: A variable does not have an associated Z3 solution" - (* Prints "name : value\n" *) - | Some e -> - if FuncDecl.get_arity d = 0 then - (* Constant case *) - let symbol_name = Symbol.to_string (FuncDecl.get_name d) in - let v = StringMap.find symbol_name ctx.ctx_z3vars in - (* TODO: Needs a better parsing of the value once we have more than integer types *) - Format.asprintf " %s : %s\n%s" (Bindlib.name_of v) (Expr.to_string e) acc - else failwith "[Z3 model]: Printing of functions is not yet supported") - "" decls + Format.asprintf "%a" + (Format.pp_print_list + ~pp_sep:(fun fmt () -> Format.fprintf fmt "\n") + (fun fmt d -> + match Model.get_const_interp model d with + (* TODO: Better handling of this case *) + | None -> failwith "[Z3 model]: A variable does not have an associated Z3 solution" + (* Prints "name : value\n" *) + | Some e -> + if FuncDecl.get_arity d = 0 then + (* Constant case *) + let symbol_name = Symbol.to_string (FuncDecl.get_name d) in + let v = StringMap.find symbol_name ctx.ctx_z3vars in + (* TODO: Needs a better parsing of the value once we have more than integer types *) + Format.fprintf fmt "%s %s : %s" + (Cli.print_with_style [ ANSITerminal.blue ] "%s" "-->") + (Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v)) + (Expr.to_string e) + else failwith "[Z3 model]: Printing of functions is not yet supported")) + decls (** [translate_typ_lit] returns the Z3 sort corresponding to the Catala literal type [t] **) let translate_typ_lit (ctx : context) (t : typ_lit) : Sort.sort = @@ -272,30 +277,43 @@ type vc_encoding_result = Success of context * Expr.expr | Fail of string let print_positive_result (vc : Conditions.verification_condition) : string = match vc.Conditions.vc_kind with | Conditions.NoEmptyError -> - Format.asprintf "%s: this variable never returns an empty error" - (Cli.print_with_style [ ANSITerminal.yellow ] "%s.%s" + Format.asprintf "%s This variable never returns an empty error" + (Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]" (Format.asprintf "%a" ScopeName.format_t vc.vc_scope) (Bindlib.name_of (Pos.unmark vc.vc_variable))) | Conditions.NoOverlappingExceptions -> - Format.asprintf "%s: no two exceptions to ever overlap for this variable" - (Cli.print_with_style [ ANSITerminal.yellow ] "%s.%s" + Format.asprintf "%s No two exceptions to ever overlap for this variable" + (Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]" (Format.asprintf "%a" ScopeName.format_t vc.vc_scope) (Bindlib.name_of (Pos.unmark vc.vc_variable))) -let print_negative_result (vc : Conditions.verification_condition) : string = - match vc.Conditions.vc_kind with - | Conditions.NoEmptyError -> - Format.asprintf "%s: this variable might return an empty error\n%s" - (Cli.print_with_style [ ANSITerminal.yellow ] "%s.%s" - (Format.asprintf "%a" ScopeName.format_t vc.vc_scope) - (Bindlib.name_of (Pos.unmark vc.vc_variable))) - (Pos.retrieve_loc_text (Pos.get_position vc.vc_variable)) - | Conditions.NoOverlappingExceptions -> - Format.asprintf "%s: at least two exceptions overlap for this variable\n%s" - (Cli.print_with_style [ ANSITerminal.yellow ] "%s.%s" - (Format.asprintf "%a" ScopeName.format_t vc.vc_scope) - (Bindlib.name_of (Pos.unmark vc.vc_variable))) - (Pos.retrieve_loc_text (Pos.get_position vc.vc_variable)) +let print_negative_result (vc : Conditions.verification_condition) (ctx : context) + (solver : Solver.solver) : string = + let var_and_pos = + match vc.Conditions.vc_kind with + | Conditions.NoEmptyError -> + Format.asprintf "%s This variable might return an empty error:\n%s" + (Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]" + (Format.asprintf "%a" ScopeName.format_t vc.vc_scope) + (Bindlib.name_of (Pos.unmark vc.vc_variable))) + (Pos.retrieve_loc_text (Pos.get_position vc.vc_variable)) + | Conditions.NoOverlappingExceptions -> + Format.asprintf "%s At least two exceptions overlap for this variable:\n%s" + (Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]" + (Format.asprintf "%a" ScopeName.format_t vc.vc_scope) + (Bindlib.name_of (Pos.unmark vc.vc_variable))) + (Pos.retrieve_loc_text (Pos.get_position vc.vc_variable)) + in + let counterexample = + match Solver.get_model solver with + | None -> + "The solver did not manage to generate a counterexample to explain the faulty behavior." + | Some model -> + Format.asprintf + "The solver generated the following counterexample to explain the faulty behavior:\n%s" + (print_model ctx model) + in + var_and_pos ^ "\n" ^ counterexample (** [encode_and_check_vc] spawns a new Z3 solver and tries to solve the expression [vc] **) let encode_and_check_vc (decl_ctx : decl_ctx) (z3_ctx : Z3.context) @@ -324,15 +342,9 @@ let encode_and_check_vc (decl_ctx : decl_ctx) (z3_ctx : Z3.context) Solver.add solver [ Boolean.mk_not z3_ctx z3_vc ]; if Solver.check solver [] = UNSATISFIABLE then Cli.result_print (print_positive_result vc) - else ( + else (* TODO: Print model as error message for Catala debugging purposes *) - Cli.error_print (print_negative_result vc); - match Solver.get_model solver with - | None -> Cli.error_print "Z3 did not manage to generate a counterexample" - | Some model -> - Cli.error_print - (Format.asprintf "Z3 generated the following counterexample:\n%s" - (print_model ctx model))) + Cli.error_print (print_negative_result vc ctx solver) | Fail msg -> Cli.error_print (Format.asprintf "The translation to Z3 failed:@\n%s" msg) (** [solve_vc] is the main entry point of this module. It takes a list of expressions [vcs] diff --git a/tests/test_proof/bad/output/no_vars-conflict.catala_en.Proof b/tests/test_proof/bad/output/no_vars-conflict.catala_en.Proof index f71d3d04..87675379 100644 --- a/tests/test_proof/bad/output/no_vars-conflict.catala_en.Proof +++ b/tests/test_proof/bad/output/no_vars-conflict.catala_en.Proof @@ -1,12 +1,11 @@ -[ERROR] A.y: at least two exceptions overlap for this variable +[ERROR] [A.y] At least two exceptions overlap for this variable: --> tests/test_proof/bad/no_vars-conflict.catala_en | 8 | context y content integer | ^ + Test -[ERROR] Z3 generated the following counterexample: - x : 0 - -[RESULT] A.y: this variable never returns an empty error -[RESULT] A.x: no two exceptions to ever overlap for this variable -[RESULT] A.x: this variable never returns an empty error +The solver generated the following counterexample to explain the faulty behavior: +--> x : 0 +[RESULT] [A.y] This variable never returns an empty error +[RESULT] [A.x] No two exceptions to ever overlap for this variable +[RESULT] [A.x] This variable never returns an empty error diff --git a/tests/test_proof/bad/output/no_vars-empty.catala_en.Proof b/tests/test_proof/bad/output/no_vars-empty.catala_en.Proof index 0d86d369..fffc745c 100644 --- a/tests/test_proof/bad/output/no_vars-empty.catala_en.Proof +++ b/tests/test_proof/bad/output/no_vars-empty.catala_en.Proof @@ -1,12 +1,11 @@ -[RESULT] A.y: no two exceptions to ever overlap for this variable -[ERROR] A.y: this variable might return an empty error +[RESULT] [A.y] No two exceptions to ever overlap for this variable +[ERROR] [A.y] This variable might return an empty error: --> tests/test_proof/bad/no_vars-empty.catala_en | 7 | context y content integer | ^ + Test -[ERROR] Z3 generated the following counterexample: - x : 1 - -[RESULT] A.x: no two exceptions to ever overlap for this variable -[RESULT] A.x: this variable never returns an empty error +The solver generated the following counterexample to explain the faulty behavior: +--> x : 1 +[RESULT] [A.x] No two exceptions to ever overlap for this variable +[RESULT] [A.x] This variable never returns an empty error diff --git a/tests/test_proof/bad/output/sat_solving.catala_en.Proof b/tests/test_proof/bad/output/sat_solving.catala_en.Proof new file mode 100644 index 00000000..a4632143 --- /dev/null +++ b/tests/test_proof/bad/output/sat_solving.catala_en.Proof @@ -0,0 +1,35 @@ +[RESULT] [A.x10] No two exceptions to ever overlap for this variable +[ERROR] [A.x10] This variable might return an empty error: + --> tests/test_proof/bad/sat_solving.catala_en + | +15 | context x10 content boolean + | ^^^ + + Test +The solver generated the following counterexample to explain the faulty behavior: +--> x6 : false +--> x8 : false +--> x5 : false +--> x2 : true +--> x1 : true +--> x9 : false +--> x3 : true +--> x7 : true +--> x4 : true +[RESULT] [A.x9] No two exceptions to ever overlap for this variable +[RESULT] [A.x9] This variable never returns an empty error +[RESULT] [A.x8] No two exceptions to ever overlap for this variable +[RESULT] [A.x8] This variable never returns an empty error +[RESULT] [A.x7] No two exceptions to ever overlap for this variable +[RESULT] [A.x7] This variable never returns an empty error +[RESULT] [A.x6] No two exceptions to ever overlap for this variable +[RESULT] [A.x6] This variable never returns an empty error +[RESULT] [A.x5] No two exceptions to ever overlap for this variable +[RESULT] [A.x5] This variable never returns an empty error +[RESULT] [A.x4] No two exceptions to ever overlap for this variable +[RESULT] [A.x4] This variable never returns an empty error +[RESULT] [A.x3] No two exceptions to ever overlap for this variable +[RESULT] [A.x3] This variable never returns an empty error +[RESULT] [A.x2] No two exceptions to ever overlap for this variable +[RESULT] [A.x2] This variable never returns an empty error +[RESULT] [A.x1] No two exceptions to ever overlap for this variable +[RESULT] [A.x1] This variable never returns an empty error diff --git a/tests/test_proof/bad/sat_solving.catala_en b/tests/test_proof/bad/sat_solving.catala_en new file mode 100644 index 00000000..abe2ffae --- /dev/null +++ b/tests/test_proof/bad/sat_solving.catala_en @@ -0,0 +1,39 @@ +## Test + + +```catala +declaration scope A: + context x1 content boolean + context x2 content boolean + context x3 content boolean + context x4 content boolean + context x5 content boolean + context x6 content boolean + context x7 content boolean + context x8 content boolean + context x9 content boolean + context x10 content boolean + +scope A: + definition x1 equals true + definition x2 equals false + definition x3 equals true + definition x4 equals false + definition x5 equals true + definition x6 equals false + definition x7 equals true + definition x8 equals false + definition x9 equals true + definition x10 under condition + (x1 or x2 or x3 or x4 or x5) + and (not x1 or not x2 or not x3 or not x4 or not x5) + and (x1 or not x2) + and (x3 or not x4 or x5) + and (x5) + and (not x1 or x2) + and (x6 or not x7 or x8 or not x1) + and (x2 or not x4 or x5 or not x6) + and (x7 or x8 or x9 or not x2) + consequence equals false + +``` diff --git a/tests/test_proof/good/output/functions.catala_en.Proof b/tests/test_proof/good/output/functions.catala_en.Proof index d6c23a69..b8a117cc 100644 --- a/tests/test_proof/good/output/functions.catala_en.Proof +++ b/tests/test_proof/good/output/functions.catala_en.Proof @@ -1,4 +1,4 @@ -[RESULT] A.z: no two exceptions to ever overlap for this variable -[RESULT] A.z: this variable never returns an empty error -[RESULT] A.x: no two exceptions to ever overlap for this variable -[RESULT] A.x: this variable never returns an empty error +[RESULT] [A.z] No two exceptions to ever overlap for this variable +[RESULT] [A.z] This variable never returns an empty error +[RESULT] [A.x] No two exceptions to ever overlap for this variable +[RESULT] [A.x] This variable never returns an empty error diff --git a/tests/test_proof/good/output/no_vars.catala_en.Proof b/tests/test_proof/good/output/no_vars.catala_en.Proof index fc9f4a47..b3b1a0d8 100644 --- a/tests/test_proof/good/output/no_vars.catala_en.Proof +++ b/tests/test_proof/good/output/no_vars.catala_en.Proof @@ -1,2 +1,2 @@ -[RESULT] A.x: no two exceptions to ever overlap for this variable -[RESULT] A.x: this variable never returns an empty error +[RESULT] [A.x] No two exceptions to ever overlap for this variable +[RESULT] [A.x] This variable never returns an empty error diff --git a/tests/test_proof/good/output/simple_vars.catala_en.Proof b/tests/test_proof/good/output/simple_vars.catala_en.Proof index 2f5c6b47..8bcf87ce 100644 --- a/tests/test_proof/good/output/simple_vars.catala_en.Proof +++ b/tests/test_proof/good/output/simple_vars.catala_en.Proof @@ -1,6 +1,6 @@ -[RESULT] A.z: no two exceptions to ever overlap for this variable -[RESULT] A.z: this variable never returns an empty error -[RESULT] A.x: no two exceptions to ever overlap for this variable -[RESULT] A.x: this variable never returns an empty error -[RESULT] A.y: no two exceptions to ever overlap for this variable -[RESULT] A.y: this variable never returns an empty error +[RESULT] [A.z] No two exceptions to ever overlap for this variable +[RESULT] [A.z] This variable never returns an empty error +[RESULT] [A.x] No two exceptions to ever overlap for this variable +[RESULT] [A.x] This variable never returns an empty error +[RESULT] [A.y] No two exceptions to ever overlap for this variable +[RESULT] [A.y] This variable never returns an empty error