[patch] support incomplete UpdateStmt

src/absDiff.ml

@@ -319,7 +319,8 @@ type t =
   (* func name is not necessary *)
   | SInsertStmt of StrSet.t * abs_node list * StrSet.t
   | SDeleteStmt of string
-  | SUpdateStmt of StrSet.t * abs_node list * StrSet.t
+  | SUpdateStmt of StrSet.t * string * abs_node list * StrSet.t
+  | SUpdateGoToStmt of StrSet.t * abs_node list * StrSet.t
   | SInsertExp of string * abs_node list * abs_node list * abs_node list
   | SDeleteExp of string * abs_node
   | SUpdateExp of string * abs_node * abs_node
@@ -426,7 +427,8 @@ let subst_single_abs_diff o_lv n_lv adiff =
   match adiff with
   | SInsertStmt (b, ss, a) -> SInsertStmt (b, List.map ~f:subst ss, a)
   | SDeleteStmt _ -> adiff
-  | SUpdateStmt (b, ss, a) -> SUpdateStmt (b, List.map ~f:subst ss, a)
+  | SUpdateGoToStmt (b, ss, a) -> SUpdateGoToStmt (b, List.map ~f:subst ss, a)
+  | SUpdateStmt (b, s, ss, a) -> SUpdateStmt (b, s, List.map ~f:subst ss, a)
   | SInsertExp (s, b, es, a) ->
       SInsertExp
         (s, List.map ~f:subst b, List.map ~f:subst es, List.map ~f:subst a)
@@ -441,21 +443,24 @@ let subst_abs_diff o_lv n_lv = List.map ~f:(subst_single_abs_diff o_lv n_lv)
 
 let change_def_single nodes = function
   | SInsertStmt (_, ss, a) -> SInsertStmt (nodes, ss, a)
-  | SUpdateStmt (_, ss, a) -> SUpdateStmt (nodes, ss, a)
+  | SUpdateStmt (_, s, ss, a) -> SUpdateStmt (nodes, s, ss, a)
+  | SUpdateGoToStmt (_, ss, a) -> SUpdateGoToStmt (nodes, ss, a)
   | _ as ad -> ad
 
 let change_def nodes = List.map ~f:(change_def_single nodes)
 
 let change_use_single nodes = function
   | SInsertStmt (b, ss, _) -> SInsertStmt (b, ss, nodes)
-  | SUpdateStmt (b, ss, _) -> SUpdateStmt (b, ss, nodes)
+  | SUpdateStmt (b, s, ss, _) -> SUpdateStmt (b, s, ss, nodes)
+  | SUpdateGoToStmt (b, ss, _) -> SUpdateGoToStmt (b, ss, nodes)
   (* NOTE: Only InsertStmt is handled correctly *)
   | _ as ad -> ad
 
 let change_use nodes = List.map ~f:(change_use_single nodes)
 
 let change_exact_single node = function
   | SDeleteStmt _ -> SDeleteStmt node
+  | SUpdateStmt (b, _, ss, a) -> SUpdateStmt (b, node, ss, a)
   | SInsertExp (_, b, es, a) -> SInsertExp (node, b, es, a)
   | SDeleteExp (_, e) -> SDeleteExp (node, e)
   | SUpdateExp (_, e1, e2) -> SUpdateExp (node, e1, e2)
@@ -679,13 +684,23 @@ let mk_abs_action maps dug = function
         mk_abs_stmt func_name maps dug (s, StrSet.empty)
       in
       (SDeleteStmt (abs_stmt.ids |> StrSet.choose), patch_comps)
