Add asm goto support

goblint.opam

@@ -106,7 +106,7 @@ x-maintenance-intent: ["(latest)" "(latest).(latest-1)"]
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.1.0" "git+https://github.com/goblint/cil.git#76083d655d56e4c7791d457db57f0dd6461faf71" ]
+  [ "goblint-cil.2.1.0" "git+https://github.com/goblint/cil.git#107afe7aa44ab60590fed88841d9f811e91872cb" ]
   # pinned for performance (https://github.com/ocaml-batteries-team/batteries-included/pull/1149) via fork, remove after new batteries release (and then bump the batteries lower-bound accordingly)
   [ "batteries.3.11.0" "git+https://github.com/sim642/batteries-included.git#3920bdf614e4a12120fabfa2c97ee913cc246b13" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release

goblint.opam.locked

@@ -164,7 +164,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.1.0"
-    "git+https://github.com/goblint/cil.git#76083d655d56e4c7791d457db57f0dd6461faf71"
+    "git+https://github.com/goblint/cil.git#107afe7aa44ab60590fed88841d9f811e91872cb"
   ]
   [
     "batteries.3.11.0"

goblint.opam.template

@@ -2,7 +2,7 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.1.0" "git+https://github.com/goblint/cil.git#76083d655d56e4c7791d457db57f0dd6461faf71" ]
+  [ "goblint-cil.2.1.0" "git+https://github.com/goblint/cil.git#107afe7aa44ab60590fed88841d9f811e91872cb" ]
   # pinned for performance (https://github.com/ocaml-batteries-team/batteries-included/pull/1149) via fork, remove after new batteries release (and then bump the batteries lower-bound accordingly)
   [ "batteries.3.11.0" "git+https://github.com/sim642/batteries-included.git#3920bdf614e4a12120fabfa2c97ee913cc246b13" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release

src/autoTune0.ml

@@ -65,6 +65,7 @@ class collectComplexityFactorsVisitor(factors) = object
     | Switch _
     | Goto _
     | ComputedGoto _
+    | Asm {gotos = _ :: _; _} (* only if has gotos *)
     | Return _ -> factors.controlFlowStatements <- factors.controlFlowStatements + 1; DoChildren
     | Break _
     | Continue _ ->

src/common/framework/cfgTools.ml

@@ -205,6 +205,7 @@ let createCFG (file: file) =
           end
 
         | Instr _
+        | Asm _
         | If _
         | Return _ ->
           stmt, visited_stmts
@@ -280,11 +281,16 @@ let createCFG (file: file) =
               | _ -> failwith "MyCFG.createCFG: >1 Instr [] succ"
             end
 
+          | Asm {template; outputs; inputs; loc; _} ->
+            let edge = (loc, ASM (template, outputs, inputs)) in
+            List.iter (fun (succ, skippedStatements) ->
+                addEdge ~skippedStatements (Statement stmt) edge (Statement succ)
+              ) (real_succs ())
+
           | Instr instrs -> (* non-empty Instr *)
             let edge_of_instr = function
               | Set (lval,exp,loc,eloc) -> Cilfacade.eloc_fallback ~eloc ~loc, Assign (lval, exp)
               | Call (lval,func,args,loc,eloc) -> Cilfacade.eloc_fallback ~eloc ~loc, Proc (lval,func,args)
-              | Asm (attr,tmpl,out,inp,regs,loc) -> loc, ASM (tmpl,out,inp)
               | VarDecl (v, loc) -> loc, VDecl(v)
             in
             let edges = List.map edge_of_instr instrs in

src/common/util/cilLocation.ml

@@ -20,7 +20,6 @@ let get_labelLoc = function
 let get_instrLoc = function
   | Set (_, _, loc, eloc) -> {loc; eloc}
   | Call (_, _, _, loc, eloc) -> {loc; eloc}
-  | Asm (_, _, _, _, _, loc) -> {loc; eloc = locUnknown}
   | VarDecl (_, loc) -> {loc; eloc = locUnknown}
 
 (** Get locations for {!Cil.stmt}. *)
@@ -43,3 +42,4 @@ let rec get_stmtLoc stmt: locs =
   | Switch (_, _, _, loc, eloc) -> {loc; eloc}
   | Loop (_, loc, eloc, _, _) -> {loc; eloc}
   | Block {bstmts = hd :: _; _} -> get_stmtLoc hd
+  | Asm {loc; _} -> {loc; eloc = locUnknown}

src/common/util/cilfacade.ml

@@ -600,14 +600,14 @@ class countFnVisitor = object
     | If (_,_,_,loc,_)
     | Switch (_,_,_,loc,_)
     | Loop (_,loc,_,_,_)
+    | Asm {loc; _}
       -> Hashtbl.replace locs loc.line (); DoChildren
     | _ ->
       DoChildren
 
   method! vinst = function
     | Set (_,_,loc,_)
     | Call (_,_,_,loc,_)
-    | Asm (_,_,_,_,_,loc)
       -> Hashtbl.replace locs loc.line (); SkipChildren
     | _ -> SkipChildren
 

src/common/util/cilfacade0.ml

@@ -29,7 +29,6 @@ let eloc_fallback ~eloc ~loc =
 let get_instrLoc = function
   | Set (_, _, loc, eloc) -> eloc_fallback ~eloc ~loc
   | Call (_, _, _, loc, eloc) -> eloc_fallback ~eloc ~loc
-  | Asm (_, _, _, _, _, loc) -> loc
   | VarDecl (_, loc) -> loc
 
 (** Get expression location for [Cil.stmt]. *)
@@ -51,3 +50,4 @@ let rec get_stmtLoc stmt =
   | Switch (_, _, _, loc, eloc) -> eloc_fallback ~eloc ~loc
   | Loop (_, loc, eloc, _, _) -> eloc_fallback ~eloc ~loc
   | Block {bstmts = hd :: _; _} -> get_stmtLoc hd
+  | Asm {loc; _} -> loc

src/incremental/compareAST.ml

@@ -310,11 +310,6 @@ let eq_instr (a: instr) (b: instr) ~(rename_mapping: rename_mapping) = match a,
     eq_lval lv1 lv2 ~rename_mapping &&>> eq_exp f1 f2 &&>> forward_list_equal eq_exp args1 args2
   | Call (None, f1, args1, _l1, _el1), Call (None, f2, args2, _l2, _el2) ->
     eq_exp f1 f2 ~rename_mapping &&>> forward_list_equal eq_exp args1 args2
-  | Asm (attr1, tmp1, ci1, dj1, rk1, l1), Asm (attr2, tmp2, ci2, dj2, rk2, l2) ->
-    (GobList.equal String.equal tmp1 tmp2, rename_mapping) &&>>
-    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_lval z1 z2) ci1 ci2 &&>>
-    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_exp z1 z2) dj1 dj2 &&>
-    GobList.equal String.equal rk1 rk2(* ignore attributes and locations *)
   | VarDecl (v1, _l1), VarDecl (v2, _l2) -> eq_varinfo v1 v2 ~rename_mapping
   | _, _ -> false, rename_mapping
 
