Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Making sure to invalidate a hint hash if Z3 version changes #3037

Merged
merged 3 commits into from
Aug 28, 2023
Merged

Making sure to invalidate a hint hash if Z3 version changes #3037

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
b1da481
FStar.Compiler.Hints: Moving hints to separate module
mtzguido Aug 27, 2023
d3f242b
SMTEncoding: make sure to include Z3 version in hint hashes
mtzguido Aug 27, 2023
f044940
snap
mtzguido Aug 27, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
118 changes: 118 additions & 0 deletions ocaml/fstar-lib/FStar_Compiler_Hints.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,118 @@
open FStar_Json

(** Hints. *)
type hint = {
hint_name:string;
hint_index:Z.t;
fuel:Z.t;
ifuel:Z.t;
unsat_core:string list option;
query_elapsed_time:Z.t;
hash:string option
}

type hints = hint option list

type hints_db = {
module_digest:string;
hints: hints
}

type hints_read_result =
| HintsOK of hints_db
| MalformedJson
| UnableToOpen

let write_hints (filename: string) (hints: hints_db): unit =
let json = `List [
`String hints.module_digest;
`List (List.map (function
| None -> `Null
| Some { hint_name; hint_index; fuel; ifuel; unsat_core; query_elapsed_time; hash } ->
`List [
`String hint_name;
`Int (Z.to_int hint_index);
`Int (Z.to_int fuel);
`Int (Z.to_int ifuel);
(match unsat_core with
| None -> `Null
| Some strings ->
`List (List.map (fun s -> `String s) strings));
`Int (Z.to_int query_elapsed_time);
`String (match hash with | Some(h) -> h | _ -> "")
]
) hints.hints)
] in
let channel = open_out_bin filename in
BatPervasives.finally
(fun () -> close_out channel)
(fun channel -> Yojson.Safe.pretty_to_channel channel json)
channel

let read_hints (filename: string) : hints_read_result =
let mk_hint nm ix fuel ifuel unsat_core time hash_opt = {
hint_name = nm;
hint_index = Z.of_int ix;
fuel = Z.of_int fuel;
ifuel = Z.of_int ifuel;
unsat_core = begin
match unsat_core with
| `Null ->
None
| `List strings ->
Some (List.map (function
| `String s -> s
| _ -> raise Exit)
strings)
| _ ->
raise Exit
end;
query_elapsed_time = Z.of_int time;
hash = hash_opt
}
in
try
let chan = open_in filename in
let json = Yojson.Safe.from_channel chan in
close_in chan;
HintsOK (
match json with
| `List [
`String module_digest;
`List hints
] -> {
module_digest;
hints = List.map (function
| `Null -> None
| `List [ `String hint_name;
`Int hint_index;
`Int fuel;
`Int ifuel;
unsat_core;
`Int query_elapsed_time ] ->
(* This case is for dealing with old-style hint files
that lack a query-hashes field. We should remove this
case once we definitively remove support for old hints *)
Some (mk_hint hint_name hint_index fuel ifuel unsat_core query_elapsed_time None)
| `List [ `String hint_name;
`Int hint_index;
`Int fuel;
`Int ifuel;
unsat_core;
`Int query_elapsed_time;
`String hash ] ->
let hash_opt = if hash <> "" then Some(hash) else None in
Some (mk_hint hint_name hint_index fuel ifuel unsat_core query_elapsed_time hash_opt)
| _ ->
raise Exit
) hints
}
| _ ->
raise Exit
)
with
| Exit ->
MalformedJson
| Sys_error _ ->
UnableToOpen

116 changes: 0 additions & 116 deletions ocaml/fstar-lib/FStar_Compiler_Util.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1137,122 +1137,6 @@ let return_execution_time f =
let t2 = Sys.time () in
(retv, 1000.0 *. (t2 -. t1))

(** Hints. *)
type hint = {
hint_name:string;
hint_index:Z.t;
fuel:Z.t;
ifuel:Z.t;
unsat_core:string list option;
query_elapsed_time:Z.t;
hash:string option
}

type hints = hint option list

type hints_db = {
module_digest:string;
hints: hints
}

type hints_read_result =
| HintsOK of hints_db
| MalformedJson
| UnableToOpen

let write_hints (filename: string) (hints: hints_db): unit =
let json = `List [
`String hints.module_digest;
`List (List.map (function
| None -> `Null
| Some { hint_name; hint_index; fuel; ifuel; unsat_core; query_elapsed_time; hash } ->
`List [
`String hint_name;
`Int (Z.to_int hint_index);
`Int (Z.to_int fuel);
`Int (Z.to_int ifuel);
(match unsat_core with
| None -> `Null
| Some strings ->
`List (List.map (fun s -> `String s) strings));
`Int (Z.to_int query_elapsed_time);
`String (match hash with | Some(h) -> h | _ -> "")
]
) hints.hints)
] in
let channel = open_out_bin filename in
BatPervasives.finally
(fun () -> close_out channel)
(fun channel -> Yojson.Safe.pretty_to_channel channel json)
channel

let read_hints (filename: string) : hints_read_result =
let mk_hint nm ix fuel ifuel unsat_core time hash_opt = {
hint_name = nm;
hint_index = Z.of_int ix;
fuel = Z.of_int fuel;
ifuel = Z.of_int ifuel;
unsat_core = begin
match unsat_core with
| `Null ->
None
| `List strings ->
Some (List.map (function
| `String s -> s
| _ -> raise Exit)
strings)
| _ ->
raise Exit
end;
query_elapsed_time = Z.of_int time;
hash = hash_opt
}
in
try
let chan = open_in filename in
let json = Yojson.Safe.from_channel chan in
close_in chan;
HintsOK (
match json with
| `List [
`String module_digest;
`List hints
] -> {
module_digest;
hints = List.map (function
| `Null -> None
| `List [ `String hint_name;
`Int hint_index;
`Int fuel;
`Int ifuel;
unsat_core;
`Int query_elapsed_time ] ->
(* This case is for dealing with old-style hint files
that lack a query-hashes field. We should remove this
case once we definitively remove support for old hints *)
Some (mk_hint hint_name hint_index fuel ifuel unsat_core query_elapsed_time None)
| `List [ `String hint_name;
`Int hint_index;
`Int fuel;
`Int ifuel;
unsat_core;
`Int query_elapsed_time;
`String hash ] ->
let hash_opt = if hash <> "" then Some(hash) else None in
Some (mk_hint hint_name hint_index fuel ifuel unsat_core query_elapsed_time hash_opt)
| _ ->
raise Exit
) hints
}
| _ ->
raise Exit
)
with
| Exit ->
MalformedJson
| Sys_error _ ->
UnableToOpen

(* Outside of this file the reference to FStar_Util.ref must use the following combinators *)
(* Export it at the end of the file so that we don't break other internal uses of ref *)
type 'a ref = 'a FStar_Monotonic_Heap.ref
Expand Down
Loading