-  | D.UpdateStmt (func_name, before, ss, after) ->
+  | D.UpdateStmt (func_name, before, s, ss, after) ->
+      let abs_before = mk_dummy_abs_stmts maps before in
+      let abs_stmt_s, _ = mk_abs_stmt func_name maps dug (s, StrSet.empty) in
+      let abs_stmt_ss, patch_comps =
+        mk_abs_stmts func_name maps dug (ss, StrSet.empty)
+      in
+      let abs_after = mk_dummy_abs_stmts maps after in
+      ( SUpdateStmt
+          (abs_before, abs_stmt_s.ids |> StrSet.choose, abs_stmt_ss, abs_after),
+        patch_comps )
+  | D.UpdateGoToStmt (func_name, before, ss, after) ->
       let abs_before = mk_dummy_abs_stmts maps before in
       let abs_stmts, patch_comps =
         mk_abs_stmts func_name maps dug (ss, StrSet.empty)
       in
       let abs_after = mk_dummy_abs_stmts maps after in
-      (SUpdateStmt (abs_before, abs_stmts, abs_after), patch_comps)
+      (SUpdateGoToStmt (abs_before, abs_stmts, abs_after), patch_comps)
   | D.UpdateExp (func_name, s, e1, e2) ->
       (* NOTE: abs_stmt is exactly that one *)
       let abs_stmt = mk_dummy_abs_stmt maps s |> StrSet.choose in

src/ast.ml

@@ -349,6 +349,11 @@ let rec eq_stmt skind1 skind2 =
       true
   | _ -> false
 
+let eq_loc_stmt s1 s2 =
+    String.equal
+      (get_stmtLoc s1.skind |> s_location)
+      (get_stmtLoc s2.skind |> s_location)
+
 let eq_global glob1 glob2 =
   match (glob1, glob2) with
   | Cil.GFun (func_info1, _), Cil.GFun (func_info2, _) ->

src/diff.ml

@@ -40,7 +40,10 @@ type t =
   | DeleteStmt of string * Cil.stmt
   (* Only use update stmt when goto is deleted and new stmt is inserted *)
   (* func name * orig before stmts (until goto) * new stmts * orig after stmts *)
-  | UpdateStmt of string * Cil.stmt list * Cil.stmt list * Cil.stmt list
+  | UpdateGoToStmt of string * Cil.stmt list * Cil.stmt list * Cil.stmt list
+  (* func name * orig before stmts * old stmt * new stmts * orig after stmts *)
+  | UpdateStmt of
+      string * Cil.stmt list * Cil.stmt * Cil.stmt list * Cil.stmt list
   (* func name * target stmt (may be call exp) * orig before exps * new exps * orig after exps *)
   | InsertExp of string * Cil.stmt * Cil.exp list * Cil.exp list * Cil.exp list
   (* func name * target stmt * deleted exps *)
@@ -91,11 +94,22 @@ let pp_diff ~simple fmt action =
       F.fprintf fmt "Function: %s\n" func;
       F.fprintf fmt "Diff Summary:\n";
       F.fprintf fmt "Deleted:%s\n" (Ast.s_stmt s)
-  | UpdateStmt (func, before, ss, after) ->
+  | UpdateStmt (func, before, s, ss, after) ->
       F.fprintf fmt "\tUpdateStmt: \n";
       F.fprintf fmt "Function: %s\n" func;
       if simple then F.fprintf fmt "# of Before:%i\n" (List.length before)
       else F.fprintf fmt "Before:%s\n" (lst2strlines Ast.s_stmt before);
+      F.fprintf fmt "From:%s\n" (Ast.s_stmt s);
+      if simple then F.fprintf fmt "# of After:%i\n" (List.length after)
+      else F.fprintf fmt "After:%s\n" (lst2strlines Ast.s_stmt after);
+      F.fprintf fmt "Diff Summary:\n";
+      F.fprintf fmt "UpdateFrom:%s\n" (Ast.s_stmt s);
+      F.fprintf fmt "UpdateTo:%s\n" (lst2strlines Ast.s_stmt ss)
+  | UpdateGoToStmt (func, before, ss, after) ->
+      F.fprintf fmt "\tUpdateGoToStmt: \n";
+      F.fprintf fmt "Function: %s\n" func;
+      if simple then F.fprintf fmt "# of Before:%i\n" (List.length before)
+      else F.fprintf fmt "Before:%s\n" (lst2strlines Ast.s_stmt before);
       if simple then F.fprintf fmt "# of After:%i\n" (List.length after)
       else F.fprintf fmt "After:%s\n" (lst2strlines Ast.s_stmt after);
       F.fprintf fmt "Diff Summary:\n";
