catala/compiler/verification/z3encoding.ml

210 lines
10 KiB
OCaml
Raw Normal View History

(* 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
<aymeric.fromherz@inria.fr>
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
2022-01-08 20:37:04 +03:00
open Dcalc
2022-01-07 20:36:25 +03:00
open Ast
open Z3
2022-01-10 16:37:17 +03:00
type context = { ctx_z3 : Z3.context; ctx_decl : decl_ctx; ctx_var : typ Pos.marked VarMap.t }
2022-01-10 13:52:48 +03:00
(** [translate_typ_lit] returns the Z3 sort corresponding to the Catala literal type [t] **)
2022-01-10 16:51:36 +03:00
let translate_typ_lit (ctx : context) (t : typ_lit) : Sort.sort = match t with
| TBool -> Boolean.mk_sort ctx.ctx_z3
| TUnit -> failwith "[Z3 encoding] TUnit type not supported"
2022-01-10 16:51:36 +03:00
| TInt -> Arithmetic.Integer.mk_sort ctx.ctx_z3
| TRat -> failwith "[Z3 encoding] TRat type not supported"
| TMoney -> failwith "[Z3 encoding] TMoney type not supported"
| TDate -> failwith "[Z3 encoding] TDate type not supported"
| TDuration -> failwith "[Z3 encoding] TDuration type not supported"
2022-01-10 16:46:41 +03:00
(** [translate_typ] returns the Z3 sort correponding to the Catala type [t] **)
2022-01-10 16:51:36 +03:00
let translate_typ (ctx : context) (t : typ) : Sort.sort = match t with
| TLit t -> translate_typ_lit ctx t
2022-01-10 16:46:41 +03:00
| TTuple _ -> failwith "[Z3 encoding] TTuple type not supported"
| TEnum _ -> failwith "[Z3 encoding] TEnum type not supported"
| TArrow _ -> failwith "[Z3 encoding] TArrow type not supported"
| TArray _ -> failwith "[Z3 encoding] TArray type not supported"
| TAny -> failwith "[Z3 encoding] TAny type not supported"
2022-01-07 20:25:35 +03:00
(** [translate_lit] returns the Z3 expression as a literal corresponding to [lit] **)
let translate_lit (ctx : context) (l : lit) : Expr.expr =
match l with
2022-01-10 13:52:48 +03:00
| LBool b -> if b then Boolean.mk_true ctx.ctx_z3 else Boolean.mk_false ctx.ctx_z3
2022-01-07 20:25:35 +03:00
| LEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
2022-01-10 13:52:48 +03:00
| LInt n -> Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (Runtime.integer_to_int n)
2022-01-07 20:36:25 +03:00
| LRat _ -> failwith "[Z3 encoding] LRat literals not supported"
| LMoney _ -> failwith "[Z3 encoding] LMoney literals not supported"
2022-01-07 20:25:35 +03:00
| LUnit -> failwith "[Z3 encoding] LUnit literals not supported"
| LDate _ -> failwith "[Z3 encoding] LDate literals not supported"
| LDuration _ -> failwith "[Z3 encoding] LDuration literals not supported"
2022-01-08 20:37:04 +03:00
(** [translate_op] returns the Z3 expression corresponding to the application of [op] to the
arguments [args] **)
2022-01-07 20:25:35 +03:00
let rec translate_op (ctx : context) (op : operator) (args : expr Pos.marked list) : Expr.expr =
match op with
| Ternop _top ->
2022-01-08 20:37:04 +03:00
let _e1, _e2, _e3 =
match args with
| [ e1; e2; e3 ] -> (e1, e2, e3)
2022-01-10 13:52:48 +03:00
| _ ->
failwith
(Format.asprintf "[Z3 encoding] Ill-formed ternary operator application: %a"
(Print.format_expr ctx.ctx_decl)
(EApp ((EOp op, Pos.no_pos), args), Pos.no_pos))
2022-01-07 20:45:54 +03:00
in
2022-01-07 20:36:25 +03:00
failwith "[Z3 encoding] ternary operator application not supported"
2022-01-08 20:37:04 +03:00
| Binop bop -> (
let e1, e2 =
match args with
| [ e1; e2 ] -> (e1, e2)
2022-01-10 13:52:48 +03:00
| _ ->
failwith
(Format.asprintf "[Z3 encoding] Ill-formed binary operator application: %a"
(Print.format_expr ctx.ctx_decl)
(EApp ((EOp op, Pos.no_pos), args), Pos.no_pos))
2022-01-07 20:45:54 +03:00
in
2022-01-07 20:36:25 +03:00
2022-01-08 20:37:04 +03:00
match bop with
2022-01-10 13:52:48 +03:00
| And -> Boolean.mk_and ctx.ctx_z3 [ translate_expr ctx e1; translate_expr ctx e2 ]
| Or -> Boolean.mk_or ctx.ctx_z3 [ translate_expr ctx e1; translate_expr ctx e2 ]
| Xor -> failwith "[Z3 encoding] application of binary operator Xor not supported"
| Add _ -> failwith "[Z3 encoding] application of binary operator Add not supported"
| Sub _ -> failwith "[Z3 encoding] application of binary operator Sub not supported"
| Mult _ -> failwith "[Z3 encoding] application of binary operator Mult not supported"
| Div _ -> failwith "[Z3 encoding] application of binary operator Div not supported"
2022-01-08 20:37:04 +03:00
| Lt op_kind -> (
match op_kind with
2022-01-10 13:52:48 +03:00
| KInt -> Arithmetic.mk_lt ctx.ctx_z3 (translate_expr ctx e1) (translate_expr ctx e2)
2022-01-08 20:37:04 +03:00
| _ ->
failwith
"[Z3 encoding] application of binary operator Lt for non-integers not supported")
2022-01-07 20:36:25 +03:00
| Lte _ -> failwith "[Z3 encoding] application of binary operator Lte not supported"
| Gt _ -> failwith "[Z3 encoding] application of binary operator Gt not supported"
| Gte KInt -> Arithmetic.mk_ge ctx.ctx_z3 (translate_expr ctx e1) (translate_expr ctx e2)
| Gte _ -> failwith "[Z3 encoding] application of non-integer binary operator Gte not supported"
| Eq -> failwith "[Z3 encoding] application of binary operator Eq not supported"
| Neq -> failwith "[Z3 encoding] application of binary operator New not supported"
| Map -> failwith "[Z3 encoding] application of binary operator Map not supported"
| Concat -> failwith "[Z3 encoding] application of binary operator Concat not supported"
2022-01-08 20:37:04 +03:00
| Filter -> failwith "[Z3 encoding] application of binary operator Filter not supported")
| Unop uop -> (
let e1 =
match args with
| [ e1 ] -> e1
(* TODO: Print term for error message *)
| _ -> failwith "[Z3 encoding] Ill-formed unary operator application"
2022-01-07 20:45:54 +03:00
in
2022-01-07 20:36:25 +03:00
2022-01-08 20:37:04 +03:00
match uop with
2022-01-07 20:36:25 +03:00
| Not -> failwith "[Z3 encoding] application of unary operator Not not supported"
| Minus _ -> failwith "[Z3 encoding] application of unary operator Minus not supported"
2022-01-07 20:45:54 +03:00
(* Omitting the log from the VC *)
| Log _ -> translate_expr ctx e1
2022-01-07 20:36:25 +03:00
| Length -> failwith "[Z3 encoding] application of unary operator Length not supported"
| IntToRat -> failwith "[Z3 encoding] application of unary operator IntToRat not supported"
| GetDay -> failwith "[Z3 encoding] application of unary operator GetDay not supported"
| GetMonth -> failwith "[Z3 encoding] application of unary operator GetMonth not supported"
2022-01-08 20:37:04 +03:00
| GetYear -> failwith "[Z3 encoding] application of unary operator GetYear not supported")
(** [translate_expr] translate the expression [vc] to its corresponding Z3 expression **)
2022-01-08 20:37:04 +03:00
and translate_expr (ctx : context) (vc : expr Pos.marked) : Expr.expr =
match Pos.unmark vc with
2022-01-10 16:46:41 +03:00
| EVar v ->
let t = VarMap.find (Pos.unmark v) ctx.ctx_var in
let v = Pos.unmark v in
let name = Format.asprintf "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v) in
2022-01-10 16:51:36 +03:00
Expr.mk_const_s ctx.ctx_z3 name (translate_typ ctx (Pos.unmark t))
2022-01-10 16:46:41 +03:00
| ETuple _ -> failwith "[Z3 encoding] ETuple unsupported"
| ETupleAccess _ -> failwith "[Z3 encoding] ETupleAccess unsupported"
| EInj _ -> failwith "[Z3 encoding] EInj unsupported"
| EMatch _ -> failwith "[Z3 encoding] EMatch unsupported"
| EArray _ -> failwith "[Z3 encoding] EArray unsupported"
2022-01-07 20:25:35 +03:00
| ELit l -> translate_lit ctx l
| EAbs _ -> failwith "[Z3 encoding] EAbs unsupported"
2022-01-08 20:37:04 +03:00
| EApp (head, args) -> (
match Pos.unmark head with
| EOp op -> translate_op ctx op args
2022-01-08 20:37:04 +03:00
| _ -> failwith "[Z3 encoding] EApp of a non-operator unsupported")
| EAssert _ -> failwith "[Z3 encoding] EAssert unsupported"
| EOp _ -> failwith "[Z3 encoding] EOp unsupported"
| EDefault _ -> failwith "[Z3 encoding] EDefault unsupported"
2022-01-07 20:36:25 +03:00
| EIfThenElse (e_if, e_then, e_else) ->
(* Encode this as (e_if ==> e_then) /\ (not e_if ==> e_else) *)
let z3_if = translate_expr ctx e_if in
2022-01-10 13:52:48 +03:00
Boolean.mk_and ctx.ctx_z3
2022-01-08 20:37:04 +03:00
[
2022-01-10 13:52:48 +03:00
Boolean.mk_implies ctx.ctx_z3 z3_if (translate_expr ctx e_then);
Boolean.mk_implies ctx.ctx_z3 (Boolean.mk_not ctx.ctx_z3 z3_if)
(translate_expr ctx e_else);
2022-01-08 20:37:04 +03:00
]
| ErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported"
2022-01-10 12:59:30 +03:00
type vc_encoding_result = Success of Expr.expr | Fail of string
2022-01-08 20:37:04 +03:00
(** [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 **)
2022-01-10 16:37:17 +03:00
let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verification_condition list) : unit =
2022-01-08 20:37:04 +03:00
Printf.printf "Running Z3 version %s\n" Version.to_string;
2022-01-08 20:37:04 +03:00
let cfg = [ ("model", "true"); ("proof", "false") ] in
2022-01-10 13:52:48 +03:00
let z3_ctx = mk_context cfg in
2022-01-07 20:36:25 +03:00
2022-01-10 13:52:48 +03:00
let solver = Solver.mk_solver z3_ctx None in
2022-01-10 12:59:30 +03:00
let z3_vcs =
List.map
(fun vc ->
2022-01-10 13:52:48 +03:00
( vc,
try
2022-01-10 16:37:17 +03:00
Success (translate_expr
{ ctx_z3 = z3_ctx; ctx_decl = decl_ctx; ctx_var = variable_types prgm }
vc.Conditions.vc_guard
)
2022-01-10 13:52:48 +03:00
with Failure msg -> Fail msg ))
2022-01-10 12:59:30 +03:00
vcs
in
List.iter
(fun (vc, z3_vc) ->
Cli.result_print
(Format.asprintf
"For this variable:\n%s\nThis verification condition was generated for %s:@\n%a"
(Pos.retrieve_loc_text (Pos.get_position vc.Conditions.vc_guard))
(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 z3_vc ->
let z3_vc_string = Expr.to_string z3_vc in
Cli.result_print
(Format.asprintf "The translation to Z3 is the following:@\n%s" z3_vc_string)
| Fail msg -> Cli.error_print (Format.asprintf "The translation to Z3 failed:@\n%s" msg))
z3_vcs;
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"
else
2022-01-07 20:36:25 +03:00
(* TODO: Print model as error message for Catala debugging purposes *)
2022-01-10 12:59:30 +03:00
Cli.error_print "Failure: Empty reachable\n"