Skip to content

Commit

Permalink
[CN-Test-Gen] Synthesize code for bug replication
Browse files Browse the repository at this point in the history
  • Loading branch information
ZippeyKeys12 committed Mar 5, 2025
1 parent 8ab1a71 commit a4ef14d
Show file tree
Hide file tree
Showing 23 changed files with 1,784 additions and 24 deletions.
10 changes: 9 additions & 1 deletion backend/cn/bin/main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -602,6 +602,7 @@ let run_tests
coverage
disable_passes
trap
replicas
=
(* flags *)
Cerb_debug.debug_level := debug_level;
Expand Down Expand Up @@ -652,7 +653,8 @@ let run_tests
sized_null;
coverage;
disable_passes;
trap
trap;
replicas
}
in
TestGeneration.set_config config;
Expand Down Expand Up @@ -1293,6 +1295,11 @@ module Testing_flags = struct
let trap =
let doc = "Raise SIGTRAP on test failure" in
Arg.(value & flag & info [ "trap" ] ~doc)


let replicas =
let doc = "Attempt to synthesize C code to replicate bugs" in
Arg.(value & flag & info [ "replicas" ] ~doc)
end

module Seq_testing_flags = struct
Expand Down Expand Up @@ -1381,6 +1388,7 @@ let testing_cmd =
$ Testing_flags.coverage
$ Testing_flags.disable_passes
$ Testing_flags.trap
$ Testing_flags.replicas
in
let doc =
"Generates tests for all functions in [FILE] with CN specifications.\n\
Expand Down
6 changes: 6 additions & 0 deletions backend/cn/lib/bugExplanation/bugExplanation.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
module CF = Cerb_frontend
module A = CF.AilSyntax

let synthesize_replicators = Replicators.synthesize

let synthesize_shape_analyzers = ShapeAnalyzers.synthesize
14 changes: 14 additions & 0 deletions backend/cn/lib/bugExplanation/bugExplanation.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
module CF = Cerb_frontend
module A = CF.AilSyntax

val synthesize_replicators
: CF.GenTypes.genTypeCategory A.sigma ->
unit Mucore.file ->
Executable_spec_extract.instrumentation list ->
(A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list

val synthesize_shape_analyzers
: CF.GenTypes.genTypeCategory A.sigma ->
unit Mucore.file ->
Executable_spec_extract.instrumentation list ->
(A.sigma_declaration * CF.GenTypes.genTypeCategory A.sigma_function_definition) list
Loading

0 comments on commit a4ef14d

Please sign in to comment.