@@ -364,7 +378,7 @@ and get_followup_diff_stmt func_name prnt_brnch depth hd1 hd2 tl1 tl2 before =
     if List.is_empty deleted_stmts then
       let env = mk_diff_env depth prnt_brnch prev_node in
       if Ast.is_cil_goto hd1.skind then
-        [ (UpdateStmt (func_name, before, [ hd2 ], tl1), env) ]
+        [ (UpdateGoToStmt (func_name, before, [ hd2 ], tl1), env) ]
       else
         [
           (DeleteStmt (func_name, hd1), env);
@@ -590,12 +604,28 @@ and fold_globals2 depth donor_gobals patch_globals left_sibs =
 
 let compare = compare
 
+let convert_to_update_stmt diff =
+  match diff with
+  | (InsertStmt (func, before, ss, after), env)
+    :: (DeleteStmt (func', s'), _)
+    :: _
+  | (DeleteStmt (func', s'), _)
+    :: (InsertStmt (func, before, ss, after), env)
+    :: _ ->
+      print_endline "check";
+      if List.hd_exn ss |> Ast.eq_loc_stmt s' then print_endline "true"
+      else print_endline "false";
+      if String.equal func func' && List.hd_exn ss |> Ast.eq_loc_stmt s' then
+        [ (UpdateStmt (func, before, s', ss, after), env) ]
+      else diff
+  | _ -> diff
+
 let define_diff out_dir buggy_file patch_file =
   let globs1, globs2 =
     ( H.remove_comments buggy_file.Cil.globals,
       H.remove_comments patch_file.Cil.globals )
   in
-  let diff = fold_globals2 0 globs1 globs2 [] in
+  let diff = fold_globals2 0 globs1 globs2 [] |> convert_to_update_stmt in
   let oc = Out_channel.create (Filename.concat out_dir "diff.txt") in
   let fmt = F.formatter_of_out_channel oc in
   pp_edit_script fmt diff;

src/diffJson.ml

@@ -79,12 +79,24 @@ let rec mk_json_obj saction =
       let action_json = ("action", `String "delete_stmt") in
       let change_json = ("change", `String s) in
       `Assoc [ action_json; change_json ]
-  | SUpdateStmt (before, ss, after) ->
+  | SUpdateStmt (before, s, ss, after) ->
       let action_json = ("action", `String "update_stmt") in
       let bn_id_lst = StrSet.fold (fun id l -> `String id :: l) before [] in
       let before_json = ("before", `List bn_id_lst) in
       let an_id_lst = StrSet.fold (fun id l -> `String id :: l) after [] in
       let after_json = ("after", `List an_id_lst) in
+      let change_from_json = ("from", `String s) in
+      let change_to_json = ("to", `List (List.map ~f:sstmt_to_json ss)) in
+      let change_json =
+        ("change", `Assoc [ change_from_json; change_to_json ])
+      in
+      `Assoc [ action_json; before_json; change_json; after_json ]
+  | SUpdateGoToStmt (before, ss, after) ->
+      let action_json = ("action", `String "update_goto_stmt") in
+      let bn_id_lst = StrSet.fold (fun id l -> `String id :: l) before [] in
+      let before_json = ("before", `List bn_id_lst) in
+      let an_id_lst = StrSet.fold (fun id l -> `String id :: l) after [] in
+      let after_json = ("after", `List an_id_lst) in
       let change_json = ("change", `List (List.map ~f:sstmt_to_json ss)) in
       `Assoc [ action_json; before_json; change_json; after_json ]
   | SUpdateExp (_, e1, e2) ->

src/doEdit.ml

@@ -216,7 +216,7 @@ class updateCallExpVisitor target_func from_stmt to_stmt =
   end
 
 let apply_insert_stmt ?(update = false) func_name before after ss donee =
-  if update then L.info "Applying UpdateStmt..."
+  if update then L.info "Applying UpdateGoToStmt..."
   else L.info "Applying InsertStmt...";
   is_patched := false;
   List.iter ~f:(fun s -> L.info "before:\n%s" (Ast.s_stmt s)) before;
@@ -229,6 +229,23 @@ let apply_insert_stmt ?(update = false) func_name before after ss donee =
   if not !is_patched then Logger.warn "failed to apply InsertStmt"
   else L.info "Successfully applied InsertStmt at %s" func_name
 
+let apply_update_stmt ?(update = false) func_name before s ss after donee =
+  L.info "Applying UpdateStmt...";
+  is_patched := false;
+  List.iter ~f:(fun s -> L.info "before:\n%s" (Ast.s_stmt s)) before;
+  let very_before = List.last before in
+  let very_after = if List.is_empty after then Some s else List.hd after in
+  if Option.is_none very_before && Option.is_none very_after then
+    L.warn "apply_update_stmt - cannot be patched";
+  let vis1 =
+    new insertStmtVisitor ~update func_name very_before very_after ss
+  in
+  Cil.visitCilFile vis1 donee;
+  let vis2 = new deleteStmtfromFuncVisitor func_name s in
+  Cil.visitCilFile vis2 donee;
+  if not !is_patched then Logger.warn "failed to apply UpdateStmt"
+  else L.info "Successfully applied UpdateStmt at %s" func_name
+
 let apply_delete_stmt func_name s donee =
   L.info "Applying DeleteStmt...";
   is_patched := false;
@@ -257,7 +274,9 @@ let apply_action donee = function
   | D.InsertStmt (func_name, before, ss, after) ->
       apply_insert_stmt func_name before after ss donee
   | D.DeleteStmt (func_name, s) -> apply_delete_stmt func_name s donee
-  | D.UpdateStmt (func_name, before, ss, after) ->
+  | D.UpdateStmt (func_name, before, s, ss, after) ->
+      apply_update_stmt func_name before s ss after donee
+  | D.UpdateGoToStmt (func_name, before, ss, after) ->
       apply_insert_stmt ~update:true func_name before after ss donee
   | D.UpdateExp (func_name, s, e1, e2) ->
       apply_update_exp func_name s e1 e2 donee

src/editFunction.ml

@@ -185,9 +185,22 @@ and translate_new_stmt maps sol_map = function
 let translate_new_stmts maps sol_map =
   List.map ~f:(fun abs_node -> translate_new_stmt maps sol_map abs_node.A.ast)
 
+(* TODO: add heuristic to find function translation *)
+let translate_func_name_alt sol_map abs_node_lst =
+  let patch_func =
+    abs_node_lst |> StrSet.choose |> Utils.get_func_name_from_node
+  in
+  Hashtbl.to_seq_keys sol_map
+  |> Seq.find (fun x -> String.is_prefix x ~prefix:patch_func)
+  |> Option.value_exn |> Utils.get_func_name_from_node
+
 let translate_func_name sol_map abs_node_lst =
-  abs_node_lst |> translate_ids sol_map |> StrSet.choose
-  |> Utils.get_func_name_from_node
+  let translated_nodes = abs_node_lst |> translate_ids sol_map in
+  let translated_node =
+    try StrSet.choose translated_nodes
+    with _ -> translate_func_name_alt sol_map abs_node_lst
+  in
+  Utils.get_func_name_from_node translated_node
 
 let translate_orig_stmts maps sol_map abs_nodes =
   let new_asts = abs_nodes |> translate_ids sol_map |> ids2asts maps in
@@ -215,15 +228,28 @@ let translate_delete_stmt maps sol_map s =
   in
   D.DeleteStmt (target_func_name, new_s)
 
-let translate_update_stmt maps sol_map before after ss =
+let translate_update_stmt maps sol_map before after s ss =
+  let target_before = translate_orig_stmts maps sol_map before in
+  let target_after = translate_orig_stmts maps sol_map after in
+  let target_func_name =
+    translate_func_name sol_map
+      (if List.is_empty target_before then after else before)
+  in
+  let new_ss = translate_new_stmts maps sol_map ss in
+  let new_s =
+    translate_orig_stmts maps sol_map (StrSet.singleton s) |> List.hd_exn
+  in
+  D.UpdateStmt (target_func_name, target_before, new_s, new_ss, target_after)
+
+let translate_update_goto_stmt maps sol_map before after ss =
   let target_before = translate_orig_stmts maps sol_map before in
   let target_after = translate_orig_stmts maps sol_map after in
   let target_func_name =
     translate_func_name sol_map
       (if List.is_empty target_before then after else before)
   in
   let new_ss = translate_new_stmts maps sol_map ss in
-  D.UpdateStmt (target_func_name, target_before, new_ss, target_after)
+  D.UpdateGoToStmt (target_func_name, target_before, new_ss, target_after)
 
 let translate_update_exp maps sol_map s e1 e2 =
   let target_func_name = translate_func_name sol_map (StrSet.singleton s) in
@@ -255,8 +281,10 @@ let translate cand_donor maps out_dir target_alarm abs_diff =
       | A.SInsertStmt (before, ss, after) ->
           translate_insert_stmt maps sol_map before after ss
       | A.SDeleteStmt s -> translate_delete_stmt maps sol_map s
-      | A.SUpdateStmt (before, ss, after) ->
-          translate_update_stmt maps sol_map before after ss
+      | A.SUpdateStmt (before, s, ss, after) ->
+          translate_update_stmt maps sol_map before after s ss
+      | A.SUpdateGoToStmt (before, ss, after) ->
+          translate_update_goto_stmt maps sol_map before after ss
       | A.SUpdateExp (s, e1, e2) -> translate_update_exp maps sol_map s e1 e2
       | A.SUpdateCallExp (s, s2) -> translate_update_callexp maps sol_map s s2
       | _ -> failwith "translate - not implemented")

src/main.ml

@@ -10,17 +10,17 @@ let db z3env inline_fns write_out donor_dir true_alarm db_dir out_dir =
       out_dir
   else L.error "No target directory specified"
 
-let patch z3env inline_fns db_dir donee_dir out_dir =
+let patch z3env inline_fns db_dir donee_dir out_dir cmd =
   if exist_all [ donee_dir; out_dir ] then
-    Patch.run ~db:true z3env inline_fns db_dir donee_dir out_dir
+    Patch.run ~db:true z3env inline_fns db_dir donee_dir out_dir cmd
   else L.error "No target directory specified"
 
-let dtd z3env inline_fns write_out donor_dir donee_dir true_alarm out_dir =
+let dtd z3env inline_fns write_out donor_dir donee_dir true_alarm out_dir cmd =
   let buggy_dir = Filename.concat donor_dir "bug" in
   let patch_dir = Filename.concat donor_dir "patch" in
   if exist_all [ buggy_dir; patch_dir; donor_dir ] then
     PatMat.run z3env inline_fns write_out true_alarm buggy_dir patch_dir
-      donee_dir out_dir
+      donee_dir out_dir cmd
   else L.error "No target directory specified"
 
 let main () =
@@ -39,9 +39,10 @@ let main () =
         options.true_alarm options.db_dir options.out_dir
   | Patch ->
       patch z3env options.inline options.db_dir options.donee_dir
-        options.out_dir
+        options.out_dir options.Options.command
   | DonorToDonee ->
       dtd z3env options.inline options.write_out options.donor_dir
         options.donee_dir options.true_alarm options.out_dir
+        options.Options.command
 
 let _ = main ()

src/patMat.ml

@@ -68,7 +68,7 @@ let sort_rule_optimize ref deps =
   (lcs |> List.rev) @ (unsorted |> List.rev)
 
 let run z3env inline_funcs write_out true_alarm buggy_dir patch_dir donee_dir
-    out_dir =
+    out_dir cmd =
   BugPatDB.run z3env inline_funcs write_out true_alarm buggy_dir patch_dir
     out_dir;
-  Patch.run z3env inline_funcs "" donee_dir out_dir
+  Patch.run z3env inline_funcs "" donee_dir out_dir cmd