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.

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

Add cram tests for CFGs #1360

Merged
merged 25 commits into from
Feb 21, 2024
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
55c9e5d
Add CFG test using graph-easy
sim642 Feb 9, 2024
3093d27
Use locations in CFG test nodes
sim642 Feb 9, 2024
b8c6e64
Use stdout for CFG test
sim642 Feb 9, 2024
d13a432
Use function names in CFG tests
sim642 Feb 9, 2024
48d4b63
Add cram tests for CFG
sim642 Feb 9, 2024
6ed1aae
Move some functions to CfgTools
sim642 Feb 9, 2024
b727532
Test CFGs per function
sim642 Feb 9, 2024
a1483d6
Fix instructions in CFG testing
sim642 Feb 9, 2024
361af13
More detailed location output in CFG tests
sim642 Feb 9, 2024
9036370
Merge branch 'master' into cfg-test
sim642 Feb 13, 2024
e81df45
Add test for synthetic witness invariant locations (PR #758)
sim642 Feb 13, 2024
7018ccf
Add test for incorrect witness invariant locations from CIL transform…
sim642 Feb 13, 2024
b734f50
Update CIL for synthetic locations fix
sim642 Feb 13, 2024
65ae0f0
Add graph-easy Ubuntu depext
sim642 Feb 13, 2024
de83ccc
Try to pin using with-test in CI
sim642 Feb 13, 2024
4d86fd0
Add enabled_if to CFG tests in 00-sanity as well
sim642 Feb 13, 2024
d48e85e
Try to pin using with-test in CI via opam-depext-flags
sim642 Feb 13, 2024
4b58d45
Try to pin using with-test in CI via hack
sim642 Feb 13, 2024
ae5b2cf
Install graph-easy manually in CI because nothing works
sim642 Feb 13, 2024
15e8ca3
Install graph-easy only on Ubuntu in CI
sim642 Feb 13, 2024
d146e9b
Update GobView for moved compute_cfg
sim642 Feb 14, 2024
b730994
Comment about depext --with-test
sim642 Feb 21, 2024
45e01c3
Extract CilCfg0
sim642 Feb 21, 2024
3f20225
Remove commented-out CilLocation.get_labelsLoc
sim642 Feb 21, 2024
5e65e22
Merge branch 'master' into cfg-test
sim642 Feb 21, 2024
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
Prev Previous commit
Next Next commit
Move some functions to CfgTools
  • Loading branch information
sim642 committed Feb 9, 2024
commit 6ed1aae9f5aadb39cc157831bb722c9ee878d726
6 changes: 6 additions & 0 deletions src/common/framework/cfgTools.ml
Original file line number Diff line number Diff line change
Expand Up @@ -620,6 +620,12 @@ let getCFG (file: file) : cfg * cfg * stmt list CfgEdgeH.t =
if get_bool "justcfg" then fprint_hash_dot cfgB;
(fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n []), skippedByEdge

let compute_cfg_skips file =
let cfgF, cfgB, skippedByEdge = getCFG file in
(module struct let prev = cfgB let next = cfgF end : CfgBidir), skippedByEdge

let compute_cfg file = fst (compute_cfg_skips file)


let iter_fd_edges (module Cfg : CfgBackward) fd =
let ready = NH.create 113 in
Expand Down
8 changes: 1 addition & 7 deletions src/framework/control.ml
Original file line number Diff line number Diff line change
Expand Up @@ -811,15 +811,9 @@ let rec analyze_loop (module CFG : CfgBidir) file fs change_info skippedByEdge =
(* TODO: do some more incremental refinement and reuse parts of solution *)
analyze_loop (module CFG) file fs change_info skippedByEdge

let compute_cfg_skips file =
let cfgF, cfgB, skippedByEdge = CfgTools.getCFG file in
(module struct let prev = cfgB let next = cfgF end : CfgBidir), skippedByEdge

let compute_cfg = fst % compute_cfg_skips

(** The main function to perform the selected analyses. *)
let analyze change_info (file: file) fs =
if (get_bool "dbg.verbose") then print_endline "Generating the control flow graph.";
let (module CFG), skippedByEdge = compute_cfg_skips file in
let (module CFG), skippedByEdge = CfgTools.compute_cfg_skips file in
MyCFG.current_cfg := (module CFG);
analyze_loop (module CFG) file fs change_info skippedByEdge