From 4a4e814b7b2b7d021eec2759ea419aaa2fc17943 Mon Sep 17 00:00:00 2001 From: Jevgenijs Protopopovs Date: Tue, 15 Apr 2025 13:04:15 +0300 Subject: [PATCH 1/7] Implement goto labels from GCC extended inline assembly syntax. Enables inline assembly to specify a list of C labels where the assembler code might jump, turning inline asm into a control flow branching point. Inline assembly is converted from instruction into a statement; dummy instruction is introduced to replace "empty" instances of inline assembly instruction previously used. --- src/cfg.ml | 6 +- src/check.ml | 19 ++- src/cil.ml | 207 +++++++++++++++++------------ src/cil.mli | 130 +++++++++--------- src/dataflow.ml | 2 +- src/ext/dataslicing/dataslicing.ml | 1 + src/ext/liveness/usedef.ml | 17 ++- src/ext/pta/ptranal.ml | 5 +- src/ext/syntacticsearch/funcVar.ml | 9 ++ src/ext/zrapp/availexps.ml | 2 +- src/ext/zrapp/availexpslv.ml | 2 +- src/ext/zrapp/deadcodeelim.ml | 16 ++- src/ext/zrapp/reachingdefs.ml | 7 +- src/ext/zrapp/rmciltmps.ml | 20 +-- src/frontc/cabs.ml | 3 +- src/frontc/cabs2cil.ml | 33 +++-- src/frontc/cabsvisit.ml | 4 +- src/frontc/cparser.mly | 32 ++++- src/frontc/cprint.ml | 2 +- src/mergecil.ml | 1 + src/rmUnused.ml | 8 ++ test/small1/asm6.c | 23 ++++ 22 files changed, 343 insertions(+), 206 deletions(-) create mode 100644 test/small1/asm6.c diff --git a/src/cfg.ml b/src/cfg.ml index 8ce0c52a6..228ef0a29 100644 --- a/src/cfg.ml +++ b/src/cfg.ml @@ -225,6 +225,9 @@ and cfgStmt (s: stmt) (next:stmt option) (break:stmt option) (cont:stmt option) cfgBlock blk (Some s) next (Some s) nodeList rlabels (* Since all loops have terminating condition true, we don't put any direct successor to stmt following the loop *) + | Asm(_, _, _, _, _, gotos, _) -> + List.iter (fun g -> addSucc !g) gotos; + addOptionSucc next (*------------------------------------------------------------*) @@ -247,7 +250,7 @@ and fasStmt (todo) (s : stmt) = | If (_, tb, fb, _, _) -> (fasBlock todo tb; fasBlock todo fb) | Switch (_, b, _, _, _) -> fasBlock todo b | Loop (b, _, _, _, _) -> fasBlock todo b - | (Return _ | Break _ | Continue _ | Goto _ | ComputedGoto _ | Instr _) -> () + | (Return _ | Break _ | Continue _ | Goto _ | ComputedGoto _ | Instr _ | Asm _) -> () end ;; @@ -270,6 +273,7 @@ let d_cfgnodelabel () (s : stmt) = | Switch _ -> "switch" | Block _ -> "block" | Return _ -> "return" + | Asm _ -> "asm" end in dprintf "%d: %s" s.sid label diff --git a/src/check.ml b/src/check.ml index d8ff57f4f..5e416e5be 100644 --- a/src/check.ml +++ b/src/check.ml @@ -809,7 +809,21 @@ and checkStmt (s: stmt) = in findCase !statements) cases; - + | Asm (_, _, _, _, _, gotos, l) -> + currentLoc := l; + (* Find a label *) + List.iter (fun gref -> + let lab = + match List.filter (function Label _ -> true | _ -> false) + !gref.labels with + Label (lab, _, _) :: _ -> lab + | _ -> + ignore (warn "Assembly goto to block without a label"); + "" + in + (* Remember it as a target *) + gotoTargets := (lab, !gref) :: !gotoTargets + ) gotos | Instr il -> List.iter checkInstr il) () (* argument of withContext *) @@ -821,6 +835,7 @@ and checkInstr (i: instr) = if !ignoreInstr i then () else match i with + DummyInstr _ -> () | Set (dest, e, l, el) -> currentLoc := l; currentExpLoc := el; @@ -885,8 +900,6 @@ and checkInstr (i: instr) = if not v.vhasdeclinstruction then E.s (bug "Encountered a VarDecl, but vhasdeclinstruction for the varinfo is not set") - | Asm _ -> () (* Not yet implemented *) - let rec checkGlobal = function GAsm _ -> () | GPragma _ -> () diff --git a/src/cil.ml b/src/cil.ml index b0fedc8f6..2358dac96 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -823,11 +823,33 @@ and stmtkind = | Block of block (** Just a block of statements. Use it as a way to keep some attributes local *) + | Asm of attributes * (* Really only const and volatile can appear + here *) + string list * (* templates (CR-separated) *) + (string option * string * lval) list * + (* outputs must be lvals with + optional names and constraints. + I would like these + to be actually variables, but I + run into some trouble with ASMs + in the Linux sources *) + (string option * string * exp) list * + (* inputs with optional names and constraints *) + string list * (* register clobbers *) + stmt ref list * (* goto labels *) + location + (** An inline assembly instruction. The arguments are (1) a list of + attributes (only const and volatile can appear here and only for + GCC), (2) templates (CR-separated), (3) a list of + outputs, each of which is an lvalue with a constraint, (4) a list + of input expressions along with constraints, (5) clobbered + registers, and (5) location information *) (** Instructions. They may cause effects directly but may not have control flow.*) and instr = - Set of lval * exp * location * location (** An assignment. A cast is present + DummyInstr of location + | Set of lval * exp * location * location (** An assignment. A cast is present if the exp has different type from lval. Second location is just for expression when inside condition. *) @@ -856,26 +878,6 @@ and instr = are used *) (* sm: I've added a notes.txt file which contains more information on interpreting Asm instructions *) - | Asm of attributes * (* Really only const and volatile can appear - here *) - string list * (* templates (CR-separated) *) - (string option * string * lval) list * - (* outputs must be lvals with - optional names and constraints. - I would like these - to be actually variables, but I - run into some trouble with ASMs - in the Linux sources *) - (string option * string * exp) list * - (* inputs with optional names and constraints *) - string list * (* register clobbers *) - location - (** An inline assembly instruction. The arguments are (1) a list of - attributes (only const and volatile can appear here and only for - GCC), (2) templates (CR-separated), (3) a list of - outputs, each of which is an lvalue with a constraint, (4) a list - of input expressions along with constraints, (5) clobbered - registers, and (5) location information *) @@ -1134,9 +1136,9 @@ let stripUnderscores (s: string) : string = let get_instrLoc (inst : instr) = match inst with - Set(_, _, loc, _) -> loc + DummyInstr(loc) -> loc + | Set(_, _, loc, _) -> loc | Call(_, _, _, loc, _) -> loc - | Asm(_, _, _, _, _, loc) -> loc | VarDecl(_,loc) -> loc let get_globalLoc (g : global) = match g with @@ -1166,6 +1168,7 @@ let rec get_stmtLoc (statement : stmtkind) = | Loop (_, loc, _, _, _) -> loc | Block b -> if b.bstmts == [] then lu else get_stmtLoc ((List.hd b.bstmts).skind) + | Asm(_, _, _, _, _, _, loc) -> loc (* The next variable identifier to use. Counts up *) @@ -1364,7 +1367,7 @@ let mkBlock (slst: stmt list) : block = let mkEmptyStmt () = mkStmt (Instr []) let mkStmtOneInstr (i: instr) = mkStmt (Instr [i]) -let dummyInstr = (Asm([], ["dummy statement!!"], [], [], [], lu)) +let dummyInstr = DummyInstr(lu) let dummyStmt = mkStmt (Instr [dummyInstr]) let compactStmts (b: stmt list) : stmt list = @@ -3586,6 +3589,7 @@ class defaultCilPrinterClass : cilPrinter = object (self) (*** INSTRUCTIONS ****) method pInstr () (i:instr) = (* imperative instruction *) match i with + DummyInstr(l) -> text "" | Set(lv,e,l,el) -> begin (* Be nice to some special cases *) match e with @@ -3749,54 +3753,6 @@ class defaultCilPrinterClass : cilPrinter = object (self) ++ unalign) ++ text (")" ^ printInstrTerminator) - | Asm(attrs, tmpls, outs, ins, clobs, l) -> - self#pLineDirective l - ++ text ("__asm__ ") - ++ self#pAttrs () attrs - ++ text " (" - ++ (align - ++ (docList ~sep:line - (fun x -> text ("\"" ^ escape_string x ^ "\"")) - () tmpls) - ++ - (if outs = [] && ins = [] && clobs = [] then - chr ':' - else - (text ": " - ++ (docList ~sep:(chr ',' ++ break) - (fun (idopt, c, lv) -> - text(match idopt with - None -> "" - | Some id -> "[" ^ id ^ "] " - ) ++ - text ("\"" ^ escape_string c ^ "\" (") - ++ self#pLval () lv - ++ text ")") () outs))) - ++ - (if ins = [] && clobs = [] then - nil - else - (text ": " - ++ (docList ~sep:(chr ',' ++ break) - (fun (idopt, c, e) -> - text(match idopt with - None -> "" - | Some id -> "[" ^ id ^ "] " - ) ++ - text ("\"" ^ escape_string c ^ "\" (") - ++ self#pExp () e - ++ text ")") () ins))) - ++ - (if clobs = [] then nil - else - (text ": " - ++ (docList ~sep:(chr ',' ++ break) - (fun c -> text ("\"" ^ escape_string c ^ "\"")) - () - clobs))) - ++ unalign) - ++ text (")" ^ printInstrTerminator) - (**** STATEMENTS ****) method pStmt () (s:stmt) = (* control-flow statement *) @@ -4018,6 +3974,75 @@ class defaultCilPrinterClass : cilPrinter = object (self) ++ self#pBlock () b) end | Block b -> align ++ self#pBlock () b + | Asm(attrs, tmpls, outs, ins, clobs, gotos, l) -> + let hasGotoAttr = List.length (List.filter (fun attr -> match attr with + Attr("goto", _) -> true + | _ -> false) attrs) > 0 in + self#pLineDirective l + ++ text ("__asm__ ") + ++ self#pAttrs () attrs + ++ text " (" + ++ (align + ++ (docList ~sep:line + (fun x -> text ("\"" ^ escape_string x ^ "\"")) + () tmpls) + ++ + (if outs = [] && ins = [] && clobs = [] && not hasGotoAttr then + chr ':' + else + (text ": " + ++ (docList ~sep:(chr ',' ++ break) + (fun (idopt, c, lv) -> + text(match idopt with + None -> "" + | Some id -> "[" ^ id ^ "] " + ) ++ + text ("\"" ^ escape_string c ^ "\" (") + ++ self#pLval () lv + ++ text ")") () outs))) + ++ + (if ins = [] && clobs = [] && not hasGotoAttr then + nil + else + (text ": " + ++ (docList ~sep:(chr ',' ++ break) + (fun (idopt, c, e) -> + text(match idopt with + None -> "" + | Some id -> "[" ^ id ^ "] " + ) ++ + text ("\"" ^ escape_string c ^ "\" (") + ++ self#pExp () e + ++ text ")") () ins))) + ++ + (if clobs = [] && not hasGotoAttr then nil + else + (text ": " + ++ (docList ~sep:(chr ',' ++ break) + (fun c -> text ("\"" ^ escape_string c ^ "\"")) + () + clobs)) + ++ + (if not hasGotoAttr then nil + else + (text ": " + ++ (docList ~sep:(chr ',' ++ break) + (fun c -> text c) + () + (List.map (fun stmt -> + let rec pickLabel = function + [] -> None + | Label (l, _, _) :: _ -> Some l + | _ :: rest -> pickLabel rest + in + match pickLabel !stmt.labels with + Some lbl -> lbl + | None -> + ignore (error "Cannot find label for target of goto"); + "__invalid_label;" + ) gotos))))) + ++ unalign) + ++ text (")" ^ printInstrTerminator) (*** GLOBALS ***) @@ -4372,6 +4397,7 @@ class defaultCilPrinterClass : cilPrinter = object (self) | "aconst", [] -> text "__const__", true | "thread", [] -> text "__thread", false | "volatile", [] -> text "volatile", false + | "goto", [] -> text "goto", false | "restrict", [] -> text "__restrict", false | "missingproto", [] -> text "/* missing proto */", false | "asm", args -> @@ -5358,6 +5384,7 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr = let fExp e = visitCilExpr vis e in let fLval lv = visitCilLval vis lv in match i with + | DummyInstr(l) -> i | VarDecl(v,l) -> i | Set(lv,e,l,el) -> let lv' = fLval lv in let e' = fExp e in @@ -5371,16 +5398,6 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr = if lv' != lv || fn' != fn || args' != args then Call(Some lv', fn', args', l, el) else i - | Asm(sl,isvol,outs,ins,clobs,l) -> - let outs' = mapNoCopy (fun ((id,s,lv) as pair) -> - let lv' = fLval lv in - if lv' != lv then (id,s,lv') else pair) outs in - let ins' = mapNoCopy (fun ((id,s,e) as pair) -> - let e' = fExp e in - if e' != e then (id,s,e') else pair) ins in - if outs' != outs || ins' != ins then - Asm(sl,isvol,outs',ins',clobs,l) else i - (* visit all nodes in a Cil statement tree in preorder *) and visitCilStmt (vis: cilVisitor) (s: stmt) : stmt = @@ -5443,6 +5460,15 @@ and childrenStmt (toPrepend: instr list ref) : cilVisitor -> stmt -> stmt = | Block b -> let b' = fBlock b in if b' != b then Block b' else s.skind + | Asm(sl,isvol,outs,ins,clobs,gotos,l) -> + let outs' = mapNoCopy (fun ((id,s,lv) as pair) -> + let lv' = visitCilLval vis lv in + if lv' != lv then (id,s,lv') else pair) outs in + let ins' = mapNoCopy (fun ((id,s,e) as pair) -> + let e' = fExp e in + if e' != e then (id,s,e') else pair) ins in + if outs' != outs || ins' != ins then + Asm(sl,isvol,outs',ins',clobs,gotos,l) else s.skind in if skind' != s.skind then s.skind <- skind'; (* Visit the labels *) @@ -5934,7 +5960,7 @@ let rec peepHole1 (* Process one instruction and possibly replace it *) | Switch (e, b, _, _, _) -> peepHole1 doone b.bstmts | Loop (b, l, el, _, _) -> peepHole1 doone b.bstmts | Block b -> peepHole1 doone b.bstmts - | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ -> ()) + | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ | Asm _ -> ()) ss let rec peepHole2 (* Process two instructions and possibly replace them both *) @@ -5962,7 +5988,7 @@ let rec peepHole2 (* Process two instructions and possibly replace them both *) | Loop (b, l, el, _, _) -> peepHole2 dotwo b.bstmts | Block b -> peepHole2 dotwo b.bstmts - | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ -> ()) + | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ | Asm _ -> ()) ss @@ -6056,7 +6082,7 @@ let dExp: doc -> exp = fun d -> Const(CStr(sprint ~width:!lineLength d, No_encoding)) let dInstr: doc -> location -> instr = - fun d l -> Asm([], [sprint ~width:!lineLength d], [], [], [], l) + fun d l -> DummyInstr l let dGlobal: doc -> location -> global = fun d l -> GAsm(sprint ~width:!lineLength d, l) @@ -6429,6 +6455,10 @@ class copyFunctionVisitor (newname: string) = object (self) | Switch (e, body, cases, l, el) -> s.skind <- Switch (e, body, Util.list_map (fun cs -> findStmt cs.sid) cases, l, el) + | Asm(attr, template, outs, ins, clobbers, gotos, loc) -> + (* Make a copy of the reference *) + let gotos' = List.map (fun sr -> ref (findStmt !sr.sid)) gotos in + s.skind <- Asm(attr, template, outs, ins, clobbers, gotos', loc) | _ -> () in List.iter patchstmt !patches; @@ -6470,7 +6500,7 @@ class copyFunctionVisitor (newname: string) = object (self) H.add stmtmap s.sid s'; (* Remember where we copied this *) (* if we have a Goto or a Switch remember them to fixup at end *) (match s'.skind with - (Goto _ | Switch _) -> patches := s' :: !patches + (Goto _ | Switch _ | Asm _) -> patches := s' :: !patches | _ -> ()); (* Do the children *) ChangeDoChildrenPost (s', fun x -> x) @@ -6541,6 +6571,9 @@ and succpred_stmt s fallthrough rlabels = | Return _ -> () | Goto(dest,l) -> link s !dest | ComputedGoto(e,l) -> List.iter (link s) rlabels + | Asm(_, _, _, _, _, gotos, _) -> + List.iter (fun l -> link s !l) gotos; + trylink s fallthrough | Break _ | Continue _ | Switch _ -> @@ -6631,7 +6664,7 @@ let rec xform_switch_stmt s break_dest cont_dest = begin | Default(l,el) -> Label(freshLabel "switch_default",l,false) ) s.labels ; match s.skind with - | Instr _ | Return _ | Goto _ | ComputedGoto _ -> () + | Instr _ | Return _ | Goto _ | ComputedGoto _ | Asm _ -> () | Break(l) -> begin try s.skind <- Goto(break_dest (),l) with e -> diff --git a/src/cil.mli b/src/cil.mli index ae19de994..41ec26fb8 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -1021,6 +1021,70 @@ and stmtkind = (** Just a block of statements. Use it as a way to keep some block attributes local *) + | Asm of attributes * (* Really only const and volatile can appear + here *) + string list * (* templates (CR-separated) *) + (string option * string * lval) list * + (* outputs must be lvals with + optional names and constraints. + I would like these + to be actually variables, but I + run into some trouble with ASMs + in the Linux sources *) + (string option * string * exp) list * + (* inputs with optional names and constraints *) + string list * (* register clobbers *) + stmt ref list * (* gotos *) + location + (** There are for storing inline assembly. They follow the GCC + specification: + {v + asm [volatile] ("...template..." "..template.." + : "c1" (o1), "c2" (o2), ..., "cN" (oN) + : "d1" (i1), "d2" (i2), ..., "dM" (iM) + : "r1", "r2", ..., "nL" ); + v} + + where the parts are + + - [volatile] (optional): when present, the assembler instruction + cannot be removed, moved, or otherwise optimized + - template: a sequence of strings, with %0, %1, %2, etc. in the string to + refer to the input and output expressions. I think they're numbered + consecutively, but the docs don't specify. Each string is printed on + a separate line. + - "ci" (oi): pairs of constraint-string and output-lval; the + constraint specifies that the register used must have some + property, like being a floating-point register; the constraint + string for outputs also has "=" to indicate it is written, or + "+" to indicate it is both read and written; 'oi' is the + name of a C lvalue (probably a variable name) to be used as + the output destination + - "dj" (ij): pairs of constraint and input expression; the constraint + is similar to the "ci"s. the 'ij' is an arbitrary C expression + to be loaded into the corresponding register + - "rk": registers to be regarded as "clobbered" by the instruction; + "memory" may be specified for arbitrary memory effects + + an example (from gcc manual): + {v + asm volatile ("movc3 %0,%1,%2" + : /* no outputs */ + : "g" (from), "g" (to), "g" (count) + : "r0", "r1", "r2", "r3", "r4", "r5"); + v} + + Starting with gcc 3.1, the operands may have names: + + {v + asm volatile ("movc3 %[in0],%1,%2" + : /* no outputs */ + : [in0] "g" (from), "g" (to), "g" (count) + : "r0", "r1", "r2", "r3", "r4", "r5"); + v} + + *) + (** {b Instructions}. An instruction {!instr} is a statement that has no local (intraprocedural) control flow. It can be either an assignment, @@ -1028,7 +1092,8 @@ function call, or an inline assembly instruction. *) (** Instructions. *) and instr = - Set of lval * exp * location * location + DummyInstr of location + | Set of lval * exp * location * location (** An assignment. The type of the expression is guaranteed to be the same with that of the lvalue. Second location is just for expression when inside condition. *) @@ -1050,69 +1115,6 @@ and instr = type T) is encoded SizeOf(T). Second location is just for expression when inside condition. *) - | Asm of attributes * (* Really only const and volatile can appear - here *) - string list * (* templates (CR-separated) *) - (string option * string * lval) list * - (* outputs must be lvals with - optional names and constraints. - I would like these - to be actually variables, but I - run into some trouble with ASMs - in the Linux sources *) - (string option * string * exp) list * - (* inputs with optional names and constraints *) - string list * (* register clobbers *) - location - (** There are for storing inline assembly. They follow the GCC - specification: -{v - asm [volatile] ("...template..." "..template.." - : "c1" (o1), "c2" (o2), ..., "cN" (oN) - : "d1" (i1), "d2" (i2), ..., "dM" (iM) - : "r1", "r2", ..., "nL" ); - v} - -where the parts are - - - [volatile] (optional): when present, the assembler instruction - cannot be removed, moved, or otherwise optimized - - template: a sequence of strings, with %0, %1, %2, etc. in the string to - refer to the input and output expressions. I think they're numbered - consecutively, but the docs don't specify. Each string is printed on - a separate line. - - "ci" (oi): pairs of constraint-string and output-lval; the - constraint specifies that the register used must have some - property, like being a floating-point register; the constraint - string for outputs also has "=" to indicate it is written, or - "+" to indicate it is both read and written; 'oi' is the - name of a C lvalue (probably a variable name) to be used as - the output destination - - "dj" (ij): pairs of constraint and input expression; the constraint - is similar to the "ci"s. the 'ij' is an arbitrary C expression - to be loaded into the corresponding register - - "rk": registers to be regarded as "clobbered" by the instruction; - "memory" may be specified for arbitrary memory effects - -an example (from gcc manual): -{v - asm volatile ("movc3 %0,%1,%2" - : /* no outputs */ - : "g" (from), "g" (to), "g" (count) - : "r0", "r1", "r2", "r3", "r4", "r5"); - v} - - Starting with gcc 3.1, the operands may have names: - -{v - asm volatile ("movc3 %[in0],%1,%2" - : /* no outputs */ - : [in0] "g" (from), "g" (to), "g" (count) - : "r0", "r1", "r2", "r3", "r4", "r5"); - v} - -*) - (** Describes a location in a source file. *) and location = { line: int; (** The line number. -1 means "do not know" *) diff --git a/src/dataflow.ml b/src/dataflow.ml index cd19e3f34..3b92d4f51 100644 --- a/src/dataflow.ml +++ b/src/dataflow.ml @@ -220,7 +220,7 @@ module ForwardsDataFlow = (* Handle instructions starting with the first one *) List.fold_left handleInstruction curr il - | Goto _ | ComputedGoto _ | Break _ | Continue _ | If _ + | Goto _ | ComputedGoto _ | Break _ | Continue _ | If _ | Asm _ | Switch _ | Loop _ | Return _ | Block _ -> curr in currentLoc := get_stmtLoc s.skind; diff --git a/src/ext/dataslicing/dataslicing.ml b/src/ext/dataslicing/dataslicing.ml index 2559e09fa..abb4f6424 100644 --- a/src/ext/dataslicing/dataslicing.ml +++ b/src/ext/dataslicing/dataslicing.ml @@ -361,6 +361,7 @@ let rec sliceStmtKind (sk : stmtkind) : stmtkind = applyOption sliceStmt so1, applyOption sliceStmt so2) | Goto _ -> sk + | Asm _ -> sk | _ -> E.s (unimp "statement") and sliceStmt (s : stmt) : stmt = diff --git a/src/ext/liveness/usedef.ml b/src/ext/liveness/usedef.ml index f002fb19d..7728afd43 100644 --- a/src/ext/liveness/usedef.ml +++ b/src/ext/liveness/usedef.ml @@ -150,12 +150,6 @@ class useDefVisitorClass : cilVisitor = object (self) E.s (bug "bad call to %s" vi.vname) | Call (lvo, f, args, _, _) -> doCall f lvo args - | Asm(_,_,slvl,_,_,_) -> List.iter (fun (_,s,lv) -> - match lv with (Var v, off) -> - if s.[0] = '+' then - varUsed := VS.add v !varUsed; - | _ -> ()) slvl; - DoChildren | _ -> DoChildren end @@ -200,6 +194,11 @@ let computeUseDefStmtKind ?(acc_used=VS.empty) | Instr il -> List.iter (fun i -> ignore (visitCilInstr useDefVisitor i)) il | Block _ -> () + | Asm(_,_,slvl,_,_,_,_) -> List.iter (fun (_,s,lv) -> + match lv with (Var v, off) -> + if s.[0] = '+' then + varUsed := VS.add v !varUsed; + | _ -> ()) slvl; in !varUsed, !varDefs @@ -242,6 +241,12 @@ let rec computeDeepUseDefStmtKind ?(acc_used=VS.empty) List.iter (fun i -> ignore (visitCilInstr useDefVisitor i)) il; !varUsed, !varDefs | Block b -> handle_block b + | Asm(_,_,slvl,_,_,_,_) -> List.iter (fun (_,s,lv) -> + match lv with (Var v, off) -> + if s.[0] = '+' then + varUsed := VS.add v !varUsed; + | _ -> ()) slvl; + !varUsed, !varDefs let computeUseLocalTypes ?(acc_used=VS.empty) (fd : fundec) diff --git a/src/ext/pta/ptranal.ml b/src/ext/pta/ptranal.ml index 8c6c40024..1c20dc167 100644 --- a/src/ext/pta/ptranal.ml +++ b/src/ext/pta/ptranal.ml @@ -269,7 +269,8 @@ let rec analyze_init (i : init ) : A.tau = let analyze_instr (i : instr ) : unit = match i with - Set (lval, rhs, l, el) -> + DummyInstr _ -> () + | Set (lval, rhs, l, el) -> A.assign (analyze_lval lval) (analyze_expr rhs) | Call (res, fexpr, actuals, l, el) -> if not (isFunctionType (typeOf fexpr)) then @@ -298,7 +299,6 @@ let analyze_instr (i : instr ) : unit = Some r -> A.assign_ret site (analyze_lval r) fnres | None -> () end - | Asm _ -> () | VarDecl _ -> () let rec analyze_stmt (s : stmt ) : unit = @@ -328,6 +328,7 @@ let rec analyze_stmt (s : stmt ) : unit = | Block b -> analyze_block b | Break l -> () | Continue l -> () + | Asm _ -> () and analyze_block (b : block ) : unit = diff --git a/src/ext/syntacticsearch/funcVar.ml b/src/ext/syntacticsearch/funcVar.ml index cdee5d74b..ce3997258 100644 --- a/src/ext/syntacticsearch/funcVar.ml +++ b/src/ext/syntacticsearch/funcVar.ml @@ -195,6 +195,15 @@ let rec search_stmt_list_for_var list name varid includeCallTmp = @ search_stmt_list_for_var [ s2 ] name varid includeCallTmp | Block block -> search_stmt_list_for_var block.bstmts name varid includeCallTmp + | Asm(_, _, outs, ins, _, gotos, loc) -> + List.flatten ( + List.concat([ + (List.map (fun asmout -> match asmout with + (_, _, lval) -> search_expression (Lval lval) name loc varid includeCallTmp) outs); + (List.map (fun asmin -> match asmin with + (_, _, exp) -> search_expression exp name loc varid includeCallTmp) ins) + ]) + ) | _ -> [] ) @ search_stmt_list_for_var xs name varid includeCallTmp | [] -> [] diff --git a/src/ext/zrapp/availexps.ml b/src/ext/zrapp/availexps.ml index e9983e2cb..1a2b933fc 100644 --- a/src/ext/zrapp/availexps.ml +++ b/src/ext/zrapp/availexps.ml @@ -243,7 +243,7 @@ let eh_handle_inst i eh = (eh_kill_mem eh; eh_kill_addrof_or_global eh; eh) - | Asm(_,_,_,_,_,_) -> + | DummyInstr(_) -> let _,d = UD.computeUseDefInstr i in (UD.VS.iter (fun vi -> eh_kill_vi eh vi) d; diff --git a/src/ext/zrapp/availexpslv.ml b/src/ext/zrapp/availexpslv.ml index 321b9f656..22335233f 100644 --- a/src/ext/zrapp/availexpslv.ml +++ b/src/ext/zrapp/availexpslv.ml @@ -305,7 +305,7 @@ let lvh_handle_inst i lvh = end; lvh end - | Asm(_,_,_,_,_,_) -> begin + | DummyInstr(_) -> begin let _,d = UD.computeUseDefInstr i in UD.VS.iter (fun vi -> lvh_kill_vi lvh vi) d; diff --git a/src/ext/zrapp/deadcodeelim.ml b/src/ext/zrapp/deadcodeelim.ml index f1135fd8d..c55900bcf 100644 --- a/src/ext/zrapp/deadcodeelim.ml +++ b/src/ext/zrapp/deadcodeelim.ml @@ -80,6 +80,15 @@ class usedDefsCollectorClass = object(self) ignore(super#vstmt s); match s.skind with | Instr _ -> DoChildren + | Asm(_,_,slvl,_,_,_,_) -> begin match self#get_cur_iosh() with + | Some iosh -> List.iter (fun (_,s,lv) -> + match lv with (Var v, off) -> + if s.[0] = '+' then + self#add_defids iosh (Lval(Var v, off)) (UD.VS.singleton v) + | _ -> ()) slvl; + DoChildren + | None -> DoChildren + end | _ -> begin let u,d = UD.computeUseDefStmtKind s.skind in match self#get_cur_iosh() with @@ -102,12 +111,7 @@ class usedDefsCollectorClass = object(self) method! vinst i = let handle_inst iosh i = match i with - | Asm(_,_,slvl,_,_,_) -> List.iter (fun (_,s,lv) -> - match lv with (Var v, off) -> - if s.[0] = '+' then - self#add_defids iosh (Lval(Var v, off)) (UD.VS.singleton v) - | _ -> ()) slvl - | Call(_,ce,el,_,_) when not (!callHasNoSideEffects i) -> + Call(_,ce,el,_,_) when not (!callHasNoSideEffects i) -> List.iter (fun e -> let u = UD.computeUseExp e in UD.VS.iter (fun vi -> diff --git a/src/ext/zrapp/reachingdefs.ml b/src/ext/zrapp/reachingdefs.ml index 8a8a2a028..19250bb8c 100644 --- a/src/ext/zrapp/reachingdefs.ml +++ b/src/ext/zrapp/reachingdefs.ml @@ -270,12 +270,11 @@ let getDefRhs didstmh stmdat defId = Set((Var vi',NoOffset),_,_,_) -> vi'.vid = vid (* _ -> NoOffset *) | Call(Some(Var vi',NoOffset),_,_,_,_) -> vi'.vid = vid (* _ -> NoOffset *) | Call(None,_,_,_,_) -> false - | Asm(_,_,sll,_,_,_) -> List.exists - (function (_,_,(Var vi',NoOffset)) -> vi'.vid = vid | _ -> false) sll | _ -> false) | None -> false) iihl in (match i with - Set((lh,_),e,_,_) -> + DummyInstr _ -> None + | Set((lh,_),e,_,_) -> (match lh with Var(vi') -> (IH.add rhsHtbl defId (Some(RDExp(e),stm.sid,iosh_in)); @@ -284,7 +283,6 @@ let getDefRhs didstmh stmdat defId = | Call(lvo,e,el,_,_) -> (IH.add rhsHtbl defId (Some(RDCall(i),stm.sid,iosh_in)); Some(RDCall(i), stm.sid, iosh_in)) - | Asm(a,sl,slvl,sel,sl',_) -> None | VarDecl _ -> None ) (* ? *) with Not_found -> @@ -292,6 +290,7 @@ let getDefRhs didstmh stmdat defId = IH.add rhsHtbl defId None; None)) with Invalid_argument _ -> None end + | Asm _ -> None | _ -> E.s (E.error "getDefRhs: defining statement not an instruction list %d" defId) (*None*) diff --git a/src/ext/zrapp/rmciltmps.ml b/src/ext/zrapp/rmciltmps.ml index 1c512d7cc..e1568bccb 100644 --- a/src/ext/zrapp/rmciltmps.ml +++ b/src/ext/zrapp/rmciltmps.ml @@ -994,16 +994,6 @@ class unusedRemoverClass : cilVisitor = object(self) (match IH.find iioh vi.vid with None -> true | Some _ -> false) end - | Asm(_,_,slvlst,_,_,_) -> begin - (* make sure the outputs are in the locals list *) - List.iter (fun (_,s,lv) -> - match lv with (Var vi,_) -> - if List.mem vi cur_func.slocals - then () - else cur_func.slocals <- vi::cur_func.slocals - |_ -> ()) slvlst; - true - end | _ -> true in @@ -1024,6 +1014,16 @@ class unusedRemoverClass : cilVisitor = object(self) let newil' = Util.list_map call_fixer newil in stm.skind <- Instr(newil'); SkipChildren + | Asm(_,_,slvlst,_,_,_,_) -> begin + (* make sure the outputs are in the locals list *) + List.iter (fun (_,s,lv) -> + match lv with (Var vi,_) -> + if List.mem vi cur_func.slocals + then () + else cur_func.slocals <- vi::cur_func.slocals + |_ -> ()) slvlst; + DoChildren + end | _ -> DoChildren end diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index 45491dc1a..b90a5cdbc 100644 --- a/src/frontc/cabs.ml +++ b/src/frontc/cabs.ml @@ -210,7 +210,8 @@ and block = and asm_details = { aoutputs: (string option * string * expression) list; (* optional name, constraints and expressions for outputs *) ainputs: (string option * string * expression) list; (* optional name, constraints and expressions for inputs *) - aclobbers: string list (* clobbered registers *) + aclobbers: string list; (* clobbered registers *) + agotos: string list (* goto labels *) } and statement = diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 023a3eb5b..4289b637d 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -842,10 +842,10 @@ module BlockChunk = {l with synthetic = true} let doInstr: instr -> instr = function + DummyInstr(eloc) -> DummyInstr(doLoc eloc) | Set (l, e, loc, eloc) -> Set (l, e, doLoc loc, doLoc eloc) | VarDecl (v, loc) -> VarDecl (v, doLoc loc) | Call (l, f, a, loc, eloc) -> Call (l, f, a, doLoc loc, doLoc eloc) - | Asm (a, b, c, d, e, loc) -> Asm (a, b, c, d, e, doLoc loc) (** Change all stmt and instr locs to synthetic, except the first one. Expressions/initializers that expand to multiple instructions cannot have intermediate locations referenced. *) @@ -883,6 +883,7 @@ module BlockChunk = | Block b -> doBlock ~first b; s.skind + | Asm (a, b, c, d, e, f, loc) -> Asm (a, b, c, d, e, f, doLoc loc) and doBlock ~first b = doStmts ~first b.bstmts and doStmts ~first = function @@ -921,6 +922,7 @@ module BlockChunk = | Block b -> doBlock b; s.skind + | Asm(attrs, templates, outs, ins, clobbers, gotos, loc) -> Asm(attrs, templates, outs, ins, clobbers, gotos, doLoc loc) and doBlock b = doStmts b.bstmts and doStmts = function @@ -936,10 +938,10 @@ module BlockChunk = c let eDoInstr: instr -> instr = function + DummyInstr(eloc) -> DummyInstr(doLoc eloc) | Set (l, e, loc, eloc) -> Set (l, e, loc, doLoc eloc) | VarDecl (v, loc) -> VarDecl (v, loc) | Call (l, f, a, loc, eloc) -> Call (l, f, a, loc, doLoc eloc) - | Asm (a, b, c, d, e, loc) -> Asm (a, b, c, d, e, loc) (** Change first stmt or instr eloc to synthetic. *) let eDoChunkHead (c: chunk): chunk = @@ -964,6 +966,7 @@ module BlockChunk = | Block b -> doBlock b; s.skind + | Asm (a, b, c, d, e, f, loc) -> Asm (a, b, c, d, e, f, doLoc loc) and doBlock b = doStmts b.bstmts and doStmts = function @@ -6490,14 +6493,14 @@ and doDecl (isglobal: bool) (isstmt: bool) : A.definition -> chunk = function unnecessary warning than to break CIL's invariant that return statements are inserted properly. *) let instrFallsThrough (i : instr) = match i with - Set _ -> true + DummyInstr _ -> true + | Set _ -> true | Call (None, Lval (Var e, NoOffset), _, _, _) -> (* See if this is exit, or if it has the noreturn attribute *) if e.vname = "exit" then false else if hasAttribute "noreturn" e.vattr then false else true | Call _ -> true - | Asm _ -> true | VarDecl _ -> true in let rec stmtFallsThrough (s: stmt) : bool = @@ -6529,6 +6532,7 @@ and doDecl (isglobal: bool) (isstmt: bool) : A.definition -> chunk = function (* A loop falls through if it can break. *) blockCanBreak b | Block b -> blockFallsThrough b + | Asm _ -> true and blockFallsThrough b = let rec fall = function [] -> true @@ -6566,7 +6570,7 @@ and doDecl (isglobal: bool) (isstmt: bool) : A.definition -> chunk = function (* will we leave this statement or block with a break command? *) and stmtCanBreak (s: stmt) : bool = match s.skind with - Instr _ | Return _ | Continue _ | Goto _ | ComputedGoto _ -> false + Instr _ | Return _ | Continue _ | Goto _ | ComputedGoto _ | Asm _ -> false | Break _ -> true | If (_, b1, b2, _, _) -> blockCanBreak b1 || blockCanBreak b2 @@ -7049,7 +7053,7 @@ and doStatement (s : A.statement) : chunk = currentLoc := loc'; currentExpLoc := loc'; (* for argument doExp below *) let stmts : chunk ref = ref empty in - let (tmpls', outs', ins', clobs') = + let (tmpls', outs', ins', clobs', gotos') = match details with | None -> let tmpls' = @@ -7057,8 +7061,8 @@ and doStatement (s : A.statement) : chunk = let escape = Str.global_replace pattern "%%" in Util.list_map escape tmpls in - (tmpls', [], [], []) - | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs } -> + (tmpls', [], [], [], []) + | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; agotos = gotos } -> let outs' = Util.list_map (fun (id, c, e) -> @@ -7081,10 +7085,19 @@ and doStatement (s : A.statement) : chunk = (id, c, e')) ins in - (tmpls, outs', ins', clobs) + let gotos' = List.map (fun l -> + let gref = ref dummyStmt in + addGoto (lookupLabel l) gref; + gref + ) gotos + in + (tmpls, outs', ins', clobs, gotos') in !stmts @@ - (i2c (Asm(attr', tmpls', outs', ins', clobs', loc'))) + { stmts = [mkStmt (Asm(attr', tmpls', outs', ins', clobs', gotos', loc'))]; + postins = []; + cases = []; + } with e when continueOnError -> begin (ignore (E.log "Error in doStatement (%s)\n" (Printexc.to_string e))); diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml index 444392e58..53e2574ea 100644 --- a/src/frontc/cabsvisit.ml +++ b/src/frontc/cabsvisit.ml @@ -435,13 +435,13 @@ and childrenStatement vis s = in let details' = match details with | None -> details - | Some { aoutputs = outl; ainputs = inl; aclobbers = clobs } -> + | Some { aoutputs = outl; ainputs = inl; aclobbers = clobs; agotos = gotos } -> let outl' = mapNoCopy childrenIdentStringExp outl in let inl' = mapNoCopy childrenIdentStringExp inl in if outl' == outl && inl' == inl then details else - Some { aoutputs = outl'; ainputs = inl'; aclobbers = clobs } + Some { aoutputs = outl'; ainputs = inl'; aclobbers = clobs; agotos = gotos } in if details' != details then ASM (sl, b, details', l) else s diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 112f423e1..2050a2a8c 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -1651,6 +1651,7 @@ paren_attr_list: /*** GCC ASM instructions ***/ asmattr: /* empty */ { [] } +| GOTO asmattr { ("goto", []) :: $2 } | VOLATILE asmattr { ("volatile", []) :: $2 } | CONST asmattr { ("const", []) :: $2 } | INLINE asmattr { ("inline", []) :: $2 } @@ -1662,8 +1663,8 @@ asmtemplate: asmoutputs: /* empty */ { None } | COLON asmoperands asminputs - { let (ins, clobs) = $3 in - Some {aoutputs = $2; ainputs = ins; aclobbers = clobs} } + { let (ins, clobs, gotos) = $3 in + Some {aoutputs = $2; ainputs = ins; aclobbers = clobs; agotos = gotos;} } ; asmoperands: /* empty */ { [] } @@ -1680,9 +1681,10 @@ asmoperand: ; asminputs: - /* empty */ { ([], []) } + /* empty */ { ([], [], []) } | COLON asmoperands asmclobber - { ($2, $3) } + { let (clobs, gotos) = $3 in + ($2, clobs, gotos) } ; asmopname: /* empty */ { None } @@ -1690,8 +1692,8 @@ asmopname: ; asmclobber: - /* empty */ { [] } -| COLON asmclobberlst { $2 } + /* empty */ { ([], []) } +| COLON asmclobberlst asmgoto { ($2, $3) } ; asmclobberlst: /* empty */ { [] } @@ -1702,4 +1704,22 @@ asmclobberlst_ne: | one_string_constant COMMA asmclobberlst_ne { $1 :: $3 } ; +asmgoto: + /* empty */ { [] } +| COLON asmgotolst { $2 } +; + +asmgotolst: + /* empty */ { [] } +| asmgotolst_ne { $1 } +; + +asmgotolst_ne: + asmgotolabel { [$1] } +| asmgotolabel COMMA asmgotolst_ne { $1 :: $3 } +; + +asmgotolabel: IDENT { fst $1 } +; + %% diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 31a2257e2..3d86faec7 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -720,7 +720,7 @@ and print_statement stat = begin match details with | None -> () - | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs } -> + | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; agotos = gotos } -> print ":"; space (); print_commas false print_asm_operand outs; if ins <> [] || clobs <> [] then begin diff --git a/src/mergecil.ml b/src/mergecil.ml index 8362a36c9..caa7e1ee2 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -1167,6 +1167,7 @@ | Switch (_, b, _, _, _) -> 43 + (47 * stmtListSum b.bstmts) (* don't look at stmt list b/c is not part of tree *) | Loop (b, _, _, _, _) -> 49 + (53 * stmtListSum b.bstmts) | Block b -> 59 + (61 * stmtListSum b.bstmts) + | Asm _ -> 67 in (* disabled 2nd and 3rd measure because they appear to get different diff --git a/src/rmUnused.ml b/src/rmUnused.ml index 834e1b9db..5df4c1062 100644 --- a/src/rmUnused.ml +++ b/src/rmUnused.ml @@ -643,6 +643,14 @@ class markUsedLabels (labelMap: (string, unit) H.t) = object H.replace labelMap ln (); DoChildren + | Asm(_, _, _, _, _, gotos, _) -> List.iter (fun dest -> + let (ln, _, _), _ = labelsToKeep !dest.labels in + if ln = "" then + E.s (E.bug "rmUnused: destination of statement does not have labels"); + (* Mark it as used *) + H.replace labelMap ln ();) gotos; + DoChildren + | _ -> DoChildren method! vexpr e = match e with diff --git a/test/small1/asm6.c b/test/small1/asm6.c new file mode 100644 index 000000000..6550e824d --- /dev/null +++ b/test/small1/asm6.c @@ -0,0 +1,23 @@ +void infinite_loop() +{ +label1: + asm goto ( + "jmp %l0" + : /* No outputs. */ + : /* No inputs */ + : /* No clobbers */ + : label1); +} + +void conditionally_infinite_loop(int x) { +label1: + asm goto ( + "test %0, %0\n" + "jz %l1\n" + "jmp %l2" + : /* No outputs. */ + : "r"(x) + : /* No clobbers */ + : label1, label2); +label2: ; +} From c2c20fe1c5ba06765550984ffdcc3000d9d6b107 Mon Sep 17 00:00:00 2001 From: Jevgenijs Protopopovs Date: Wed, 14 Jan 2026 13:51:04 +0200 Subject: [PATCH 2/7] Update testcil.pl with new inline assembly goto parsing test --- test/testcil.pl | 1 + 1 file changed, 1 insertion(+) diff --git a/test/testcil.pl b/test/testcil.pl index ce9f20818..69e90e41d 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -182,6 +182,7 @@ sub addToGroup { addTest("test/asm4 _GNUCC=1"); addTest("test/asm_emptyclobberallowed _GNUCC=1"); addTest("testobj/asm5 _GNUCC=1"); +addTest("test/asm6"); addTest("testrun/offsetof"); addTest("testrun/offsetof1"); From bfdeb864c1a45f6c248f62c16fcb9f9d8a511ad3 Mon Sep 17 00:00:00 2001 From: Jevgenijs Protopopovs Date: Thu, 15 Jan 2026 15:08:19 +0200 Subject: [PATCH 3/7] Revert to the original definition of dummyStmt --- src/cil.ml | 7 +++---- src/cil.mli | 9 +++------ src/frontc/cabs2cil.ml | 2 +- 3 files changed, 7 insertions(+), 11 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 2358dac96..b8c393a2f 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -1367,8 +1367,7 @@ let mkBlock (slst: stmt list) : block = let mkEmptyStmt () = mkStmt (Instr []) let mkStmtOneInstr (i: instr) = mkStmt (Instr [i]) -let dummyInstr = DummyInstr(lu) -let dummyStmt = mkStmt (Instr [dummyInstr]) +let dummyStmt = mkStmt (Asm([], ["dummy statement!!"], [], [], [], [], lu)) let compactStmts (b: stmt list) : stmt list = (* Try to compress statements. Scan the list of statements and remember @@ -6081,8 +6080,8 @@ let typeSigAttrs = function let dExp: doc -> exp = fun d -> Const(CStr(sprint ~width:!lineLength d, No_encoding)) -let dInstr: doc -> location -> instr = - fun d l -> DummyInstr l +let dStmt: doc -> location -> stmt = + fun d l -> mkStmt (Asm([], [sprint ~width:!lineLength d], [], [], [], [], l)) let dGlobal: doc -> location -> global = fun d l -> GAsm(sprint ~width:!lineLength d, l) diff --git a/src/cil.mli b/src/cil.mli index 41ec26fb8..a00c8b8a7 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -1767,10 +1767,7 @@ val compactStmts: stmt list -> stmt list (** Returns an empty statement (of kind [Instr]) *) val mkEmptyStmt: unit -> stmt -(** A instr to serve as a placeholder *) -val dummyInstr: instr - -(** A statement consisting of just [dummyInstr] *) +(** A statement to serve as a placeholder *) val dummyStmt: stmt (** Make a while loop. Can contain Break or Continue *) @@ -2669,8 +2666,8 @@ val get_stmtLoc: stmtkind -> location (** Generate an {!exp} to be used in case of errors. *) val dExp: Pretty.doc -> exp -(** Generate an {!instr} to be used in case of errors. *) -val dInstr: Pretty.doc -> location -> instr +(** Generate an {!stmt} to be used in case of errors. *) +val dStmt: Pretty.doc -> location -> stmt (** Generate a {!global} to be used in case of errors. *) val dGlobal: Pretty.doc -> location -> global diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 4289b637d..d0c444285 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -5071,7 +5071,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) with e when continueOnError -> begin (*ignore (E.log "error in doExp (%s)" (Printexc.to_string e));*) E.hadErrors := true; - (i2c (dInstr (dprintf "booo_exp(%t)" d_thisloc) !currentLoc), + (s2c (dStmt (dprintf "booo_exp(%t)" d_thisloc) !currentLoc), integer 0, intType) end From a47bd172336709a794a2797450a1a91f62db1b85 Mon Sep 17 00:00:00 2001 From: Jevgenijs Protopopovs Date: Thu, 15 Jan 2026 15:13:17 +0200 Subject: [PATCH 4/7] Remove DummyInstr instructiontype --- src/check.ml | 3 +-- src/cil.ml | 10 +++------- src/cil.mli | 3 +-- src/ext/pta/ptranal.ml | 3 +-- src/ext/syntacticsearch/funcVar.ml | 2 -- src/ext/zrapp/availexps.ml | 5 ----- src/ext/zrapp/availexpslv.ml | 6 ------ src/ext/zrapp/reachingdefs.ml | 3 +-- src/frontc/cabs2cil.ml | 9 +++------ 9 files changed, 10 insertions(+), 34 deletions(-) diff --git a/src/check.ml b/src/check.ml index 5e416e5be..31c7735f7 100644 --- a/src/check.ml +++ b/src/check.ml @@ -835,8 +835,7 @@ and checkInstr (i: instr) = if !ignoreInstr i then () else match i with - DummyInstr _ -> () - | Set (dest, e, l, el) -> + Set (dest, e, l, el) -> currentLoc := l; currentExpLoc := el; let t = checkLval false false dest in diff --git a/src/cil.ml b/src/cil.ml index b8c393a2f..5124072bf 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -848,8 +848,7 @@ and stmtkind = (** Instructions. They may cause effects directly but may not have control flow.*) and instr = - DummyInstr of location - | Set of lval * exp * location * location (** An assignment. A cast is present + Set of lval * exp * location * location (** An assignment. A cast is present if the exp has different type from lval. Second location is just for expression when inside condition. *) @@ -1136,8 +1135,7 @@ let stripUnderscores (s: string) : string = let get_instrLoc (inst : instr) = match inst with - DummyInstr(loc) -> loc - | Set(_, _, loc, _) -> loc + Set(_, _, loc, _) -> loc | Call(_, _, _, loc, _) -> loc | VarDecl(_,loc) -> loc let get_globalLoc (g : global) = @@ -3588,8 +3586,7 @@ class defaultCilPrinterClass : cilPrinter = object (self) (*** INSTRUCTIONS ****) method pInstr () (i:instr) = (* imperative instruction *) match i with - DummyInstr(l) -> text "" - | Set(lv,e,l,el) -> begin + Set(lv,e,l,el) -> begin (* Be nice to some special cases *) match e with BinOp((PlusA|PlusPI|IndexPI),Lval(lv'),Const(CInt(one,_,_)),_) @@ -5383,7 +5380,6 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr = let fExp e = visitCilExpr vis e in let fLval lv = visitCilLval vis lv in match i with - | DummyInstr(l) -> i | VarDecl(v,l) -> i | Set(lv,e,l,el) -> let lv' = fLval lv in let e' = fExp e in diff --git a/src/cil.mli b/src/cil.mli index a00c8b8a7..583cb0a0e 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -1092,8 +1092,7 @@ function call, or an inline assembly instruction. *) (** Instructions. *) and instr = - DummyInstr of location - | Set of lval * exp * location * location + Set of lval * exp * location * location (** An assignment. The type of the expression is guaranteed to be the same with that of the lvalue. Second location is just for expression when inside condition. *) diff --git a/src/ext/pta/ptranal.ml b/src/ext/pta/ptranal.ml index 1c20dc167..661a34c23 100644 --- a/src/ext/pta/ptranal.ml +++ b/src/ext/pta/ptranal.ml @@ -269,8 +269,7 @@ let rec analyze_init (i : init ) : A.tau = let analyze_instr (i : instr ) : unit = match i with - DummyInstr _ -> () - | Set (lval, rhs, l, el) -> + Set (lval, rhs, l, el) -> A.assign (analyze_lval lval) (analyze_expr rhs) | Call (res, fexpr, actuals, l, el) -> if not (isFunctionType (typeOf fexpr)) then diff --git a/src/ext/syntacticsearch/funcVar.ml b/src/ext/syntacticsearch/funcVar.ml index ce3997258..491cbad5f 100644 --- a/src/ext/syntacticsearch/funcVar.ml +++ b/src/ext/syntacticsearch/funcVar.ml @@ -159,8 +159,6 @@ let rec search_instr_list_for_var list name varid includeCallTmp = search_expression exp name loc varid includeCallTmp @ search_expression_list exp_list name loc varid includeCallTmp @ search_instr_list_for_var xs name varid includeCallTmp - (* Should I consider Asm too? *) - | _ :: xs -> search_instr_list_for_var xs name varid includeCallTmp | [] -> [] (* Finds a variable in a list of statements *) diff --git a/src/ext/zrapp/availexps.ml b/src/ext/zrapp/availexps.ml index 1a2b933fc..48dc8a740 100644 --- a/src/ext/zrapp/availexps.ml +++ b/src/ext/zrapp/availexps.ml @@ -243,11 +243,6 @@ let eh_handle_inst i eh = (eh_kill_mem eh; eh_kill_addrof_or_global eh; eh) - | DummyInstr(_) -> - let _,d = UD.computeUseDefInstr i in - (UD.VS.iter (fun vi -> - eh_kill_vi eh vi) d; - eh) | VarDecl _ -> raise (Unimplemented "VarDecl") (* VarDecl instruction is not supported for availexps, to make availexps work for programs without VLA *) (* make sure to set alwaysGenerateVarDecl in cabs2cil.ml to false. To support VLA, implement this. *) diff --git a/src/ext/zrapp/availexpslv.ml b/src/ext/zrapp/availexpslv.ml index 22335233f..8b42eb1c1 100644 --- a/src/ext/zrapp/availexpslv.ml +++ b/src/ext/zrapp/availexpslv.ml @@ -305,12 +305,6 @@ let lvh_handle_inst i lvh = end; lvh end - | DummyInstr(_) -> begin - let _,d = UD.computeUseDefInstr i in - UD.VS.iter (fun vi -> - lvh_kill_vi lvh vi) d; - lvh - end | VarDecl _ -> raise (Unimplemented "VarDecl") (* VarDecl instruction is not supported for availexpslv, to make availexpslv work for programs without VLA *) (* make sure to set alwaysGenerateVarDecl in cabs2cil.ml to false. To support VLA, implement this. *) diff --git a/src/ext/zrapp/reachingdefs.ml b/src/ext/zrapp/reachingdefs.ml index 19250bb8c..cc2d9d532 100644 --- a/src/ext/zrapp/reachingdefs.ml +++ b/src/ext/zrapp/reachingdefs.ml @@ -273,8 +273,7 @@ let getDefRhs didstmh stmdat defId = | _ -> false) | None -> false) iihl in (match i with - DummyInstr _ -> None - | Set((lh,_),e,_,_) -> + Set((lh,_),e,_,_) -> (match lh with Var(vi') -> (IH.add rhsHtbl defId (Some(RDExp(e),stm.sid,iosh_in)); diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index d0c444285..84be49340 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -842,8 +842,7 @@ module BlockChunk = {l with synthetic = true} let doInstr: instr -> instr = function - DummyInstr(eloc) -> DummyInstr(doLoc eloc) - | Set (l, e, loc, eloc) -> Set (l, e, doLoc loc, doLoc eloc) + Set (l, e, loc, eloc) -> Set (l, e, doLoc loc, doLoc eloc) | VarDecl (v, loc) -> VarDecl (v, doLoc loc) | Call (l, f, a, loc, eloc) -> Call (l, f, a, doLoc loc, doLoc eloc) @@ -938,8 +937,7 @@ module BlockChunk = c let eDoInstr: instr -> instr = function - DummyInstr(eloc) -> DummyInstr(doLoc eloc) - | Set (l, e, loc, eloc) -> Set (l, e, loc, doLoc eloc) + Set (l, e, loc, eloc) -> Set (l, e, loc, doLoc eloc) | VarDecl (v, loc) -> VarDecl (v, loc) | Call (l, f, a, loc, eloc) -> Call (l, f, a, loc, doLoc eloc) @@ -6493,8 +6491,7 @@ and doDecl (isglobal: bool) (isstmt: bool) : A.definition -> chunk = function unnecessary warning than to break CIL's invariant that return statements are inserted properly. *) let instrFallsThrough (i : instr) = match i with - DummyInstr _ -> true - | Set _ -> true + Set _ -> true | Call (None, Lval (Var e, NoOffset), _, _, _) -> (* See if this is exit, or if it has the noreturn attribute *) if e.vname = "exit" then false From b70dae0aae0a2ac8d899ac1cf19ddca2114497a5 Mon Sep 17 00:00:00 2001 From: Jevgenijs Protopopovs Date: Fri, 16 Jan 2026 10:45:49 +0200 Subject: [PATCH 5/7] Rollback spurious changes to reduce diff clutter --- src/check.ml | 2 +- src/cil.ml | 4 ++-- src/cil.mli | 2 +- src/ext/pta/ptranal.ml | 2 +- src/ext/zrapp/reachingdefs.ml | 4 ++-- src/frontc/cabs2cil.ml | 4 ++-- 6 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/check.ml b/src/check.ml index 31c7735f7..6e0d919b4 100644 --- a/src/check.ml +++ b/src/check.ml @@ -835,7 +835,7 @@ and checkInstr (i: instr) = if !ignoreInstr i then () else match i with - Set (dest, e, l, el) -> + | Set (dest, e, l, el) -> currentLoc := l; currentExpLoc := el; let t = checkLval false false dest in diff --git a/src/cil.ml b/src/cil.ml index 5124072bf..24dee2e31 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -848,7 +848,7 @@ and stmtkind = (** Instructions. They may cause effects directly but may not have control flow.*) and instr = - Set of lval * exp * location * location (** An assignment. A cast is present + Set of lval * exp * location * location (** An assignment. A cast is present if the exp has different type from lval. Second location is just for expression when inside condition. *) @@ -3586,7 +3586,7 @@ class defaultCilPrinterClass : cilPrinter = object (self) (*** INSTRUCTIONS ****) method pInstr () (i:instr) = (* imperative instruction *) match i with - Set(lv,e,l,el) -> begin + | Set(lv,e,l,el) -> begin (* Be nice to some special cases *) match e with BinOp((PlusA|PlusPI|IndexPI),Lval(lv'),Const(CInt(one,_,_)),_) diff --git a/src/cil.mli b/src/cil.mli index 583cb0a0e..1b9d27fa9 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -1092,7 +1092,7 @@ function call, or an inline assembly instruction. *) (** Instructions. *) and instr = - Set of lval * exp * location * location + Set of lval * exp * location * location (** An assignment. The type of the expression is guaranteed to be the same with that of the lvalue. Second location is just for expression when inside condition. *) diff --git a/src/ext/pta/ptranal.ml b/src/ext/pta/ptranal.ml index 661a34c23..e1b00b1c3 100644 --- a/src/ext/pta/ptranal.ml +++ b/src/ext/pta/ptranal.ml @@ -269,7 +269,7 @@ let rec analyze_init (i : init ) : A.tau = let analyze_instr (i : instr ) : unit = match i with - Set (lval, rhs, l, el) -> + Set (lval, rhs, l, el) -> A.assign (analyze_lval lval) (analyze_expr rhs) | Call (res, fexpr, actuals, l, el) -> if not (isFunctionType (typeOf fexpr)) then diff --git a/src/ext/zrapp/reachingdefs.ml b/src/ext/zrapp/reachingdefs.ml index cc2d9d532..2852e34fd 100644 --- a/src/ext/zrapp/reachingdefs.ml +++ b/src/ext/zrapp/reachingdefs.ml @@ -267,13 +267,13 @@ let getDefRhs didstmh stmdat defId = match time "iosh_defId_find" (iosh_defId_find iosh') defId with Some vid -> (match i with - Set((Var vi',NoOffset),_,_,_) -> vi'.vid = vid (* _ -> NoOffset *) + Set((Var vi',NoOffset),_,_,_) -> vi'.vid = vid (* _ -> NoOffset *) | Call(Some(Var vi',NoOffset),_,_,_,_) -> vi'.vid = vid (* _ -> NoOffset *) | Call(None,_,_,_,_) -> false | _ -> false) | None -> false) iihl in (match i with - Set((lh,_),e,_,_) -> + Set((lh,_),e,_,_) -> (match lh with Var(vi') -> (IH.add rhsHtbl defId (Some(RDExp(e),stm.sid,iosh_in)); diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 84be49340..1b3586dc0 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -842,7 +842,7 @@ module BlockChunk = {l with synthetic = true} let doInstr: instr -> instr = function - Set (l, e, loc, eloc) -> Set (l, e, doLoc loc, doLoc eloc) + | Set (l, e, loc, eloc) -> Set (l, e, doLoc loc, doLoc eloc) | VarDecl (v, loc) -> VarDecl (v, doLoc loc) | Call (l, f, a, loc, eloc) -> Call (l, f, a, doLoc loc, doLoc eloc) @@ -937,7 +937,7 @@ module BlockChunk = c let eDoInstr: instr -> instr = function - Set (l, e, loc, eloc) -> Set (l, e, loc, doLoc eloc) + | Set (l, e, loc, eloc) -> Set (l, e, loc, doLoc eloc) | VarDecl (v, loc) -> VarDecl (v, loc) | Call (l, f, a, loc, eloc) -> Call (l, f, a, loc, doLoc eloc) From 00120f7e6981ad30276c882dd711a40c811f74c8 Mon Sep 17 00:00:00 2001 From: Jevgenijs Protopopovs Date: Fri, 16 Jan 2026 11:08:54 +0200 Subject: [PATCH 6/7] Integrate some of the changes from #161 --- src/ext/liveness/usedef.ml | 11 +++++------ src/ext/zrapp/deadcodeelim.ml | 2 +- src/frontc/cparser.mly | 22 +++++++++++++++++++++- src/frontc/cprint.ml | 31 +++++++++++++++++-------------- 4 files changed, 44 insertions(+), 22 deletions(-) diff --git a/src/ext/liveness/usedef.ml b/src/ext/liveness/usedef.ml index 7728afd43..b1d446899 100644 --- a/src/ext/liveness/usedef.ml +++ b/src/ext/liveness/usedef.ml @@ -241,12 +241,11 @@ let rec computeDeepUseDefStmtKind ?(acc_used=VS.empty) List.iter (fun i -> ignore (visitCilInstr useDefVisitor i)) il; !varUsed, !varDefs | Block b -> handle_block b - | Asm(_,_,slvl,_,_,_,_) -> List.iter (fun (_,s,lv) -> - match lv with (Var v, off) -> - if s.[0] = '+' then - varUsed := VS.add v !varUsed; - | _ -> ()) slvl; - !varUsed, !varDefs + | Asm (a, b, c, d, e, f, g) -> + computeUseDefStmtKind + ~acc_used:!varUsed + ~acc_defs:!varDefs + (Asm (a, b, c, d, e, f, g)) let computeUseLocalTypes ?(acc_used=VS.empty) (fd : fundec) diff --git a/src/ext/zrapp/deadcodeelim.ml b/src/ext/zrapp/deadcodeelim.ml index c55900bcf..96d8d814d 100644 --- a/src/ext/zrapp/deadcodeelim.ml +++ b/src/ext/zrapp/deadcodeelim.ml @@ -111,7 +111,7 @@ class usedDefsCollectorClass = object(self) method! vinst i = let handle_inst iosh i = match i with - Call(_,ce,el,_,_) when not (!callHasNoSideEffects i) -> + | Call(_,ce,el,_,_) when not (!callHasNoSideEffects i) -> List.iter (fun e -> let u = UD.computeUseExp e in UD.VS.iter (fun vi -> diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 2050a2a8c..1e7fb071c 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -244,6 +244,26 @@ let transformOffsetOf (speclist, dtype) member = queue; Buffer.contents buffer + (* this makes sure that the labels are only allowed when goto annotation was provided *) + let checkAsm asm = + let labels_no_goto = "labels provided in inline asm without goto attribute" in + let goto_no_labels = "expected non-empty labels list in asm goto" in + (match asm with + | ASM (attrs, _, details, _) -> + (match details, (List.assoc_opt "goto" attrs) with + | None, Some _ -> + parse_error goto_no_labels; + raise Parsing.Parse_error + | Some details, Some _ when details.agotos = [] -> + parse_error goto_no_labels; + raise Parsing.Parse_error + | Some details, None when details.agotos <> [] -> + parse_error labels_no_goto; + raise Parsing.Parse_error + | _, _ -> ()) + | _ -> failwith "called checkAsm on non-ASM variant"); + asm + %} %token IDENT @@ -983,7 +1003,7 @@ statement_no_null: | GOTO STAR comma_expression SEMICOLON { COMPGOTO (smooth_expression (fst $3), joinLoc $1 $4) } | ASM asmattr LPAREN asmtemplate asmoutputs RPAREN SEMICOLON - { ASM ($2, $4, $5, joinLoc $1 $7) } + { checkAsm (ASM ($2, $4, $5, joinLoc $1 $7)) } | error location SEMICOLON { (NOP $2)} ; diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 3d86faec7..2c9d8193f 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -717,22 +717,25 @@ and print_statement stat = print_attributes attrs; print "("; print_list (fun () -> new_line()) print_string tlist; (* templates *) - begin - match details with - | None -> () - | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; agotos = gotos } -> + begin + match details with + | None -> () + | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; agotos = labels } -> print ":"; space (); print_commas false print_asm_operand outs; - if ins <> [] || clobs <> [] then begin - print ":"; space (); - print_commas false print_asm_operand ins; - if clobs <> [] then begin - print ":"; space (); - print_commas false print_string clobs - end; - end - end; - print ");" + if ins <> [] || clobs <> [] || labels <> [] then begin + print ":"; space (); + print_commas false print_asm_operand ins; + if clobs <> [] || labels <> [] then begin + print ":"; space (); + print_commas false print_string clobs; + if labels <> [] then + print ":"; space (); + print_commas false print labels + end; + end; + end; + print ");"; end; new_line () From 395bb4e89e4a99879c5be446818d9daf7bff8745 Mon Sep 17 00:00:00 2001 From: Jevgenijs Protopopovs Date: Fri, 16 Jan 2026 11:12:05 +0200 Subject: [PATCH 7/7] Integrate test cases from #161 --- test/small1/{asm6.c => asm_goto0.c} | 0 test/small1/asm_goto1.c | 6 ++++++ test/small1/asm_goto2.c | 6 ++++++ test/small1/asm_goto3.c | 8 ++++++++ test/small1/asm_goto4.c | 8 ++++++++ test/small1/asm_goto5.c | 6 ++++++ test/small1/asm_goto6.c | 6 ++++++ test/testcil.pl | 8 +++++++- 8 files changed, 47 insertions(+), 1 deletion(-) rename test/small1/{asm6.c => asm_goto0.c} (100%) create mode 100644 test/small1/asm_goto1.c create mode 100644 test/small1/asm_goto2.c create mode 100644 test/small1/asm_goto3.c create mode 100644 test/small1/asm_goto4.c create mode 100644 test/small1/asm_goto5.c create mode 100644 test/small1/asm_goto6.c diff --git a/test/small1/asm6.c b/test/small1/asm_goto0.c similarity index 100% rename from test/small1/asm6.c rename to test/small1/asm_goto0.c diff --git a/test/small1/asm_goto1.c b/test/small1/asm_goto1.c new file mode 100644 index 000000000..c95eb4ee4 --- /dev/null +++ b/test/small1/asm_goto1.c @@ -0,0 +1,6 @@ +#include "testharness.h" + +int main() { + asm goto ("nop"); + E(1); +} \ No newline at end of file diff --git a/test/small1/asm_goto2.c b/test/small1/asm_goto2.c new file mode 100644 index 000000000..56994c285 --- /dev/null +++ b/test/small1/asm_goto2.c @@ -0,0 +1,6 @@ +#include "testharness.h" + +void code() { + asm goto ("nop" : ); + E(1); +} \ No newline at end of file diff --git a/test/small1/asm_goto3.c b/test/small1/asm_goto3.c new file mode 100644 index 000000000..eeefb0d0b --- /dev/null +++ b/test/small1/asm_goto3.c @@ -0,0 +1,8 @@ +#include "testharness.h" + +int main(void) { +start: + asm goto ("nop" : : : : start, exit); +exit: + SUCCESS; +} \ No newline at end of file diff --git a/test/small1/asm_goto4.c b/test/small1/asm_goto4.c new file mode 100644 index 000000000..51858f55c --- /dev/null +++ b/test/small1/asm_goto4.c @@ -0,0 +1,8 @@ +#include "testharness.h" + +void code() { +start: + asm("nop" : : : : start, exit); +exit: + E(1); +} \ No newline at end of file diff --git a/test/small1/asm_goto5.c b/test/small1/asm_goto5.c new file mode 100644 index 000000000..ed7495ccc --- /dev/null +++ b/test/small1/asm_goto5.c @@ -0,0 +1,6 @@ +#include "testharness.h" + +void code() { + asm goto ("nop" : : : : start, exit); + E(1); +} \ No newline at end of file diff --git a/test/small1/asm_goto6.c b/test/small1/asm_goto6.c new file mode 100644 index 000000000..b0b01fd6d --- /dev/null +++ b/test/small1/asm_goto6.c @@ -0,0 +1,6 @@ +#include "testharness.h" + +void code() { + asm goto ("nop" : : : ); + E(1); +} \ No newline at end of file diff --git a/test/testcil.pl b/test/testcil.pl index 69e90e41d..825735d0d 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -182,7 +182,13 @@ sub addToGroup { addTest("test/asm4 _GNUCC=1"); addTest("test/asm_emptyclobberallowed _GNUCC=1"); addTest("testobj/asm5 _GNUCC=1"); -addTest("test/asm6"); +addTest("test/asm_goto0"); +addTestFail("test/asm_goto1", "expected non-empty labels list in asm goto"); +addTestFail("test/asm_goto2", "expected non-empty labels list in asm goto"); +addTest("test/asm_goto3"); +addTestFail("test/asm_goto4", "labels provided in inline asm without goto attribute"); +addTestFail("test/asm_goto5", "Error: Label start not found"); +addTestFail("test/asm_goto6", "expected non-empty labels list in asm goto"); addTest("testrun/offsetof"); addTest("testrun/offsetof1");