Skip to content

Commit

Permalink
[absPat] add full pattern
Browse files Browse the repository at this point in the history
  • Loading branch information
@spearo2
spearo2 committed Oct 15, 2024
1 parent 4b7926b commit d562386
Show file tree
Hide file tree
Showing 5 changed files with 201 additions and 108 deletions.
97 changes: 89 additions & 8 deletions src/absPat.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -244,6 +244,65 @@ let abs_by_comps ?(new_ad = false) maps dug patch_comps snk alarm_exps alarm_lvs
|> Chc.remove_detached_edges,
if new_ad then abs_diff' else abs_diff )

let get_ast_rels_by_node dug node =
let node_info = Dug.info_of_v dug node in
node_info.Dug.rels

let get_src_rels dug src edges =
let src_asts = get_ast_rels_by_node dug src in
let src_duedge = List.hd_exn edges |> Dug.edge2rel in
( Chc.filter
(fun c ->
match c with
| Chc.Elt.FuncApply ("Set", _)
| Chc.Elt.FuncApply ("CallExp", _)
| Chc.Elt.FuncApply ("ReadCallExp", _)
| Chc.Elt.FuncApply ("LibCallExp", _)
| Chc.Elt.FuncApply ("AllocExp", _) ->
true
| _ -> false)
src_asts
|> Chc.add src_duedge,
List.tl_exn edges )

let filter_interesting_rels duedge rels =
if
Chc.exists
(fun c ->
match c with
| Chc.Elt.FuncApply ("BinOpExp", _)
| Chc.Elt.FuncApply ("ReadCallExp", _)
| Chc.Elt.FuncApply ("LibCallExp", _)
| Chc.Elt.FuncApply ("AllocExp", _)
| Chc.Elt.FuncApply ("CallExp", _) ->
true
| _ -> false)
rels
then Chc.add duedge rels
else Chc.empty

