From 30be1a608f53c187d0c35391894fbb26b129e6cb Mon Sep 17 00:00:00 2001 From: oojahooo Date: Wed, 5 Jun 2024 02:26:53 +0900 Subject: [PATCH] [Patron] clean up implementation for artifact --- src/absDiff.ml | 2 ++ src/absPat.ml | 23 +++++++++++++++++++++ src/bugPatDB.ml | 4 +++- src/chc.ml | 6 ++++++ src/patch.ml | 53 ++++++++++++++++++++++++++++++------------------- src/z3utils.ml | 1 + 6 files changed, 68 insertions(+), 21 deletions(-) diff --git a/src/absDiff.ml b/src/absDiff.ml index ef6d90c..3ada221 100644 --- a/src/absDiff.ml +++ b/src/absDiff.ml @@ -328,6 +328,8 @@ type t = | SDeleteLval of string * abs_node | SUpdateLval of string * abs_node * abs_node +let is_insert_stmt = function SInsertStmt _ -> true | _ -> false + let rec to_styp t = match t with | Cil.TVoid _ -> SVoid diff --git a/src/absPat.ml b/src/absPat.ml index 3b96373..b5f1568 100644 --- a/src/absPat.ml +++ b/src/absPat.ml @@ -164,6 +164,18 @@ let num_of_rels rels = F.asprintf "#Rels: %d, #DUEdges: %d" (Chc.cardinal rels) (Chc.filter Chc.Elt.is_duedge rels |> Chc.cardinal) +let gen_patpat abs_diff snk facts = + let n = "Node-00" in + if List.exists ~f:AbsDiff.is_insert_stmt abs_diff then + let e1 = "Exp-00" in + let e2 = "Exp-000" in + let e3 = "Exp-0000" in + let op = "BinOp-00" in + Chc.add (Chc.Elt.duedge n snk) facts + |> Chc.add (Chc.Elt.assume n e1) + |> Chc.add (Chc.Elt.binop e1 op e2 e3) + else Chc.singleton (Chc.Elt.cfpath n n) + let run maps dug patch_comps alarm_exps alarm_lvs src snk facts abs_diff = let errtrace = Chc.Elt.FuncApply @@ -178,6 +190,10 @@ let run maps dug patch_comps alarm_exps alarm_lvs src snk facts abs_diff = let pattern_in_numeral = Chc.Elt.Implies (abs_facts |> Chc.to_list, errtrace) in + let patpat = + Chc.Elt.Implies (gen_patpat abs_diff snk abs_facts |> Chc.to_list, errtrace) + |> Chc.Elt.numer2var |> Chc.singleton + in let snk_func = Utils.get_func_name_from_node snk in let alt_pc, alt_diff = find_alt_lvs snk_func facts patch_comps abs_diff in let alt_pat = @@ -191,13 +207,20 @@ let run maps dug patch_comps alarm_exps alarm_lvs src snk facts abs_diff = let alt_pattern_in_numeral = Chc.Elt.Implies (alt_facts |> Chc.to_list, errtrace) in + let alt_patpat = + Chc.Elt.Implies + (gen_patpat abs_diff snk alt_facts |> Chc.to_list, errtrace) + |> Chc.Elt.numer2var |> Chc.singleton + in [ ( alt_pattern_in_numeral |> Chc.singleton, alt_pattern_in_numeral |> Chc.Elt.numer2var |> Chc.singleton, + alt_patpat, alt_diff' ); ] in ( pattern_in_numeral |> Chc.singleton, pattern_in_numeral |> Chc.Elt.numer2var |> Chc.singleton, + patpat, abs_diff' ) :: alt_pat diff --git a/src/bugPatDB.ml b/src/bugPatDB.ml index 56077c7..2a01a8f 100644 --- a/src/bugPatDB.ml +++ b/src/bugPatDB.ml @@ -7,10 +7,12 @@ module Map = Stdlib.Map module Sys = Stdlib.Sys let preproc_using_pattern z3env maps src snk facts out_dir i - (pattern_in_numeral, pattern, diff) = + (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 diff --git a/src/chc.ml b/src/chc.ml index 366b9b0..17d6f31 100644 --- a/src/chc.ml +++ b/src/chc.ml @@ -183,6 +183,12 @@ module Elt = struct | Implies (cons, hd) -> Sexp.List (chc2sexp hd :: List.map ~f:chc2sexp cons) let duedge src dst = FuncApply ("DUEdge", [ numer src; numer dst ]) + let assume n e = FuncApply ("Assume", [ numer n; numer e ]) + + let binop e o e1 e2 = + FuncApply ("BinOpExp", [ numer e; numer o; numer e1; numer e2 ]) + + let cfpath src dst = FuncApply ("CFPath", [ numer src; numer dst ]) let is_rel = function FuncApply _ -> true | _ -> false let is_rule = function Implies _ -> true | _ -> false let is_duedge = function FuncApply ("DUEdge", _) -> true | _ -> false diff --git a/src/patch.ml b/src/patch.ml index 9ff1887..8b30b80 100644 --- a/src/patch.ml +++ b/src/patch.ml @@ -29,6 +29,11 @@ let match_once z3env cand_donor donor_dir buggy_maps donee_dir target_alarm ast |> 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 @@ -38,31 +43,39 @@ let match_once z3env cand_donor donor_dir buggy_maps donee_dir target_alarm ast let facts, (src, snk, _, _), target_maps = Parser.make_facts donee_dir target_alarm ast out_dir in - let status = + let is_bug = Chc.match_and_log z3env out_dir target_alarm target_maps facts src snk pattern in Maps.dump target_alarm target_maps out_dir; - if Option.is_some status then ( - 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 = 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 + if Option.is_some is_bug then + let is_pat = + Chc.match_and_log z3env out_dir target_alarm target_maps facts src snk + patpat 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 ()) + if Option.is_none is_pat then ( + 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 = 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" target_alarm; + Continue ()) else ( L.info "%s is Not Matched" target_alarm; Continue ()) diff --git a/src/z3utils.ml b/src/z3utils.ml index 81bc1f2..6d95bf5 100644 --- a/src/z3utils.ml +++ b/src/z3utils.ml @@ -136,6 +136,7 @@ let match_sort z3env s = | "Loc" -> z3env.loc | "Val" -> z3env.value | "Pos" -> z3env.int_sort + | "BinOp" -> z3env.binop_sort | _ -> z3env.node let numer_cnt = ref 24 (* for binop, unop *)