diff --git a/compiler/driver.ml b/compiler/driver.ml index 0192bfc9..886f6d25 100644 --- a/compiler/driver.ml +++ b/compiler/driver.ml @@ -217,7 +217,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool) match backend with | Cli.Proof -> let vcs = Verification.Conditions.generate_verification_conditions prgm in - Verification.Z3encoding.solve_vc prgm prgm.decl_ctx vcs; + Verification.Solver.solve_vc prgm prgm.decl_ctx vcs; 0 | Cli.Interpret -> Cli.debug_print "Starting interpretation..."; diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml new file mode 100644 index 00000000..fa5cb8c5 --- /dev/null +++ b/compiler/verification/io.ml @@ -0,0 +1,113 @@ +(* This file is part of the Catala compiler, a specification language for tax and social benefits + computation rules. Copyright (C) 2022 Inria, contributor: Aymeric Fromherz + + + Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except + in compliance with the License. You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software distributed under the License + is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express + or implied. See the License for the specific language governing permissions and limitations under + the License. *) + +open Utils +open Dcalc.Ast + +module type Backend = sig + type backend_context + + type vc_encoding + + val print_encoding : vc_encoding -> string + + type model + + type solver_result = ProvenTrue | ProvenFalse of model option | Unknown + + val solve_vc_encoding : backend_context -> vc_encoding -> solver_result + + val print_model : backend_context -> model -> string + + val is_model_empty : model -> bool +end + +module SolverIO (B : Backend) = struct + type vc_encoding_result = Success of B.vc_encoding * B.backend_context | 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 "%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 "%a" ScopeName.format_t vc.vc_scope) + (Bindlib.name_of (Pos.unmark vc.vc_variable))) + + let print_negative_result (vc : Conditions.verification_condition) (ctx : B.backend_context) + (model : B.model option) : 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 : string option = + match model with + | None -> + Some + "The solver did not manage to generate a counterexample to explain the faulty behavior." + | Some model -> + if B.is_model_empty model then None + else + Some + (Format.asprintf + "The solver generated the following counterexample to explain the faulty behavior:\n\ + %s" + (B.print_model ctx model)) + in + var_and_pos + ^ match counterexample with None -> "" | Some counterexample -> "\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) + (vc : Conditions.verification_condition * vc_encoding_result) : unit = + let vc, z3_vc = vc in + + Cli.debug_print + (Format.asprintf "For this variable:\n%s\n" + (Pos.retrieve_loc_text (Pos.get_position vc.Conditions.vc_guard))); + Cli.debug_print + (Format.asprintf "This verification condition was generated for %s:@\n%a" + (Cli.print_with_style [ ANSITerminal.yellow ] "%s" + (match vc.vc_kind with + | Conditions.NoEmptyError -> "the variable definition never to return an empty error" + | NoOverlappingExceptions -> "no two exceptions to ever overlap")) + (Dcalc.Print.format_expr decl_ctx) + vc.vc_guard); + + match z3_vc with + | Success (encoding, backend_ctx) -> ( + Cli.debug_print + (Format.asprintf "The translation to Z3 is the following:@\n%s" + (B.print_encoding encoding)); + match B.solve_vc_encoding backend_ctx encoding with + | ProvenTrue -> Cli.result_print (print_positive_result vc) + | ProvenFalse model -> Cli.error_print (print_negative_result vc backend_ctx model) + | Unknown -> failwith "The solver failed at proving or disproving the VC") + | Fail msg -> Cli.error_print (Format.asprintf "The translation to Z3 failed:@\n%s" msg) +end diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml new file mode 100644 index 00000000..4ac35ecb --- /dev/null +++ b/compiler/verification/solver.ml @@ -0,0 +1,58 @@ +(* This file is part of the Catala compiler, a specification language for tax and social benefits + computation rules. Copyright (C) 2022 Inria, contributor: Aymeric Fromherz + + + Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except + in compliance with the License. You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software distributed under the License + is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express + or implied. See the License for the specific language governing permissions and limitations under + the License. *) + +open Utils +open Dcalc.Ast +open Z3 +open Z3backend + +(** [solve_vc] is the main entry point of this module. It takes a list of expressions [vcs] + corresponding to verification conditions that must be discharged by Z3, and attempts to solve + them **) +let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verification_condition list) : + unit = + 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 + let make_backend_context (free_vars_typ : typ Pos.marked VarMap.t) = + { + ctx_z3 = z3_ctx; + ctx_decl = decl_ctx; + ctx_var = + VarMap.union + (fun _ _ _ -> failwith "[Z3 encoding]: A Variable cannot be both free and bound") + (variable_types prgm) free_vars_typ; + ctx_funcdecl = VarMap.empty; + ctx_z3vars = StringMap.empty; + ctx_z3datatypes = EnumMap.empty; + ctx_z3matchsubsts = VarMap.empty; + ctx_z3structs = StructMap.empty; + } + in + let z3_vcs = + List.map + (fun vc -> + ( vc, + try + let ctx, z3_vc = + Z3backend.translate_expr + (make_backend_context vc.Conditions.vc_free_vars_typ) + (Bindlib.unbox (Dcalc.Optimizations.remove_all_logs vc.Conditions.vc_guard)) + in + Z3backend.Io.Success (z3_vc, ctx) + with Failure msg -> Fail msg )) + vcs + in + List.iter (Z3backend.Io.encode_and_check_vc decl_ctx) z3_vcs diff --git a/compiler/verification/z3encoding.ml b/compiler/verification/z3backend.ml similarity index 84% rename from compiler/verification/z3encoding.ml rename to compiler/verification/z3backend.ml index 15431ab3..3b40b434 100644 --- a/compiler/verification/z3encoding.ml +++ b/compiler/verification/z3backend.ml @@ -468,7 +468,7 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : context * Expr.expr let body = Bindlib.msubst (Pos.unmark e) [| fresh_e |] in translate_expr ctx body - (* TODO: Denis, Is this true for constructors with no payload? *) + (* Invariant: Catala match arms are always lambda*) | _ -> failwith "[Z3 encoding] : Arms branches inside VCs should be lambdas" in @@ -558,121 +558,28 @@ and translate_expr (ctx : context) (vc : expr Pos.marked) : context * Expr.expr ] ) | ErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported" -type vc_encoding_result = Success of context * Expr.expr | Fail of string +module Backend = struct + type backend_context = context -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 "%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 "%a" ScopeName.format_t vc.vc_scope) - (Bindlib.name_of (Pos.unmark vc.vc_variable))) + type vc_encoding = Z3.Expr.expr -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 : string option = - match Solver.get_model solver with - | None -> - Some - "The solver did not manage to generate a counterexample to explain the faulty behavior." - | Some model -> - if List.length (Model.get_decls model) = 0 then None - else - Some - (Format.asprintf - "The solver generated the following counterexample to explain the faulty behavior:\n\ - %s" - (print_model ctx model)) - in - var_and_pos - ^ match counterexample with None -> "" | Some counterexample -> "\n" ^ counterexample + let print_encoding (vc : vc_encoding) : string = Expr.to_string vc -(** [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) - (vc : Conditions.verification_condition * vc_encoding_result) : unit = - let vc, z3_vc = vc in + type model = Z3.Model.model - Cli.debug_print - (Format.asprintf "For this variable:\n%s\n" - (Pos.retrieve_loc_text (Pos.get_position vc.Conditions.vc_guard))); - Cli.debug_print - (Format.asprintf "This verification condition was generated for %s:@\n%a" - (Cli.print_with_style [ ANSITerminal.yellow ] "%s" - (match vc.vc_kind with - | Conditions.NoEmptyError -> "the variable definition never to return an empty error" - | NoOverlappingExceptions -> "no two exceptions to ever overlap")) - (Dcalc.Print.format_expr decl_ctx) - vc.vc_guard); + type solver_result = ProvenTrue | ProvenFalse of model option | Unknown - match z3_vc with - | Success (ctx, z3_vc) -> - Cli.debug_print - (Format.asprintf "The translation to Z3 is the following:@\n%s" (Expr.to_string z3_vc)); + let solve_vc_encoding (ctx : backend_context) (encoding : vc_encoding) : solver_result = + let solver = Z3.Solver.mk_solver ctx.ctx_z3 None in + Z3.Solver.add solver [ Boolean.mk_not ctx.ctx_z3 encoding ]; + match Z3.Solver.check solver [] with + | UNSATISFIABLE -> ProvenTrue + | SATISFIABLE -> ProvenFalse (Z3.Solver.get_model solver) + | UNKNOWN -> Unknown - let solver = Solver.mk_solver z3_ctx None in + let print_model (ctx : backend_context) (m : model) : string = print_model ctx m - Solver.add solver [ Boolean.mk_not z3_ctx z3_vc ]; + let is_model_empty (m : model) : bool = List.length (Z3.Model.get_decls m) = 0 +end - if Solver.check solver [] = UNSATISFIABLE then Cli.result_print (print_positive_result vc) - else 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] - corresponding to verification conditions that must be discharged by Z3, and attempts to solve - them **) -let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verification_condition list) : - unit = - 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 - - let z3_vcs = - List.map - (fun vc -> - ( vc, - try - let ctx, z3_vc = - translate_expr - { - ctx_z3 = z3_ctx; - ctx_decl = decl_ctx; - ctx_var = - VarMap.union - (fun _ _ _ -> - failwith "[Z3 encoding]: A Variable cannot be both free and bound") - (variable_types prgm) vc.Conditions.vc_free_vars_typ; - ctx_funcdecl = VarMap.empty; - ctx_z3vars = StringMap.empty; - ctx_z3datatypes = EnumMap.empty; - ctx_z3matchsubsts = VarMap.empty; - ctx_z3structs = StructMap.empty; - } - (Bindlib.unbox (Dcalc.Optimizations.remove_all_logs vc.Conditions.vc_guard)) - in - Success (ctx, z3_vc) - with Failure msg -> Fail msg )) - vcs - in - - List.iter (encode_and_check_vc decl_ctx z3_ctx) z3_vcs +module Io = Io.SolverIO (Backend) diff --git a/compiler/verification/z3encoding.mli b/compiler/verification/z3encoding.mli deleted file mode 100644 index c1eca56a..00000000 --- a/compiler/verification/z3encoding.mli +++ /dev/null @@ -1,18 +0,0 @@ -(* This file is part of the Catala compiler, a specification language for tax and social benefits - computation rules. Copyright (C) 2022 Inria, contributor: Aymeric Fromherz - - - Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except - in compliance with the License. You may obtain a copy of the License at - - http://www.apache.org/licenses/LICENSE-2.0 - - Unless required by applicable law or agreed to in writing, software distributed under the License - is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express - or implied. See the License for the specific language governing permissions and limitations under - the License. *) - -(** Encodes Dcalc expressions into Z3 queries *) - -val solve_vc : - Dcalc.Ast.program -> Dcalc.Ast.decl_ctx -> Conditions.verification_condition list -> unit