From 83bdd0b63254c147c8754c725a9f2d7fdf6a0a28 Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Tue, 11 Jan 2022 16:13:34 +0100 Subject: [PATCH] Test base for verification conditions encoding --- build_system/clerk.ml | 1 + compiler/verification/z3encoding.ml | 6 +- tests/test_proof/good/enums.catala_en | 20 ++ tests/test_proof/good/functions.catala_en | 14 ++ tests/test_proof/good/no_vars.catala_en | 10 + .../good/output/enums.catala_en.Proof | 104 +++++++++ .../good/output/functions.catala_en.Proof | 1 + .../good/output/no_vars.catala_en.Proof | 55 +++++ .../good/output/simple_vars.catala_en.Proof | 205 ++++++++++++++++++ .../good/output/structs.catala_en.Proof | 108 +++++++++ tests/test_proof/good/simple_vars.catala_en | 16 ++ tests/test_proof/good/structs.catala_en | 20 ++ 12 files changed, 557 insertions(+), 3 deletions(-) create mode 100644 tests/test_proof/good/enums.catala_en create mode 100644 tests/test_proof/good/functions.catala_en create mode 100644 tests/test_proof/good/no_vars.catala_en create mode 100644 tests/test_proof/good/output/enums.catala_en.Proof create mode 100644 tests/test_proof/good/output/functions.catala_en.Proof create mode 100644 tests/test_proof/good/output/no_vars.catala_en.Proof create mode 100644 tests/test_proof/good/output/simple_vars.catala_en.Proof create mode 100644 tests/test_proof/good/output/structs.catala_en.Proof create mode 100644 tests/test_proof/good/simple_vars.catala_en create mode 100644 tests/test_proof/good/structs.catala_en diff --git a/build_system/clerk.ml b/build_system/clerk.ml index 6303a9c2..f730bd54 100644 --- a/build_system/clerk.ml +++ b/build_system/clerk.ml @@ -124,6 +124,7 @@ let filename_to_expected_output_descr (output_dir : string) (filename : string) | ".tex" -> Some Cli.Latex | ".html" -> Some Cli.Html | ".py" -> Some Cli.Python + | ".proof" -> Some Cli.Proof | _ -> None in match backend with diff --git a/compiler/verification/z3encoding.ml b/compiler/verification/z3encoding.ml index 0f7eadf5..0efaba61 100644 --- a/compiler/verification/z3encoding.ml +++ b/compiler/verification/z3encoding.ml @@ -162,7 +162,7 @@ type vc_encoding_result = Success of Expr.expr | Fail of string them **) let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verification_condition list) : unit = - Printf.printf "Running Z3 version %s\n" Version.to_string; + Cli.debug_print (Format.asprintf "Running Z3 version %s" Version.to_string); let cfg = [ ("model", "true"); ("proof", "false") ] in let z3_ctx = mk_context cfg in @@ -205,7 +205,7 @@ let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verificati Solver.add solver (List.filter_map (fun (_, vc) -> match vc with Success e -> Some e | _ -> None) z3_vcs); - if Solver.check solver [] = SATISFIABLE then Cli.result_print "Success: Empty unreachable\n" + if Solver.check solver [] = SATISFIABLE then Cli.result_print "Success: Empty unreachable" else (* TODO: Print model as error message for Catala debugging purposes *) - Cli.error_print "Failure: Empty reachable\n" + Cli.error_print "Failure: Empty reachable" diff --git a/tests/test_proof/good/enums.catala_en b/tests/test_proof/good/enums.catala_en new file mode 100644 index 00000000..ec8db3ac --- /dev/null +++ b/tests/test_proof/good/enums.catala_en @@ -0,0 +1,20 @@ +## Test + +```catala +declaration enumeration T: + -- C content boolean + -- D content integer + +declaration enumeration S: + -- A content integer + -- B content T + +declaration scope A: + context x content integer + context y content S + +scope A: + definition y equals B content (D content 1) + definition x under condition match y with pattern -- A of a: true -- B of b: false consequence equals 0 + definition x under condition match y with pattern -- A of a: false -- B of b: true consequence equals 1 +``` \ No newline at end of file diff --git a/tests/test_proof/good/functions.catala_en b/tests/test_proof/good/functions.catala_en new file mode 100644 index 00000000..5458705c --- /dev/null +++ b/tests/test_proof/good/functions.catala_en @@ -0,0 +1,14 @@ +## Test + +```catala +declaration scope A: + context x content integer depends on boolean + context z content integer + +scope A: + definition x of y under condition y consequence equals 0 + definition x of y under condition not y consequence equals 1 + definition z under condition x of true = 0 consequence equals 0 + definition z under condition x of true < 0 consequence equals -1 + definition z under condition x of true > 0 consequence equals 1 +``` \ No newline at end of file diff --git a/tests/test_proof/good/no_vars.catala_en b/tests/test_proof/good/no_vars.catala_en new file mode 100644 index 00000000..a2d9012c --- /dev/null +++ b/tests/test_proof/good/no_vars.catala_en @@ -0,0 +1,10 @@ +## Test + +```catala +declaration scope A: + context x content integer + +scope A: + definition x under condition (6*7 = 42) and (false or (true and 1458 / 27 = 54)) + consequence equals 0 +``` \ No newline at end of file diff --git a/tests/test_proof/good/output/enums.catala_en.Proof b/tests/test_proof/good/output/enums.catala_en.Proof new file mode 100644 index 00000000..26b62047 --- /dev/null +++ b/tests/test_proof/good/output/enums.catala_en.Proof @@ -0,0 +1,104 @@ +[RESULT] For this variable: + --> test_proof/good/enums.catala_en + | +13 | context x content integer + | ^ + + Test +This verification condition was generated for no two exceptions to ever overlap: +true && true && + true && true && true && true && true && ~ false && + true && true && true && ~ false && true && true && ~ false && + true && true && true && true && true && ~ false && + true && true && true && ~ false && true && true && ~ false && + true && true && true && ~ false && true && true && true && ~ false && + true && true && + ~ + if true then + if false then false else false && true && true || + if + match y_12 with + A: λ (a_44: integer) → true + | B: λ (b_45: T) → false then true else false && + true && true && true && true else false && true && true && + if true then + if false then false else false && true && true || + if + match y_12 with + A: λ (a_46: integer) → false + | B: λ (b_47: T) → true then true else false && + true && true && true && true else false && true && true + && true && ~ false && true +[RESULT] The translation to Z3 is the following: +TODO +[RESULT] For this variable: + --> test_proof/good/enums.catala_en + | +13 | context x content integer + | ^ + + Test +This verification condition was generated for the variable definition never to return an empty error: +if true then + if true then + if false then false else false && true && true || + if false then false else false && true && true else false && + true && true || + if true then + if false then false else false && true && true || + if + match y_12 with + A: λ (a_48: integer) → true + | B: λ (b_49: T) → false then true else false && + true && true && true && true else false && true && true || + if true then + if false then false else false && true && true || + if + match y_12 with + A: λ (a_50: integer) → false + | B: λ (b_51: T) → true then true else false && + true && true && true && true else false && true && true else + false && true || false && true +[RESULT] The translation to Z3 is the following: +TODO +[RESULT] For this variable: + --> test_proof/good/enums.catala_en + | +14 | context y content S + | ^ + + Test +This verification condition was generated for no two exceptions to ever overlap: +true && true && + true && true && true && ~ false && true && true && true && ~ false && + true && true && ~ false && + true && true && true && ~ false && true && true && true && ~ false && + true && true && ~ false && true && ~ false && true +[RESULT] The translation to Z3 is the following: +(let ((a!1 (and (and true (and (and true true) (not false))) + (and true (and (and true true) (not false))) + (and (and true true) (not false))))) + (and (and true true) a!1 a!1 true (not false) true)) +[RESULT] For this variable: + --> test_proof/good/enums.catala_en + | +14 | context y content S + | ^ + + Test +This verification condition was generated for the variable definition never to return an empty error: +if true then + if true then + if false then false else false && true && true || + if false then false else false && true && true else false && + true && true || + if true then + if false then false else false && true && true || + if true then true else false && true && true else false && + true && true else false && true || false && true +[RESULT] The translation to Z3 is the following: +(let ((a!1 (and (=> false false) (=> (not false) false) (and true true)))) +(let ((a!2 (or a!1 (and (=> true true) (=> (not true) false) (and true true))))) +(let ((a!3 (or (and (=> true (or a!1 a!1)) + (=> (not true) false) + (and true true)) + (and (=> true a!2) (=> (not true) false) (and true true))))) +(let ((a!4 (or (and (=> true a!3) (=> (not true) false) true) false))) + (and a!4 true))))) +[RESULT] Success: Empty unreachable diff --git a/tests/test_proof/good/output/functions.catala_en.Proof b/tests/test_proof/good/output/functions.catala_en.Proof new file mode 100644 index 00000000..30404ce4 --- /dev/null +++ b/tests/test_proof/good/output/functions.catala_en.Proof @@ -0,0 +1 @@ +TODO \ No newline at end of file diff --git a/tests/test_proof/good/output/no_vars.catala_en.Proof b/tests/test_proof/good/output/no_vars.catala_en.Proof new file mode 100644 index 00000000..e91d2414 --- /dev/null +++ b/tests/test_proof/good/output/no_vars.catala_en.Proof @@ -0,0 +1,55 @@ +[RESULT] For this variable: + --> test_proof/good/no_vars.catala_en + | +5 | context x content integer + | ^ + + Test +This verification condition was generated for no two exceptions to ever overlap: +true && true && + true && + true && true && true && true && true && true && true && true && true && + true && true && true && true && true && true && true && ~ false && + true && true && true && ~ false && true && true && ~ false && + true && true && true && ~ false && true && true && true && ~ false && + true && true && ~ false && true && ~ false && true +[RESULT] The translation to Z3 is the following: +(and (and true true) + true + (and true true (and true true) true) + (and true true) + (and true true) + (and true true (and true true) true) + true + true + (not false) + (and true (and (and true true) (not false))) + (and (and true true) (not false)) + (and true (and (and true true) (not false))) + (and true (and (and true true) (not false))) + (and (and true true) (not false)) + true + (not false) + true) +[RESULT] For this variable: + --> test_proof/good/no_vars.catala_en + | +5 | context x content integer + | ^ + + Test +This verification condition was generated for the variable definition never to return an empty error: +if true then + if true then + if false then false else false && true && true || + if false then false else false && true && true else false && + true && true || + if true then + if false then false else false && true && true || + if 6 * 7 = 42 && false || true && 1458 / 27 = 54 then true else false + && + true && true && true && true && true && true && true && + true && true && true && true && true && true && true && true && + true else false && true && true else false && true || false && + true +[RESULT] The translation to Z3 is the following: +TODO +[RESULT] Success: Empty unreachable diff --git a/tests/test_proof/good/output/simple_vars.catala_en.Proof b/tests/test_proof/good/output/simple_vars.catala_en.Proof new file mode 100644 index 00000000..fb0c084e --- /dev/null +++ b/tests/test_proof/good/output/simple_vars.catala_en.Proof @@ -0,0 +1,205 @@ +[RESULT] For this variable: + --> test_proof/good/simple_vars.catala_en + | +7 | context z content integer + | ^ + + Test +This verification condition was generated for no two exceptions to ever overlap: +true && true && + true && true && true && true && true && ~ false && + true && true && true && ~ false && true && true && ~ false && + true && true && true && true && true && true && ~ false && + true && true && true && ~ false && true && true && ~ false && + true && true && true && true && true && ~ false && + true && true && true && ~ false && true && true && ~ false && + true && true && true && ~ false && true && true && true && ~ false && + true && true && + ~ + if true then + if false then false else false && true && true || + if x_5 = 0 then true else false && + true && true && true && true else false && true && true + && + if true then + if false then false else false && true && true || + if x_5 < 0 then true && true else false && + true && true && true && true else false && true && true + || + if true then + if false then false else false && true && true || + if x_5 = 0 then true else false && + true && true && true && true else false && true && true + && + if true then + if false then false else false && true && true || + if x_5 > 0 then true else false && + true && true && true && true else false && + true && true || + if true then + if false then false else false && true && true || + if x_5 < 0 then true && true else false && + true && true && true && true else false && + true && true && + if true then + if false then false else false && true && true || + if x_5 > 0 then true else false && + true && true && true && true else false && + true && true && true && ~ false && true +[RESULT] The translation to Z3 is the following: +TODO +[RESULT] For this variable: + --> test_proof/good/simple_vars.catala_en + | +7 | context z content integer + | ^ + + Test +This verification condition was generated for the variable definition never to return an empty error: +if true then + if true then + if false then false else false && true && true || + if false then false else false && true && true else false && + true && true || + if true then + if false then false else false && true && true || + if x_5 = 0 then true else false && true && true && true && true else + false && true && true || + if true then + if false then false else false && true && true || + if x_5 < 0 then true && true else false && + true && true && true && true else false && true && true || + if true then + if false then false else false && true && true || + if x_5 > 0 then true else false && true && true && true && true + else false && true && true else false && true || false && true +[RESULT] The translation to Z3 is the following: +TODO +[RESULT] For this variable: + --> test_proof/good/simple_vars.catala_en + | +5 | context x content integer + | ^ + + Test +This verification condition was generated for no two exceptions to ever overlap: +true && true && + true && true && true && ~ false && true && true && true && ~ false && + true && true && ~ false && + true && true && true && true && ~ false && + true && true && true && ~ false && true && true && ~ false && + true && true && true && ~ false && true && true && true && ~ false && + true && true && + ~ + if true then + if false then false else false && true && true || + if y_4 then true else false && true && true else false && + true && true && + if true then + if false then false else false && true && true || + if ~ y_4 then true else false && true && true && true else + false && true && true && true && ~ false && true +[RESULT] The translation to Z3 is the following: +(let ((a!1 (and (and true (and (and true true) (not false))) + (and true (and (and true true) (not false))))) + (a!2 (and (=> false false) (=> (not false) false) (and true true))) + (a!4 (and (=> (not y_4) true) + (=> (not (not y_4)) false) + (and (and true true) true)))) +(let ((a!3 (or a!2 (and (=> y_4 true) (=> (not y_4) false) (and true true))))) +(let ((a!5 (not (and (=> true a!3) + (=> (not true) false) + (and true true) + (=> true (or a!2 a!4)) + (=> (not true) false) + (and true true))))) + (and (and true true) + a!1 + (and (and true true) (not false)) + true + (and (and true true) true) + (not false) + (and true (and (and true true) (not false))) + (and (and true true) (not false)) + a!1 + (and true true) + a!5 + true + (not false) + true)))) +[RESULT] For this variable: + --> test_proof/good/simple_vars.catala_en + | +5 | context x content integer + | ^ + + Test +This verification condition was generated for the variable definition never to return an empty error: +if true then + if true then + if false then false else false && true && true || + if false then false else false && true && true else false && + true && true || + if true then + if false then false else false && true && true || + if y_4 then true else false && true && true else false && + true && true || + if true then + if false then false else false && true && true || + if ~ y_4 then true else false && true && true && true else false && + true && true else false && true || false && true +[RESULT] The translation to Z3 is the following: +(let ((a!1 (and (=> false false) (=> (not false) false) (and true true))) + (a!3 (and (=> (not y_4) true) + (=> (not (not y_4)) false) + (and true true) + true))) +(let ((a!2 (or a!1 (and (=> y_4 true) (=> (not y_4) false) (and true true))))) +(let ((a!4 (or (and (=> true (or a!1 a!1)) + (=> (not true) false) + (and true true)) + (and (=> true a!2) (=> (not true) false) (and true true)) + (and (=> true (or a!1 a!3)) + (=> (not true) false) + (and true true))))) +(let ((a!5 (or (and (=> true a!4) (=> (not true) false) true) false))) + (and a!5 true))))) +[RESULT] For this variable: + --> test_proof/good/simple_vars.catala_en + | +6 | context y content boolean + | ^ + + Test +This verification condition was generated for no two exceptions to ever overlap: +true && true && + true && true && true && ~ false && true && true && true && ~ false && + true && true && ~ false && + true && true && true && ~ false && true && true && true && ~ false && + true && true && ~ false && true && ~ false && true +[RESULT] The translation to Z3 is the following: +(let ((a!1 (and (and true (and (and true true) (not false))) + (and true (and (and true true) (not false))) + (and (and true true) (not false))))) + (and (and true true) a!1 a!1 true (not false) true)) +[RESULT] For this variable: + --> test_proof/good/simple_vars.catala_en + | +6 | context y content boolean + | ^ + + Test +This verification condition was generated for the variable definition never to return an empty error: +if true then + if true then + if false then false else false && true && true || + if false then false else false && true && true else false && + true && true || + if true then + if false then false else false && true && true || + if true then true else false && true && true else false && + true && true else false && true || false && true +[RESULT] The translation to Z3 is the following: +(let ((a!1 (and (=> false false) (=> (not false) false) (and true true)))) +(let ((a!2 (or a!1 (and (=> true true) (=> (not true) false) (and true true))))) +(let ((a!3 (or (and (=> true (or a!1 a!1)) + (=> (not true) false) + (and true true)) + (and (=> true a!2) (=> (not true) false) (and true true))))) +(let ((a!4 (or (and (=> true a!3) (=> (not true) false) true) false))) + (and a!4 true))))) +[RESULT] Success: Empty unreachable diff --git a/tests/test_proof/good/output/structs.catala_en.Proof b/tests/test_proof/good/output/structs.catala_en.Proof new file mode 100644 index 00000000..6bd56ff0 --- /dev/null +++ b/tests/test_proof/good/output/structs.catala_en.Proof @@ -0,0 +1,108 @@ +[RESULT] For this variable: + --> test_proof/good/structs.catala_en + | +13 | context x content integer + | ^ + + Test +This verification condition was generated for no two exceptions to ever overlap: +true && true && + true && true && true && true && true && true && true && ~ false && + true && true && true && ~ false && true && true && ~ false && + true && + true && true && true && true && true && true && true && true && ~ false + && true && true && true && ~ false && true && true && ~ false && + true && true && true && ~ false && true && true && true && ~ false && + true && true && + ~ + if true then + if false then false else false && true && true || + if y_4."a" = 0 && y_4."b"."c" then true else false && + true && true && true && true && true && true else false && + true && true && + if true then + if false then false else false && true && true || + if ~ y_4."a" = 0 || ~ y_4."b"."c" then true else false && + true && true && true && true && true && true && true && + true else false && true && true && true && ~ false && + true +[RESULT] The translation to Z3 is the following: +TODO +[RESULT] For this variable: + --> test_proof/good/structs.catala_en + | +13 | context x content integer + | ^ + + Test +This verification condition was generated for the variable definition never to return an empty error: +if true then + if true then + if false then false else false && true && true || + if false then false else false && true && true else false && + true && true || + if true then + if false then false else false && true && true || + if y_4."a" = 0 && y_4."b"."c" then true else false && + true && true && true && true && true && true else false && + true && true || + if true then + if false then false else false && true && true || + if ~ y_4."a" = 0 || ~ y_4."b"."c" then true else false && + true && true && true && true && true && true && true && true else + false && true && true else false && true || false && true +[RESULT] The translation to Z3 is the following: +TODO +[RESULT] For this variable: + --> test_proof/good/structs.catala_en + | +14 | context y content S + | ^ + + Test +This verification condition was generated for no two exceptions to ever overlap: +true && true && + true && true && true && true && true && ~ false && + true && true && true && ~ false && true && true && ~ false && + true && true && true && ~ false && true && true && true && ~ false && + true && true && ~ false && true && ~ false && true +[RESULT] The translation to Z3 is the following: +(and (and true true) + (and true true) + true + (and (and true true) (not false)) + (and true (and (and true true) (not false))) + (and (and true true) (not false)) + (and true (and (and true true) (not false))) + (and true (and (and true true) (not false))) + (and (and true true) (not false)) + true + (not false) + true) +[RESULT] For this variable: + --> test_proof/good/structs.catala_en + | +14 | context y content S + | ^ + + Test +This verification condition was generated for the variable definition never to return an empty error: +if true then + if true then + if false then false else false && true && true || + if false then false else false && true && true else false && + true && true || + if true then + if false then false else false && true && true || + if true then true && true && true else false && true && true else + false && true && true else false && true || false && true +[RESULT] The translation to Z3 is the following: +(let ((a!1 (and (=> false false) (=> (not false) false) (and true true))) + (a!2 (and (=> true (and (and true true) true)) + (=> (not true) false) + (and true true)))) +(let ((a!3 (or (and (=> true (or a!1 a!1)) + (=> (not true) false) + (and true true)) + (and (=> true (or a!1 a!2)) + (=> (not true) false) + (and true true))))) +(let ((a!4 (or (and (=> true a!3) (=> (not true) false) true) false))) + (and a!4 true)))) +[RESULT] Success: Empty unreachable diff --git a/tests/test_proof/good/simple_vars.catala_en b/tests/test_proof/good/simple_vars.catala_en new file mode 100644 index 00000000..85f28b96 --- /dev/null +++ b/tests/test_proof/good/simple_vars.catala_en @@ -0,0 +1,16 @@ +## Test + +```catala +declaration scope A: + context x content integer + context y content boolean + context z content integer + +scope A: + definition y equals true + definition x under condition y consequence equals 0 + definition x under condition not y consequence equals 1 + definition z under condition x = 0 consequence equals 0 + definition z under condition x < 0 consequence equals -1 + definition z under condition x > 0 consequence equals 1 +``` \ No newline at end of file diff --git a/tests/test_proof/good/structs.catala_en b/tests/test_proof/good/structs.catala_en new file mode 100644 index 00000000..352ca6c5 --- /dev/null +++ b/tests/test_proof/good/structs.catala_en @@ -0,0 +1,20 @@ +## Test + +```catala +declaration structure T: + data c content boolean + data d content integer + +declaration structure S: + data a content integer + data b content T + +declaration scope A: + context x content integer + context y content S + +scope A: + definition y equals S { -- a : 0 -- b : T { -- c : false -- d: 0}} + definition x under condition (y.a = 0) and y.b.c consequence equals 0 + definition x under condition not (y.a = 0) or not y.b.c consequence equals 1 +``` \ No newline at end of file