[AbsDiff] add SLoop

src/absDiff.ml

@@ -91,6 +91,7 @@ and abs_lval = SLNull | Lval of abs_lhost * abs_offset
 and abs_stmt =
   | SSNull
   | SIf of abs_node * abs_node list * abs_node list
+  | SLoop of abs_node list
   | SSet of abs_node * abs_node
   | SCall of abs_node option * abs_node * abs_node list
   | SReturn of abs_node option
@@ -139,6 +140,7 @@ and pp_absstmt fmt s =
   | SIf (e, s1, s2) ->
       Format.fprintf fmt "SIf(%a, %a, %a)" pp_node e pp_node_lst s1 pp_node_lst
         s2
+  | SLoop ss -> Format.fprintf fmt "SLoop(%a)" pp_node_lst ss
   | SSet (l, e) -> Format.fprintf fmt "SSet(%a, %a)" pp_node l pp_node e
   | SCall (l, e, es) ->
       Format.fprintf fmt "SCall(%a, %a, %a)" pp_soptlval l pp_node e pp_node_lst
@@ -276,6 +278,7 @@ let rec subst_abs_stmt o_lv n_lv astmt =
   match astmt with
   | SSNull | SBreak | SContinue -> astmt
   | SIf (e, s1, s2) -> SIf (subst e, List.map ~f:subst s1, List.map ~f:subst s2)
+  | SLoop ss -> SLoop (List.map ~f:subst ss)
   | SSet (l, e) -> SSet (subst l, subst e)
   | SCall (l, e, es) ->
       SCall (Option.(l >>| subst), subst e, List.map ~f:subst es)
@@ -601,6 +604,11 @@ and mk_abs_stmt func_name maps dug (s, pc) =
           mk_abs_stmts func_name maps dug (s2.Cil.bstmts, pc2)
         in
         (SIf (abs_exp_node, abs_stmt_node1, abs_stmt_node2), pc3)
+    | Cil.Loop (b, _, _, _) ->
+        let abs_stmts_node, pc1 =
+          mk_abs_stmts func_name maps dug (b.bstmts, pc)
+        in
+        (SLoop abs_stmts_node, pc1)
     | Cil.Instr il -> mk_abs_instr func_name maps dug (List.hd_exn il, pc)
     | Cil.Block b ->
         let abs_stmts_node, pc1 =
@@ -618,7 +626,7 @@ and mk_abs_stmt func_name maps dug (s, pc) =
         (SGoto { ids; ast; literal }, pc)
     | Cil.Break _ -> (SBreak, pc)
     | Cil.Continue _ -> (SContinue, pc)
-    | _ -> L.error "mk_abs_stmt - not implemented"
+    | _ -> L.error "mk_abs_stmt - not implemented: %s" (Ast.s_stmt s)
   in
   let ast = AbsStmt (abs_stmt, s) in
   let literal = Ast.s_stmt s in

src/editFunction.ml

@@ -116,16 +116,10 @@ and translate_exp maps sol_map = function
 let rec translate_if_stmt maps sol_map scond sthen_block selse_block =
   let cond = translate_exp maps sol_map scond.A.ast in
   let then_block =
-    List.fold_left
-      ~f:(fun acc ss -> translate_new_stmt maps sol_map ss.A.ast :: acc)
-      ~init:[] sthen_block
-    |> List.rev
+    List.map ~f:(fun ss -> translate_new_stmt maps sol_map ss.A.ast) sthen_block
   in
   let else_block =
-    List.fold_left
-      ~f:(fun acc ss -> translate_new_stmt maps sol_map ss.A.ast :: acc)
-      ~init:[] selse_block
-    |> List.rev
+    List.map ~f:(fun ss -> translate_new_stmt maps sol_map ss.A.ast) selse_block
   in
   Cil.mkStmt
     (Cil.If
@@ -164,11 +158,18 @@ and translate_instr maps sol_map abs_instr i =
          %s"
         AbsDiff.pp_absstmt a (Ast.s_instr i)
 
+and translate_loop maps sol_map sb =
+  let block =
+    List.map ~f:(fun ss -> translate_new_stmt maps sol_map ss.A.ast) sb
+  in
+  Cil.mkStmt (Cil.Loop (Cil.mkBlock block, Cil.locUnknown, None, None))
+
 and translate_new_stmt maps sol_map = function
   | A.AbsStmt (sym, cil) -> (
       match (sym, cil.Cil.skind) with
       | A.SIf (scond, sthen_block, selse_block), Cil.If _ ->
           translate_if_stmt maps sol_map scond sthen_block selse_block
+      | A.SLoop sb, Cil.Loop _ -> translate_loop maps sol_map sb
       | A.SReturn (Some sym), Cil.Return _ ->
           let exp = translate_exp maps sol_map sym.A.ast in
           Cil.mkStmt (Cil.Return (Some exp, Cil.locUnknown))