@@ -352,6 +347,12 @@ let rec eq_stmtkind ?(cfg_comp = false) ((a, af): stmtkind * fundec) ((b, bf): s
   | Switch (exp1, block1, stmts1, _l1, _el1), Switch (exp2, block2, stmts2, _l2, _el2) -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else eq_exp exp1 exp2 ~rename_mapping &&>> eq_block' block1 block2 &&>> forward_list_equal (fun a b -> eq_stmt (a,af) (b,bf)) stmts1 stmts2
   | Loop (block1, _l1, _el1, _con1, _br1), Loop (block2, _l2, _el2, _con2, _br2) -> eq_block' block1 block2 ~rename_mapping
   | Block block1, Block block2 -> eq_block' block1 block2 ~rename_mapping
+  | Asm {template = tmp1; outputs = ci1; inputs = dj1; clobbers = rk1; gotos = gotos1; _}, Asm {template = tmp2; outputs = ci2; inputs = dj2; clobbers = rk2; gotos = gotos2; _} ->
+    (GobList.equal String.equal tmp1 tmp2, rename_mapping) &&>>
+    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_lval z1 z2) ci1 ci2 &&>>
+    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_exp z1 z2) dj1 dj2 &&>>
+    forward_list_equal (fun g1 g2 ~rename_mapping:x-> eq_stmt_with_location (!g1, af) (!g2, bf), x) gotos1 gotos2 &&>
+    GobList.equal String.equal rk1 rk2(* ignore attributes and locations *)
   | _, _ -> false, rename_mapping
 
 and eq_stmt ?cfg_comp ((a, af): stmt * fundec) ((b, bf): stmt * fundec) ~(rename_mapping: rename_mapping) =

src/transform/deadCode.ml

