Fetch UnsatCoreTAC files via unsat_core_map.json instead of the whole archive#2
Fetch UnsatCoreTAC files via unsat_core_map.json instead of the whole archive#2jar-ben wants to merge 3 commits into
Conversation
jar-ben
changed the title
| Fetch statsdata.json for a job via Lambda. | ||
| """Fetch statsdata.json for a job via Lambda.""" | ||
| try: | ||
| return cast(Dict[str, Any], json.loads(self.fetch_output_file(job_identifier, "statsdata.json"))) |
There was a problem hiding this comment.
TIOLI: are we sure we want to load it all to memory? iirc statsdata.json can get pretty big
There was a problem hiding this comment.
We already did that before this PR. I don't want to change the interface (the return type of this function). I don't need fetch_statsdata for my current efforts, I am just simplifying the code since I have added fetch_output_file.
Though, note that my change actually improves things - the peak memory is reduced by ~29% when calling fetch_statsdata (based on some measurements I made).
| dest_dir.mkdir(parents=True, exist_ok=True) | ||
| tar_content = self._fetch_outputs_cached(job_identifier) | ||
| extracted: List[Path] = [] | ||
| with tarfile.open(fileobj=io.BytesIO(tar_content), mode="r:gz") as tar: |
There was a problem hiding this comment.
worth checking - this does not open the whole thing in memory?
There was a problem hiding this comment.
Well, this was preexisting before this PR - we were fetching the whole tar to extract the unsat core files. Now, we fetch only the unsat core files and avoid fetching the whole tar - it is done via the unsat_core_map which depends on a change on the prover side (not released yet). So, for backward compatibility, we keep also the original "whole tar" approach.
I don't see a regression here, only improvement if the user will run with a new prover version.
shellygr
left a comment
shellygr
left a comment
There was a problem hiding this comment.
lgtm, two memory related nits
|
also - what is the rule_id? |
It's a unique rule identifier. We added it to the prover already some time ago, but it was not exported. There is a prover PR that exports it to treeView (which allows us to match treeView items (rule&method results) to corresponding unsat core files). |
2 participants
Uses the job's
unsat_core_map.json({ ruleId -> [UnsatCoreTAC .txt] }) to fetch onlythe referenced files via the per-file endpoint, instead of pulling the full output tar.
fetch_output_file(job, rel_path)— fetch oneReports/-relative file via the/f/<name>endpoint (added to all fetchers).
fetch_statsdatanow delegates to it.unsat_core_map/unsat_core_filenames/read_unsat_cores— look up a rule's unsat-core.txtfiles (and their contents) by its treeViewruleId.extract_unsat_core_files— fetches only the mapped files; falls back to the output tar whenthe map is absent.
CheckResult.rule_id(parsed from the treeView node) andNodeStatus.SANITY_FAILED.Consumer flow: parse the treeView, select rules by status, then fetch their
.txtbyrule_id.Works for any rule with unsat cores (verified, failed
satisfy, or vacuous), not just sanity.