Skip to content

Commit

Permalink
Make YAML output buffer sizing exponential
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Nov 17, 2023
1 parent b57e80d commit f709482
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 7 deletions.
11 changes: 11 additions & 0 deletions src/util/std/gobYaml.ml
Original file line number Diff line number Diff line change
@@ -1,3 +1,14 @@
let to_string' ?(len=65535 * 4) ?encoding ?scalar_style ?layout_style v =
assert (len >= 1);
let rec aux len =
match Yaml.to_string ~len ?encoding ?scalar_style ?layout_style v with
| Ok _ as o -> o
| Error (`Msg ("scalar failed" | "doc_end failed")) when len < Sys.max_string_length / 2 ->
aux (len * 2)
| Error (`Msg _) as e -> e
in
aux len

include Yaml.Util

include GobResult.Syntax
Expand Down
13 changes: 6 additions & 7 deletions src/witness/yamlWitness.ml
Original file line number Diff line number Diff line change
Expand Up @@ -143,12 +143,11 @@ struct
}
end

let yaml_entries_to_file ?(invariants=0) yaml_entries file =
let yaml_entries_to_file yaml_entries file =
let yaml = `A yaml_entries in
(* Yaml_unix.to_file_exn file yaml *)
(* to_file/to_string uses a fixed-size buffer... *)
(* estimate how big it should be + extra in case empty *)
let text = match Yaml.to_string ~len:((List.length yaml_entries + invariants) * 8192 + 2048) yaml with
let text = match GobYaml.to_string' yaml with
| Ok text -> text
| Error (`Msg m) -> failwith ("Yaml.to_string: " ^ m)
in
Expand Down Expand Up @@ -432,7 +431,7 @@ struct
in

(* Generate invariant set *)
let (entries, invariants) =
let entries =
if entry_type_enabled YamlWitnessType.InvariantSet.entry_type then (
let invariants = [] in

Expand Down Expand Up @@ -503,10 +502,10 @@ struct

let invariants = List.rev invariants in
let entry = Entry.invariant_set ~task ~invariants in
(entry :: entries, List.length invariants)
entry :: entries
)
else
(entries, 0)
entries
in

let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in (* reverse to make entries in file in the same order as generation messages *)
Expand All @@ -515,7 +514,7 @@ struct
(Pretty.dprintf "total generation entries: %d" (List.length yaml_entries), None);
];

yaml_entries_to_file ~invariants yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"))
yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"))

let write () =
Timing.wrap "yaml witness" write ()
Expand Down

0 comments on commit f709482

Please sign in to comment.