[Patron] clean up implementation for artifact

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

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

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

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

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 ())

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 *)