diff --git a/goblint.opam b/goblint.opam index b89de32bc8..edc8db7f8e 100644 --- a/goblint.opam +++ b/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 diff --git a/goblint.opam.locked b/goblint.opam.locked index ad97ddd842..926567922d 100644 --- a/goblint.opam.locked +++ b/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" diff --git a/goblint.opam.template b/goblint.opam.template index e75f5c7767..72c0f80e7f 100644 --- a/goblint.opam.template +++ b/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 diff --git a/src/autoTune0.ml b/src/autoTune0.ml index b8336a9de7..18969389e8 100644 --- a/src/autoTune0.ml +++ b/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 _ -> diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml index d2d1a92f8c..481029f254 100644 --- a/src/common/framework/cfgTools.ml +++ b/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 diff --git a/src/common/util/cilLocation.ml b/src/common/util/cilLocation.ml index 5b8771d8d4..34ee3114e8 100644 --- a/src/common/util/cilLocation.ml +++ b/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} diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 595f56c381..6a96bd6c81 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -600,6 +600,7 @@ class countFnVisitor = object | If (_,_,_,loc,_) | Switch (_,_,_,loc,_) | Loop (_,loc,_,_,_) + | Asm {loc; _} -> Hashtbl.replace locs loc.line (); DoChildren | _ -> DoChildren @@ -607,7 +608,6 @@ class countFnVisitor = object method! vinst = function | Set (_,_,loc,_) | Call (_,_,_,loc,_) - | Asm (_,_,_,_,_,loc) -> Hashtbl.replace locs loc.line (); SkipChildren | _ -> SkipChildren diff --git a/src/common/util/cilfacade0.ml b/src/common/util/cilfacade0.ml index 5748d9166c..acd089904e 100644 --- a/src/common/util/cilfacade0.ml +++ b/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 diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml index 4d01d7e166..dadaf06029 100644 --- a/src/incremental/compareAST.ml +++ b/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) = diff --git a/src/transform/deadCode.ml b/src/transform/deadCode.ml index 1f6b74695a..490d41cc5c 100644 --- a/src/transform/deadCode.ml +++ b/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; diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 4dee3a62c8..5a797d261f 100644 --- a/src/util/loopUnrolling.ml +++ b/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 diff --git a/src/util/terminationPreprocessing.ml b/src/util/terminationPreprocessing.ml index 95fae95d26..5adac4dc0d 100644 --- a/src/util/terminationPreprocessing.ml +++ b/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); diff --git a/tests/regression/55-loop-unrolling/15-unrolled-loop-asm-goto.c b/tests/regression/55-loop-unrolling/15-unrolled-loop-asm-goto.c new file mode 100644 index 0000000000..5a74466384 --- /dev/null +++ b/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; +} diff --git a/tests/regression/55-loop-unrolling/15-unrolled-loop-asm-goto.t b/tests/regression/55-loop-unrolling/15-unrolled-loop-asm-goto.t new file mode 100644 index 0000000000..089ccaee37 --- /dev/null +++ b/tests/regression/55-loop-unrolling/15-unrolled-loop-asm-goto.t @@ -0,0 +1,120 @@ + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 1 --enable justcil --set dbg.justcil-printer clean 15-unrolled-loop-asm-goto.c + [Info] unrolling loop at 15-unrolled-loop-asm-goto.c:6:3-18:3 with factor 1 + int main(void) + { + int x ; + + { + { + __loop_condition___0: /* CIL Label */ + if (! 1) { + goto loop_end; + } + __asm__ goto ("nop": : : : label1___0, label2); + x = 0; + goto loop_continue_0; + label1___0: + x = 1; + loop_continue_0: /* CIL Label */ ; + { + while (1) { + while_continue: /* CIL Label */ ; + __loop_condition: /* CIL Label */ + if (! 1) { + goto while_break; + } + __asm__ goto ("nop": : : : label1, label2); + x = 0; + goto while_continue; + label1: + x = 1; + } + while_break: /* CIL Label */ ; + } + loop_end: /* CIL Label */ ; + } + return (0); + label2: + return (1); + } + } + + $ cfgDot --unroll 1 15-unrolled-loop-asm-goto.c + [Info] unrolling loop at 15-unrolled-loop-asm-goto.c:6:3-18:3 with factor 1 + + $ graph-easy --as=boxart main.dot + ┌─────────────────────────────────────────────────────┐ + │ main() │ + └─────────────────────────────────────────────────────┘ + │ Neg(1) + │ (body) ┌──────────────────────────────────────────────────────────────────┐ + ▼ ▼ │ + ┌─────────────────────────────────────────────────────┐ ┌──────────────────────────────────────────────────┐ │ + │ 15-unrolled-loop-asm-goto.c:6:3-18:3 (synthetic) │ │ │ │ + │ (15-unrolled-loop-asm-goto.c:6:10-6:11 (synthetic)) │ │ 15-unrolled-loop-asm-goto.c:19:3-19:11 │ │ + │ [15-unrolled-loop-asm-goto.c:6:3-18:3 (synthetic) │ │ (15-unrolled-loop-asm-goto.c:19:10-19:11) │ │ + │ (unknown)] │ │ YAML loc: 15-unrolled-loop-asm-goto.c:19:3-19:11 │ │ + │ YAML loop: 15-unrolled-loop-asm-goto.c:6:3-18:3 │ Neg(1) │ server: true │ │ + ┌········ │ server: false │ ──────────▶ │ │ ───────────┐ │ + : └─────────────────────────────────────────────────────┘ └──────────────────────────────────────────────────┘ │ │ + : │ │ │ + : │ Pos(1) │ │ + : ▼ │ │ + ┌──────────────────────────────────────────────────┐ ┌──────────────────────────────────────────────────┐ : ┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ │ + │ 15-unrolled-loop-asm-goto.c:17:5-17:10 │ │ 15-unrolled-loop-asm-goto.c:17:5-17:10 │ : │ 15-unrolled-loop-asm-goto.c:7:5-13:6 │ │ │ + │ (15-unrolled-loop-asm-goto.c:17:5-17:10) │ │ (15-unrolled-loop-asm-goto.c:17:5-17:10) │ : │ (unknown) │ │ │ + │ YAML loc: 15-unrolled-loop-asm-goto.c:17:5-17:10 │ │ YAML loc: 15-unrolled-loop-asm-goto.c:17:5-17:10 │ ASM ... : │ YAML loc: 15-unrolled-loop-asm-goto.c:7:5-13:6 │ │ │ + ┌───────▶ │ server: true │ ◀·· │ server: true │ ◀────────────────────────────────────────────────────────────────┼──────── │ server: true │ │ │ + │ └──────────────────────────────────────────────────┘ └──────────────────────────────────────────────────┘ : └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ │ │ + │ │ │ : │ : │ │ │ + │ │ │ : │ ASM ... : │ │ │ + │ │ │ : ▼ : │ │ │ + │ │ │ : ┌─────────────────────────────────────────────────────┐ : │ │ │ + │ │ │ : │ 15-unrolled-loop-asm-goto.c:14:5-14:10 │ : │ │ │ + │ │ │ : │ (15-unrolled-loop-asm-goto.c:14:5-14:10) │ : │ │ │ + │ │ │ : │ YAML loc: 15-unrolled-loop-asm-goto.c:14:5-14:10 │ : │ │ │ + │ │ │ ┌···················································┼········ │ server: true │ : └────────────────────────────────────────────────────────┐ │ │ + │ │ │ : : └─────────────────────────────────────────────────────┘ : │ │ │ + │ │ │ : : │ : │ │ │ + │ │ │ : : │ x = 0 └································································┐ │ │ │ + │ │ │ : : ▼ : │ │ │ + │ │ │ : : ┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : │ │ │ + │ │ │ ┌···········┘ └·······▶ │ 15-unrolled-loop-asm-goto.c:6:3-18:3 (synthetic) │ ─┼────┼────┼────┘ + │ │ │ : │ (15-unrolled-loop-asm-goto.c:6:10-6:11 (synthetic)) │ : │ │ + │ │ │ : x = 0 │ [15-unrolled-loop-asm-goto.c:6:3-18:3 (synthetic) │ : │ │ + │ │ │ : ┌───────────────────────────────────────────────────────────▶ │ (unknown)] │ : │ │ + │ │ │ : │ │ YAML loop: 15-unrolled-loop-asm-goto.c:6:3-18:3 │ : │ │ + │ │ │ : │ x = 1 │ server: false │ : │ │ + │ │ └───────────────────────────────────────────────────┼───────────┼───────────────────────────────────────────────────────────▶ │ │ ◀┼────┼────┼────┐ + │ │ : │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : │ │ │ + │ │ : │ │ : │ │ │ + │ │ : │ │ Pos(1) : │ │ │ + │ │ : │ ▼ : │ │ │ + │ │ : ┌──────────────────────────────────────────────────┐ ┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : │ │ │ + │ ASM ... │ : │ 15-unrolled-loop-asm-goto.c:14:5-14:10 │ │ 15-unrolled-loop-asm-goto.c:7:5-13:6 │ : │ │ │ + │ │ : │ (15-unrolled-loop-asm-goto.c:14:5-14:10) │ │ (unknown) │ : │ │ │ + │ │ : │ YAML loc: 15-unrolled-loop-asm-goto.c:14:5-14:10 │ ASM ... │ YAML loc: 15-unrolled-loop-asm-goto.c:7:5-13:6 │ : │ │ │ + │ │ └·······▶ │ server: true │ ◀───────── │ server: true │ ◀┘ │ │ │ + │ │ └──────────────────────────────────────────────────┘ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ + │ │ │ ASM ... │ │ │ │ + │ │ ▼ │ │ │ │ + │ │ ┌─────────────────────────────────────────────────────┐ │ │ │ │ + │ │ │ 15-unrolled-loop-asm-goto.c:21:3-21:11 │ │ │ │ │ x = 1 + │ │ │ (15-unrolled-loop-asm-goto.c:21:10-21:11) │ │ │ │ │ + │ │ │ [15-unrolled-loop-asm-goto.c:20:1-21:3 │ │ │ │ │ + │ │ │ (unknown)] │ │ │ │ │ + │ │ │ YAML loc: 15-unrolled-loop-asm-goto.c:21:3-21:11 │ ASM ... │ │ │ │ + │ │ │ server: true │ ◀─────────────┼────────────────────────────────────────────────────────┘ │ │ + │ │ └─────────────────────────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ + │ │ │ return 1 │ │ │ + │ │ ▼ │ │ │ + │ │ ┌─────────────────────────────────────────────────────┐ return 0 │ │ │ + │ │ │ return of main() │ ◀─────────────┼─────────────────────────────────────────────────────────────┘ │ + │ │ └─────────────────────────────────────────────────────┘ │ │ + │ │ │ │ + │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┼──────────────────────────────────────────────────────────────────┘ + │ │ + │ │ + └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ diff --git a/tests/regression/55-loop-unrolling/dune b/tests/regression/55-loop-unrolling/dune index a2bf9b4515..ed1a2130f8 100644 --- a/tests/regression/55-loop-unrolling/dune +++ b/tests/regression/55-loop-unrolling/dune @@ -2,7 +2,7 @@ (deps (glob_files *.c))) (cram - (applies_to 11-unrolled-loop-invariant) + (applies_to 11-unrolled-loop-invariant 15-unrolled-loop-asm-goto) (enabled_if %{bin-available:graph-easy}) (deps %{bin:cfgDot})) diff --git a/tests/regression/70-transform/05-asm-goto.c b/tests/regression/70-transform/05-asm-goto.c new file mode 100644 index 0000000000..a5e05f21d1 --- /dev/null +++ b/tests/regression/70-transform/05-asm-goto.c @@ -0,0 +1,22 @@ +// SKIP: this is an input file for cram tests +int main() { + asm goto ( + "rdrand %%eax\n" + "and $1, %%eax\n" + "test %%eax, %%eax\n" + "jz %l0\n" + "jmp %l1" + : + : + : "rax", "cc" + : label1, label3 + ); + return 0; +label1: + return 1; // This is reachable +label2: + return 2; // This is certainly dead! +label3: + return 3; // This is reachable +} + \ No newline at end of file diff --git a/tests/regression/70-transform/05-asm-goto.t b/tests/regression/70-transform/05-asm-goto.t new file mode 100644 index 0000000000..f8cd22453f --- /dev/null +++ b/tests/regression/70-transform/05-asm-goto.t @@ -0,0 +1,18 @@ + $ ./transform.sh remove_dead_code -- --enable ana.int.interval --enable sem.noreturn.dead_code 05-asm-goto.c + int main(void) + { + + + { + __asm__ goto ("rdrand %%eax\n" + "and $1, %%eax\n" + "test %%eax, %%eax\n" + "jz %l0\n" + "jmp %l1": : : "rax", "cc": label1, label3); + return (0); + label1: + return (1); + label3: + return (3); + } + } diff --git a/tests/regression/cfg/asm-goto.t/asm-goto.c b/tests/regression/cfg/asm-goto.t/asm-goto.c new file mode 100644 index 0000000000..3c1d328515 --- /dev/null +++ b/tests/regression/cfg/asm-goto.t/asm-goto.c @@ -0,0 +1,21 @@ +int main() { +label0: // This is actually unused + asm goto ( + "rdrand %%eax\n" + "and $1, %%eax\n" + "test %%eax, %%eax\n" + "jz %l0\n" + "jmp %l1" + : + : + : "rax", "cc" + : label1, label3, label0 + ); + return 0; +label1: + return 1; // This is reachable +label2: + return 2; // This is certainly dead! +label3: + return 3; // This is reachable +} diff --git a/tests/regression/cfg/asm-goto.t/run.t b/tests/regression/cfg/asm-goto.t/run.t new file mode 100644 index 0000000000..fab9ab1684 --- /dev/null +++ b/tests/regression/cfg/asm-goto.t/run.t @@ -0,0 +1,50 @@ + $ cfgDot asm-goto.c + + $ graph-easy --as=boxart main.dot + ┌─────────────────────────────────┐ + │ asm-goto.c:18:3-18:11 │ + │ (asm-goto.c:18:10-18:11) │ + │ [asm-goto.c:17:1-18:3 │ + │ (unknown)] │ + │ YAML loc: asm-goto.c:18:3-18:11 │ + │ server: true │ + └─────────────────────────────────┘ + │ + │ return 2 + ▼ + ┌────────────────────────────────────────────────────────────────────┐ return 1 + ┌────────▶ │ return of main() │ ◀──────────────┐ + │ └────────────────────────────────────────────────────────────────────┘ │ + │ ▲ │ + │ │ return 3 │ + │ │ │ + │ ┌─────────────────────────────────┐┌─────────────────────────────────┐ │ + │ │ ││ asm-goto.c:20:3-20:11 │ │ + │ │ ││ (asm-goto.c:20:10-20:11) │ │ + │ │ main() ││ [asm-goto.c:19:1-20:3 │ │ + │ │ ││ (unknown)] │ │ + │ │ ││ YAML loc: asm-goto.c:20:3-20:11 │ │ + │ │ ││ server: true │ │ + │ └─────────────────────────────────┘└─────────────────────────────────┘ │ + │ │ ▲ │ + │ return 0 │ (body) │ ASM ... │ + │ ▼ │ │ + │ ┌────────────────────────────────────────────────────────────────────┐ │ + │ │ asm-goto.c:3:3-13:4 │ │ + │ │ (unknown) │ │ + │ │ [asm-goto.c:2:1-3:3 │ ASM ... │ + │ │ (unknown)] │ ──────────┐ │ + │ │ YAML loc: asm-goto.c:3:3-13:4 │ │ │ + │ │ server: true │ ◀─────────┘ │ + │ └────────────────────────────────────────────────────────────────────┘ │ + │ │ │ │ + │ │ ASM ... │ ASM ... │ + │ ▼ ▼ │ + │ ┌─────────────────────────────────┐┌─────────────────────────────────┐ │ + │ │ ││ asm-goto.c:16:3-16:11 │ │ + │ │ asm-goto.c:14:3-14:11 ││ (asm-goto.c:16:10-16:11) │ │ + │ │ (asm-goto.c:14:10-14:11) ││ [asm-goto.c:15:1-16:3 │ │ + │ │ YAML loc: asm-goto.c:14:3-14:11 ││ (unknown)] │ │ + │ │ server: true ││ YAML loc: asm-goto.c:16:3-16:11 │ │ + └───────── │ ││ server: true │ ───────────────┘ + └─────────────────────────────────┘└─────────────────────────────────┘