let mk_complete_pat maps dug patch_comps src snk alarm_exps alarm_lvs facts
abs_diff cmd =
let abs_facts, abs_diff' =
abs_by_comps maps dug patch_comps snk alarm_exps alarm_lvs facts abs_diff
cmd
in
let edges = Dug.shortest_path dug src snk in
let src_rels, edges' = get_src_rels dug src edges in
let full_facts =
List.fold ~init:src_rels
~f:(fun acc edge ->
let src_node = Dug.I.E.src edge in
let duedge = Dug.edge2rel edge in
let filtered_rels =
get_ast_rels_by_node dug src_node |> filter_interesting_rels duedge
in
Chc.union filtered_rels acc)
edges'
|> Chc.union abs_facts
in
(full_facts, abs_facts, abs_diff')

let num_of_rels rels =
F.asprintf "#Rels: %d, #DUEdges: %d" (Chc.cardinal rels)
(Chc.filter Chc.Elt.is_duedge rels |> Chc.cardinal)
Expand Down Expand Up @@ -393,9 +452,17 @@ let run maps dug patch_comps alarm_exps alarm_lvs src snk facts abs_diff cmd =
in
Z3env.buggy_src := src;
Z3env.buggy_snk := snk;
let abs_facts, abs_diff' =
abs_by_comps maps dug patch_comps snk alarm_exps alarm_lvs facts abs_diff
cmd
let full_facts, abs_facts, abs_diff' =
mk_complete_pat maps dug patch_comps src snk alarm_exps alarm_lvs facts
abs_diff cmd
in
L.info "Full Pattern - %s" (num_of_rels full_facts);
let full_pattern_in_numeral =
Chc.Elt.Implies (full_facts |> Chc.to_list, errtrace)
in
let full_patpat =
Chc.Elt.Implies (gen_patpat abs_diff snk full_facts |> Chc.to_list, errtrace)
|> Chc.Elt.numer2var |> Chc.singleton
in
L.info "Abstract Pattern - %s" (num_of_rels abs_facts);
let pattern_in_numeral =
Expand Down Expand Up @@ -430,8 +497,22 @@ let run maps dug patch_comps alarm_exps alarm_lvs src snk facts abs_diff cmd =
alt_diff' );
]
in
( pattern_in_numeral |> Chc.singleton,
pattern_in_numeral |> Chc.Elt.numer2var |> Chc.singleton,
patpat,
abs_diff' )
:: alt_pat
let full_pat =
( full_pattern_in_numeral |> Chc.singleton,
full_pattern_in_numeral |> Chc.Elt.numer2var |> Chc.singleton,
full_patpat,
abs_diff' )
in
let abs_pat =
( pattern_in_numeral |> Chc.singleton,
pattern_in_numeral |> Chc.Elt.numer2var |> Chc.singleton,
patpat,
abs_diff' )
in
let is_altpat_eq_abspat =
Chc.fold
(fun elt acc ->
acc && Chc.exists (fun e -> Chc.Elt.equal e elt) abs_facts)
alt_pc true
in
(full_pat :: abs_pat :: alt_pat, not is_altpat_eq_abspat)
50 changes: 26 additions & 24 deletions src/bugPatDB.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,29 +6,31 @@ module Set = Stdlib.Set
module Map = Stdlib.Map
module Sys = Stdlib.Sys

let preproc_using_pattern z3env maps src snk facts out_dir i
let preproc_using_pattern is_altpat_useful z3env maps src snk facts out_dir i
(pattern_in_numeral, pattern, patpat, diff) =
let i_str = string_of_int i in
Chc.sexp_dump (Filename.concat out_dir "pattern_" ^ i_str) pattern;
Chc.pretty_dump (Filename.concat out_dir "pattern_" ^ i_str) pattern;
Chc.sexp_dump (Filename.concat out_dir "patch_pattern_" ^ i_str) patpat;
Chc.pretty_dump (Filename.concat out_dir "patch_pattern_" ^ i_str) patpat;
Maps.dump "buggy" maps out_dir;
L.info "Try matching with buggy numeral...";
( Chc.match_and_log z3env out_dir ("buggy_numer_" ^ i_str) maps facts src snk
pattern_in_numeral
|> fun status -> assert (Option.is_some status) );
Maps.dump ("buggy_numer_" ^ i_str) maps out_dir;
let src_oc = Filename.concat out_dir "src" in
Out_channel.write_all src_oc ~data:src;
let snk_oc = Filename.concat out_dir "snk" in
Out_channel.write_all snk_oc ~data:snk;
let diff_oc =
Filename.concat out_dir ("abs_diff_" ^ i_str ^ ".marshal")
|> Out_channel.create
in
Marshal.to_channel diff_oc diff [];
Out_channel.close diff_oc
if is_altpat_useful then (
let i_str = string_of_int i in
Chc.sexp_dump (Filename.concat out_dir "pattern_" ^ i_str) pattern;
Chc.pretty_dump (Filename.concat out_dir "pattern_" ^ i_str) pattern;
Chc.sexp_dump (Filename.concat out_dir "patch_pattern_" ^ i_str) patpat;
Chc.pretty_dump (Filename.concat out_dir "patch_pattern_" ^ i_str) patpat;
Maps.dump "buggy" maps out_dir;
L.info "Try matching with buggy numeral...";
( Chc.match_and_log z3env out_dir ("buggy_numer_" ^ i_str) maps facts src
snk pattern_in_numeral
|> fun status -> assert (Option.is_some status) );
Maps.dump ("buggy_numer_" ^ i_str) maps out_dir;
let src_oc = Filename.concat out_dir "src" in
Out_channel.write_all src_oc ~data:src;
let snk_oc = Filename.concat out_dir "snk" in
Out_channel.write_all snk_oc ~data:snk;
let diff_oc =
Filename.concat out_dir ("abs_diff_" ^ i_str ^ ".marshal")
|> Out_channel.create
in
Marshal.to_channel diff_oc diff [];
Out_channel.close diff_oc)
else L.info "No useful alternative pattern found."

let run z3env inline_funcs write_out true_alarm buggy_dir patch_dir out_dir cmd
=
Expand All @@ -51,12 +53,12 @@ let run z3env inline_funcs write_out true_alarm buggy_dir patch_dir out_dir cmd
if write_out then (
L.info "Writing out the edit script...";
DiffJson.dump abs_diff out_dir);
let patterns =
let patterns, is_altpat_useful =
AbsPat.run maps dug patch_comps alarm_exps alarm_lvs src snk facts abs_diff
cmd
in
L.info "Making Bug Pattern is done";
List.iteri
~f:(preproc_using_pattern z3env maps src snk facts out_dir)
~f:(preproc_using_pattern is_altpat_useful z3env maps src snk facts out_dir)
patterns;
L.info "Preprocessing with pattern is done."
5 changes: 5 additions & 0 deletions src/dug.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,11 @@ let is_skip_node cmd_map n =
| Maps.Skip _ | Maps.Assume _ -> true
| _ -> false

let edge2rel (edge : W.edge) =
let src = I.E.src edge in
let dst = I.E.dst edge in
Chc.Elt.duedge src dst

let of_facts lval_map cmd_map rels =
let module NodeSet = Set.Make (String) in
let du_rels, ast_rels = Chc.partition Chc.Elt.is_duedge rels in
Expand Down
22 changes: 9 additions & 13 deletions src/parser.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -133,19 +133,15 @@ let expand_edges src dst duedges skip_set assume_set cmd_map =

let connect_true_duedges (cmd_map : (string, Maps.cmd) Hashtbl.t) chc =
let assume_set, skip_set, duedges = Chc.partition_to_filter chc cmd_map in
Chc.cardinal duedges |> L.info "Before: %d";
let t =
Chc.fold
(fun elt acc ->
match elt with
| Chc.Elt.FuncApply ("DUEdge", [ src; dst ]) ->
expand_edges src dst duedges skip_set assume_set cmd_map
|> Chc.union acc
| _ -> acc)
duedges Chc.empty
in
Chc.cardinal t |> L.info "After: %d";
Chc.union chc t
Chc.fold
(fun elt acc ->
match elt with
| Chc.Elt.FuncApply ("DUEdge", [ src; dst ]) ->
expand_edges src dst duedges skip_set assume_set cmd_map
|> Chc.union acc
| _ -> acc)
duedges Chc.empty
|> Chc.union chc

let file2func = function
| "AllocExp.facts" -> "AllocExp"
Expand Down
135 changes: 72 additions & 63 deletions src/patch.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,73 +23,82 @@ let mk_file_diff orig_path patch_path cand_donor target_alarm out_dir =

let match_once z3env cand_donor donor_dir buggy_maps target_maps
(donee_facts, donee_src, donee_snk) target_alarm ast out_dir i cmd =
let src_ic = Filename.concat donor_dir "src" in
Z3env.buggy_src := In_channel.read_all src_ic;
let snk_ic = Filename.concat donor_dir "snk" in
Z3env.buggy_snk := In_channel.read_all snk_ic;
let pattern =
match
F.asprintf "pattern_%d_mach.chc" i
|> Filename.concat donor_dir |> Parser.parse_chc
|> Chc.map Chc.Elt.numer2var
in
let patpat =
F.asprintf "patch_pattern_%d_mach.chc" i
|> Filename.concat donor_dir |> Parser.parse_chc
|> Chc.map Chc.Elt.numer2var
in
let cdp_ic =
F.asprintf "abs_diff_%d.marshal" i
|> Filename.concat donor_dir |> In_channel.create
in
let diff = Marshal.from_channel cdp_ic in
In_channel.close cdp_ic;
L.info "Pattern Matching on %d-th level pattern" i;
L.info "First, trying to match %s with bug pattern" target_alarm;
let is_bug =
Chc.match_and_log z3env out_dir target_alarm target_maps donee_facts
donee_src donee_snk pattern
in
Maps.dump target_alarm target_maps out_dir;
if Option.is_some is_bug then
let is_pat =
L.info "%s is Matched with bug pattern" target_alarm;
L.info "Now, trying to match %s with patch pattern" target_alarm;
match cmd with
| Options.DonorToDonee -> None
| _ ->
Chc.match_and_log z3env out_dir target_alarm target_maps donee_facts
donee_src donee_snk patpat
in
if Option.is_none is_pat then (
L.info "%s is not Matched with patch pattern (Good)" target_alarm;
Modeling.match_ans buggy_maps target_maps target_alarm i cand_donor
donor_dir out_dir;
L.info "Matching with %s is done" target_alarm;
let target_diff =
EditFunction.translate cand_donor target_maps out_dir target_alarm diff
|> Filename.concat donor_dir |> Sys_unix.file_exists
with
| `No | `Unknown -> Continue ()
| `Yes ->
let src_ic = Filename.concat donor_dir "src" in
Z3env.buggy_src := In_channel.read_all src_ic;
let snk_ic = Filename.concat donor_dir "snk" in
Z3env.buggy_snk := In_channel.read_all snk_ic;
let pattern =
F.asprintf "pattern_%d_mach.chc" i
|> Filename.concat donor_dir |> Parser.parse_chc
|> Chc.map Chc.Elt.numer2var
in
L.info "Applying patch on the target file ...";
let out_file_orig =
F.asprintf "%s/orig_%s_%s_%d.c" out_dir cand_donor target_alarm i
let patpat =
F.asprintf "patch_pattern_%d_mach.chc" i
|> Filename.concat donor_dir |> Parser.parse_chc
|> Chc.map Chc.Elt.numer2var
in
DoEdit.write_out out_file_orig ast;
let patch_file =
Ast.extract_snk_stmt target_maps.ast_map donee_snk
|> DoEdit.run ast target_diff
let cdp_ic =
F.asprintf "abs_diff_%d.marshal" i
|> Filename.concat donor_dir |> In_channel.create
in
let out_file_patch =
F.asprintf "%s/patch_%s_%s_%d.c" out_dir cand_donor target_alarm i
let diff = Marshal.from_channel cdp_ic in
In_channel.close cdp_ic;
L.info "Pattern Matching on %d-th level pattern" i;
L.info "First, trying to match %s with bug pattern" target_alarm;
let is_bug =
Chc.match_and_log z3env out_dir target_alarm target_maps donee_facts
donee_src donee_snk pattern
in
DoEdit.write_out out_file_patch patch_file;
L.info "Patch for %s is done, written at %s" target_alarm out_file_patch;
mk_file_diff out_file_orig out_file_patch cand_donor target_alarm out_dir;
Stop ())
else (
L.info "%s is Matched with patch pattern (Bad)" target_alarm;
Continue ())
else (
L.info "%s is Not Matched with bug pattern" target_alarm;
Continue ())
Maps.dump target_alarm target_maps out_dir;
if Option.is_some is_bug then
let is_pat =
L.info "%s is Matched with bug pattern" target_alarm;
L.info "Now, trying to match %s with patch pattern" target_alarm;
match cmd with
| Options.DonorToDonee -> None
| _ ->
Chc.match_and_log z3env out_dir target_alarm target_maps
donee_facts donee_src donee_snk patpat
in
if Option.is_none is_pat then (
L.info "%s is not Matched with patch pattern (Good)" target_alarm;
Modeling.match_ans buggy_maps target_maps target_alarm i cand_donor
donor_dir out_dir;
L.info "Matching with %s is done" target_alarm;
let target_diff =
EditFunction.translate cand_donor target_maps out_dir target_alarm
diff
in
L.info "Applying patch on the target file ...";
let out_file_orig =
F.asprintf "%s/orig_%s_%s_%d.c" out_dir cand_donor target_alarm i
in
DoEdit.write_out out_file_orig ast;
let patch_file =
Ast.extract_snk_stmt target_maps.ast_map donee_snk
|> DoEdit.run ast target_diff
in
let out_file_patch =
F.asprintf "%s/patch_%s_%s_%d.c" out_dir cand_donor target_alarm i
in
DoEdit.write_out out_file_patch patch_file;
L.info "Patch for %s is done, written at %s" target_alarm
out_file_patch;
mk_file_diff out_file_orig out_file_patch cand_donor target_alarm
out_dir;
Stop ())
else (
L.info "%s is Matched with patch pattern (Bad)" target_alarm;
Continue ())
else (
L.info "%s is Not Matched with bug pattern" target_alarm;
Continue ())

let match_one_by_one ?(db = false) z3env bt_dir donee_dir target_alarm
inline_funcs out_dir cmd cand_donor =
Expand All @@ -109,7 +118,7 @@ let match_one_by_one ?(db = false) z3env bt_dir donee_dir target_alarm
~f:(fun _ i ->
match_once z3env cand_donor donor_dir buggy_maps target_maps
(facts, src, snk) target_alarm donee_ast out_dir i cmd)
[ 0; 1 ] ~finish:ignore
[ 0; 1; 2 ] ~finish:ignore

let match_one_alarm ?(db = false) z3env donee_dir inline_funcs out_dir db_dir
target_alarm cmd =
Expand Down

0 comments on commit d562386

Please sign in to comment.