@@ -72,7 +72,7 @@ let filter_map_block ?(unchecked_condition = Fun.const (GoblintCil.integer 1)) f
         let keep_block = impl_block b in
         if keep_stmt || keep_block then Some skind else None
 
-      | Instr _ | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ as skind ->
+      | Instr _ | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ | Asm _ as skind ->
         (* no further statements are contained recursively here, so nothing left to do *)
         if keep_stmt then Some skind else None
 
@@ -91,7 +91,8 @@ let filter_map_block ?(unchecked_condition = Fun.const (GoblintCil.integer 1)) f
 (** Is it possible for this statement to begin executing normally, but not finish? *)
 let may_stop_execution stmt =
   match stmt.skind with
-  | Instr is -> List.exists (function Call _ | Asm _ -> true | _ -> false) is
+  | Instr is -> List.exists (function Call _ -> true | _ -> false) is
+  | Asm _ -> true
   | _ -> false
 
 (** Perform a depth first search over the CFG. Record the IDs of live statements;

src/util/loopUnrolling.ml

@@ -380,11 +380,25 @@ class patchLabelsGotosVisitor(newtarget) = object
   inherit nopCilVisitor
 
   method! vstmt s =
+    (* TODO: why sometimes SkipChildren? *)
     match s.skind with
     | Goto (target,loc) ->
       (match newtarget !target with
        | None -> SkipChildren
        | Some nt -> s.skind <- Goto (ref nt, loc); DoChildren)
+    | Asm a ->
+      let (changed, gotos') = List.fold_left_map (fun acc target ->
+          match newtarget !target with
+          | None -> (acc, target) (* TODO: need to copy target ref as well? *)
+          | Some nt -> (true, ref nt)
+        ) false a.gotos
+      in
+      if changed then (
+        s.skind <- Asm {a with gotos = gotos'};
+        DoChildren
+      )
+      else
+        SkipChildren
     | _ -> DoChildren
 end
 

src/util/terminationPreprocessing.ml

@@ -44,6 +44,20 @@ class loopCounterVisitor lc (fd : fundec) = object(self)
       let one = Const (CInt (Cilint.one_cilint, counter_ikind, None)) in
       constFold false (BinOp(bop, e, one, et)) in
 
+    let action_goto l sref =
+      let goto_jmp_stmt = sref.contents in
+      let loc_stmt = Cilfacade.get_stmtLoc goto_jmp_stmt in
+      if CilType.Location.compare l loc_stmt >= 0 then (
+        (* is pos if first loc is greater -> below the second loc *)
+        (* problem: the program might not terminate! *)
+        let open Cilfacade in
+        let current = FunLocH.find_opt funs_with_upjumping_gotos fd in
+        let current = BatOption.default (LocSet.create 13) current in
+        LocSet.replace current l ();
+        FunLocH.replace funs_with_upjumping_gotos fd current;
+      )
+    in
+
     let action s = match s.skind with
       | Loop (b, loc, eloc, _, _) ->
         let vname = "term" ^ string_of_int loc.line ^ "_" ^ string_of_int loc.column ^ "_id" ^ (string_of_int !vcounter) in
@@ -59,17 +73,10 @@ class loopCounterVisitor lc (fd : fundec) = object(self)
         s.skind <- Block nb;
         s
       | Goto (sref, l) ->
-        let goto_jmp_stmt = sref.contents in
-        let loc_stmt = Cilfacade.get_stmtLoc goto_jmp_stmt in
-        if CilType.Location.compare l loc_stmt >= 0 then (
-          (* is pos if first loc is greater -> below the second loc *)
-          (* problem: the program might not terminate! *)
-          let open Cilfacade in
-          let current = FunLocH.find_opt funs_with_upjumping_gotos fd in
-          let current = BatOption.default (LocSet.create 13) current in
-          LocSet.replace current l ();
-          FunLocH.replace funs_with_upjumping_gotos fd current;
-        );
+        action_goto l sref;
+        s
+      | Asm {gotos; loc; _} ->
+        List.iter (action_goto loc) gotos;
         s
       | _ -> s
     in ChangeDoChildrenPost (s, action);

tests/regression/55-loop-unrolling/15-unrolled-loop-asm-goto.c

@@ -0,0 +1,22 @@
+// CRAM
+
+int main()
+{
+  int x;
+  while (1) {
+    asm goto (
+      "nop"
+      :
+      :
+      :
+      : label1, label2
+    );
+    x = 0;
+    continue;
+  label1:
+    x = 1;
+  }
+  return 0;
+label2:
+  return 1;
+}