From 8fa8ac0d555a47f3fe633e579d475e8942f1d7ba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 29 Jun 2023 19:09:16 +0200 Subject: [PATCH] [models] Actually print values, not terms This patch makes it so that the model values that we print are actually values, not terms (i.e. they do not contain variables). This is achieved by aggressively substituting variable definitions when printing. The patch is a bit more involved than I'd have liked, because we can't simply substitute semantic values into terms, so the guts of the model printing had to be changed a little. The code now works in two pass. In the first pass, we build a hash table from symbols (constants and arrays) to their respective definitions using the new `value_defn` mini-language, which we then use for printing. The substitution is performed on-the-fly in the second pass, which actually prints, using the hash table that was built in the first pass. --- src/lib/frontend/models.ml | 203 ++++++++++++++++------------ src/lib/structures/ty.ml | 65 +++++---- src/lib/structures/ty.mli | 3 + tests/issues/555.models.expected | 3 +- tests/models/uf/uf2.models.expected | 2 +- 5 files changed, 160 insertions(+), 116 deletions(-) diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 31ddd5ce0..43d05cef0 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -41,13 +41,14 @@ module E = Expr module ME = Expr.Map module SE = Expr.Set module MS = Map.Make(String) +module MX = Shostak.MXH let constraints = ref MS.empty module Pp_smtlib_term = struct let to_string_type t = - asprintf "%a" Ty.print t + asprintf "%a" Ty.pp_smtlib t let rec print fmt t = let {E.f;xs;ty; _} = E.term_view t in @@ -229,26 +230,24 @@ module Pp_smtlib_term = struct end module SmtlibCounterExample = struct - - let x_print fmt (_ , ppr) = fprintf fmt "%s" ppr - let pp_term fmt t = if Options.get_output_format () == Why3 then Pp_smtlib_term.print fmt t else E.print fmt t - let dummy_value_of_type ty = + let rec pp_dummy_value_of_type ppf ty = match ty with - Ty.Tint -> "0" - | Ty.Treal -> "0.0" - | Ty.Tbool -> "false" - | _ -> asprintf "%a" pp_term (Expr.fresh_name ty) + Ty.Tint -> Fmt.pf ppf "0" + | Ty.Treal -> Fmt.pf ppf "0.0" + | Ty.Tbool -> Fmt.pf ppf "false" + | Ty.Tfarray (_, rty) -> + Fmt.pf ppf "((as const %a) %a)" Ty.pp_smtlib ty pp_dummy_value_of_type rty + | _ -> Fmt.pf ppf "@@%a" pp_term (Expr.fresh_name ty) let pp_dummy_value_of_type fmt ty = if not (Options.get_interpretation_use_underscore ()) then - let d = dummy_value_of_type ty in - fprintf fmt "%s " d + pp_dummy_value_of_type fmt ty else fprintf fmt "_ " @@ -316,43 +315,39 @@ module SmtlibCounterExample = struct let print_fun_def fmt name args ty t = let print_args fmt (ty,name) = - Format.fprintf fmt "(%s %a)" name Ty.print ty in + Format.fprintf fmt "(%s %a)" name Ty.pp_smtlib ty in let defined_value = try - let res,_,_ = (MS.find (Sy.to_string name) !constraints) in res + let res,_,_ = (MS.find (Sy.to_string name) !constraints) in + dprintf "%s" res with _ -> t in Format.fprintf fmt - "@ (define-fun %a (%a) %a %s)" + "@ (@[define-fun %a (%a) %a@ %t)@]" Sy.print name (Printer.pp_list_space (print_args)) args - Ty.print ty + Ty.pp_smtlib ty defined_value - let output_constants_counterexample ?(ignored = Sy.Set.empty) fmt records = + let output_constants_counterexample pp fmt records = ModelMap.iter (fun (f, xs_ty, ty) st -> assert (xs_ty == []); - begin match ty with - | Ty.Tfarray _ when Sy.Set.mem f ignored -> () - | _ -> - match ModelMap.V.elements st with - | [[], rep] -> - let rep = Format.asprintf "%a" x_print rep in - let rep = - match ty with - | Ty.Trecord r -> - let constr = mk_records_constr records f r in - sprintf "(%s)" constr - | _ -> rep - in - - print_fun_def fmt f [] ty rep - | _ -> assert false - end) - - let output_functions_counterexample fmt records fprofs = + match ModelMap.V.elements st with + | [[], rep] -> + let rep = + match ty with + | Ty.Trecord r -> + let constr = mk_records_constr records f r in + dprintf "(%s)" constr + | _ -> dprintf "%a" pp rep + in + + print_fun_def fmt f [] ty rep + | _ -> assert false) + + let output_functions_counterexample pp fmt records fprofs = let records = ref records in ModelMap.iter (fun (f, xs_ty, ty) st -> @@ -362,92 +357,68 @@ module SmtlibCounterExample = struct let rep = let representants = - ModelMap.V.fold (fun (xs_values,(_rep,srep)) acc -> + ModelMap.V.fold (fun (xs_values,(rep,srep)) acc -> assert ((List.length xs_ty_named) = (List.length xs_values)); records := check_records !records xs_ty_named xs_values f ty srep; - let reps = try MS.find srep acc with Not_found -> [] in - MS.add srep (xs_values :: reps) acc - ) st MS.empty in + let reps = try MX.find rep acc |> snd with Not_found -> [] in + MX.add rep (srep, xs_values :: reps) acc + ) st MX.empty in - let representants = MS.fold (fun srep xs_values_list acc -> - (srep,xs_values_list) :: acc) representants [] in + let representants = MX.fold (fun rep (srep, xs_values_list) acc -> + ((rep, srep),xs_values_list) :: acc) representants [] in let rec mk_ite_and xs tys = match xs, tys with | [],[] -> assert false - | [xs,_],[_ty,name] -> - asprintf "(= %s %a)" name pp_term xs - | (xs,_) :: l1, (_ty,name) :: l2 -> - asprintf "(and (= %s %a) %s)" + | [_,rs],[_ty,name] -> + dprintf "(= %s %a)" name pp rs + | (_,rs) :: l1, (_ty,name) :: l2 -> + dprintf "(and (= %s %a) %t)" name - pp_term xs + pp rs (mk_ite_and l1 l2) | _, _ -> assert false in let mk_ite_or l = let pp_or_list fmt xs_values = - fprintf fmt "%s" (mk_ite_and xs_values xs_ty_named) + fprintf fmt "%t" (mk_ite_and xs_values xs_ty_named) in match l with | [] -> assert false | [xs_values] -> mk_ite_and xs_values xs_ty_named | xs_values :: l -> - asprintf "(or %s %a)" + dprintf "(or %t %a)" (mk_ite_and xs_values xs_ty_named) (Printer.pp_list_space pp_or_list) l in let rec reps_aux reps = match reps with - | [] -> asprintf "%a" pp_dummy_value_of_type ty + | [] -> dprintf "%a" pp_dummy_value_of_type ty | [srep,xs_values_list] -> if Options.get_interpretation_use_underscore () then - asprintf "(ite %s %s %s)" + dprintf "(@[ite %t@ %a@ %t)@]" (mk_ite_or xs_values_list) - srep + pp srep (reps_aux []) else - srep + dprintf "%a" pp srep | (srep,xs_values_list) :: l -> - asprintf "(ite %s %s %s)" + dprintf "(@[ite %t@ %a@ %t)@]" (mk_ite_or xs_values_list) - srep + pp srep (reps_aux l) in if List.length representants = 1 then - sprintf "%s" (fst (List.hd representants)) + dprintf "%a" pp (fst (List.hd representants)) else reps_aux representants in print_fun_def fmt f xs_ty_named ty rep; ) fprofs; !records - - let output_arrays_counterexample fmt arrays = - let pp_array ppf (symbol, dty, st) = - let abstract = - Format.dprintf "(as @@%a %t)" Sy.print symbol dty - in - ModelMap.V.fold (fun (keys, (_value_r, value_s)) rst -> - Format.dprintf "(@[store@ %t@ %a %s)@]" - rst - Fmt.(list ~sep:sp (using (fun (_, (_, s)) -> s) string)) keys - value_s - ) st abstract ppf - in - let pp_array_ty ppf (args_ty, ret_ty) = - Format.fprintf ppf "(@[Array@ %a@ %a)@]" - Fmt.(list ~sep:sp Ty.print) args_ty - Ty.print ret_ty - in - ModelMap.iter - (fun (f, xs_ty, ty) st -> - let dty = Format.dprintf "%a" pp_array_ty (xs_ty, ty) in - Format.fprintf fmt "@ (@[define-fun %a () %t@ %a)@]" - Sy.print f dty pp_array (f, dty, st)) arrays - end (* of module SmtlibCounterExample *) @@ -475,6 +446,40 @@ module Why3CounterExample = struct end (* of module Why3CounterExample *) +(* The [value_defn] type is a mini-language of the expressions that can occur in + constant values. *) +type value_defn = + | Store of value_defn * value_defn * value_defn + (* An array store: [(store array key value)] *) + | Constant of Symbols.t * Ty.t + (* A constant of a given type. If the constant is defined in a model, it + must be resolved before being printed. *) + | Value of X.r * string + (* A leaf semantic value. This must be an actual value, i.e. it must not + contain any uninterpreted terms. *) + +let value (r, s) = + match X.term_extract r with + | Some t, _ -> + begin match E.term_view t with + | { f = Name _ as sy; _ } -> Constant (sy, X.type_info r) + | _ -> Value (r, s) + end + | _ -> + Value (r, s) + +let rec pp_value ppk ppf = function + | Store (a, k, v) -> + Format.fprintf ppf "(@[store@ %a@ %a %a)@]" + (pp_value ppk) a + (pp_value ppk) k + (pp_value ppk) v + | Constant (sy, t) -> ppk ppf (sy, t) + | Value (_, s) -> Format.pp_print_string ppf s + +let pp_constant ppf (_, t) = + Format.fprintf ppf "%a" SmtlibCounterExample.pp_dummy_value_of_type t + let output_concrete_model fmt props ~functions ~constants ~arrays = Format.fprintf fmt "@[("; if Options.get_model_type_constraints () then @@ -483,20 +488,42 @@ let output_concrete_model fmt props ~functions ~constants ~arrays = Format.fprintf fmt "@ ; values" end; + let values = Hashtbl.create 17 in + (* Add the constants *) + ModelMap.iter (fun (f, xs_ty, _) st -> + assert (Lists.is_empty xs_ty); + + ModelMap.V.iter (fun (keys, (value_r, value_s)) -> + assert (Lists.is_empty keys); + Hashtbl.add values f (value (value_r, value_s))) + st) constants; + + (* Add the arrays values, when applicable *) + ModelMap.iter (fun (f, xs_ty, ty) st -> + let root = + try Hashtbl.find values f + with Not_found -> Constant (f, Tfarray (List.hd xs_ty, ty)) + in + Hashtbl.replace values f @@ + ModelMap.V.fold (fun (keys, rs) acc -> + Store (acc, value (snd (List.hd keys)), value rs)) + st root) + arrays; + + let pp_value = + pp_value (fun ppf (sy, _) -> + pp_value pp_constant ppf (Hashtbl.find values sy)) + in + + let pp_x ppf xs = pp_value ppf (value xs) in + (* Functions *) let records = SmtlibCounterExample.output_functions_counterexample - fmt MS.empty functions in - - let array_symbols = - ModelMap.fold (fun (f, _, _) _ -> Sy.Set.add f) arrays Sy.Set.empty + pp_x fmt MS.empty functions in (* Constants *) - (* If the constant is present in the arrays map, it will be printed there. *) SmtlibCounterExample.output_constants_counterexample - ~ignored:array_symbols fmt records constants; - - (* Arrays *) - SmtlibCounterExample.output_arrays_counterexample fmt arrays; + pp_x fmt records constants; Printer.print_fmt fmt "@]@,)"; diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index a424e9166..141559cca 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -49,6 +49,26 @@ and trecord = { record_constr : Hstring.t; (* for ADTs that become records. default is "{" *) } +module Smtlib = struct + let rec pp ppf = function + | Tint -> Fmt.pf ppf "Int" + | Treal -> Fmt.pf ppf "Real" + | Tbool -> Fmt.pf ppf "Bool" + | Tunit -> Fmt.pf ppf "unit" + | Tbitv n -> Fmt.pf ppf "(_ BitVec %d)" n + | Tfarray (a_t, r_t) -> + Fmt.pf ppf "(Array %a %a)" pp a_t pp r_t + | Tsum (name, _) | Text ([], name) + | Trecord { args = []; name; _ } | Tadt (name, []) -> + Fmt.pf ppf "%a" Hstring.print name + | Text (args, name) | Trecord { args; name; _ } | Tadt (name, args) -> + Fmt.(pf ppf "(@[%a %a@])" Hstring.print name (list ~sep:sp pp) args) + | Tvar { v; value = None; _ } -> Fmt.pf ppf "A%d" v + | Tvar { value = Some t; _ } -> pp ppf t +end + +let pp_smtlib = Smtlib.pp + exception TypeClash of t*t exception Shorten of t @@ -83,15 +103,9 @@ let print_generic body_of = let rec print = let open Format in fun body_of fmt -> function - | Tint -> - if Options.get_output_smtlib () then fprintf fmt "Int" - else fprintf fmt "int" - | Treal -> - if Options.get_output_smtlib () then fprintf fmt "Real" - else fprintf fmt "real" - | Tbool -> - if Options.get_output_smtlib () then fprintf fmt "Bool" - else fprintf fmt "bool" + | Tint -> fprintf fmt "int" + | Treal -> fprintf fmt "real" + | Tbool -> fprintf fmt "bool" | Tunit -> fprintf fmt "unit" | Tbitv n -> fprintf fmt "bitv[%d]" n | Tvar{v=v ; value = None} -> fprintf fmt "'a_%d" v @@ -106,27 +120,15 @@ let print_generic body_of = (*fprintf fmt "('a_%d->%a)" v print t *) print body_of fmt t | Text(l, s) when l == [] -> - if Options.get_output_smtlib () then fprintf fmt "%s" (Hstring.view s) - else fprintf fmt "%s" (Hstring.view s) + fprintf fmt "%s" (Hstring.view s) | Text(l,s) -> - if Options.get_output_smtlib () then - fprintf fmt "(%s %a)" (Hstring.view s) print_list l - else fprintf fmt "%a %s" print_list l (Hstring.view s) + fprintf fmt "%a %s" print_list l (Hstring.view s) | Tfarray (t1, t2) -> - if Options.get_output_smtlib () then - fprintf fmt "(Array %a %a)" (print body_of) t1 (print body_of) t2 - else - fprintf fmt "(%a,%a) farray" (print body_of) t1 (print body_of) t2 + fprintf fmt "(%a,%a) farray" (print body_of) t1 (print body_of) t2 | Tsum(s, _) -> - if Options.get_output_smtlib () then - fprintf fmt "%s" (Hstring.view s) - else fprintf fmt "%s" (Hstring.view s) + fprintf fmt "%s" (Hstring.view s) | Trecord { args = lv; name = n; lbs = lbls; _ } -> - if Options.get_output_smtlib () then begin - if lv == [] then fprintf fmt "%s" (Hstring.view n) - else fprintf fmt "%a %s" print_list lv (Hstring.view n) - end - else begin + begin fprintf fmt "%a %s" print_list lv (Hstring.view n); if body_of != None then begin fprintf fmt " = {"; @@ -177,6 +179,17 @@ let print_generic body_of = List.iter (Format.fprintf fmt ", %a" (print body_of)) l; Format.fprintf fmt ")" in + let print body_of ppf t = + if Options.get_output_smtlib () then + pp_smtlib ppf t + else + print body_of ppf t + and print_list ppf ts = + if Options.get_output_smtlib () then + Fmt.(list ~sep:sp pp_smtlib |> parens) ppf ts + else + print_list ppf ts + in print, print_list let print_list = snd (print_generic None) diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index c33d1d1a7..895bac4e2 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -130,6 +130,9 @@ val equal : t -> t -> bool val compare : t -> t -> int (** Comparison function *) +val pp_smtlib : Format.formatter -> t -> unit +(** Printing function for types in smtlib2 format. *) + val print : Format.formatter -> t -> unit (** Printing function for types (does not print the type of each fields for records). *) diff --git a/tests/issues/555.models.expected b/tests/issues/555.models.expected index f08f315e8..e81320831 100644 --- a/tests/issues/555.models.expected +++ b/tests/issues/555.models.expected @@ -1,7 +1,8 @@ unknown ( + (define-fun a1 () (Array Int Int) + (store ((as const (Array Int Int)) 0) 0 0)) (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) ) diff --git a/tests/models/uf/uf2.models.expected b/tests/models/uf/uf2.models.expected index 5d1f06107..3c1182254 100644 --- a/tests/models/uf/uf2.models.expected +++ b/tests/models/uf/uf2.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun f ((arg_0 Int)) Int (ite (= arg_0 a) 2 0)) + (define-fun f ((arg_0 Int)) Int (ite (= arg_0 0) 2 0)) (define-fun a () Int 0) (define-fun b () Int (- 2)) )