Skip to content

Implement goto labels from GCC extended inline assembly syntax. #203

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jprotopopov-ut wants to merge 7 commits into
base: develop
Choose a base branch
from
Open

Implement goto labels from GCC extended inline assembly syntax. #203

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
4a4e814
Implement goto labels from GCC extended inline assembly syntax.
jprotopopov-ut Apr 15, 2025
c2c20fe
Update testcil.pl with new inline assembly goto parsing test
jprotopopov-ut Jan 14, 2026
bfdeb86
Revert to the original definition of dummyStmt
jprotopopov-ut Jan 15, 2026
a47bd17
Remove DummyInstr instructiontype
jprotopopov-ut Jan 15, 2026
b70dae0
Rollback spurious changes to reduce diff clutter
jprotopopov-ut Jan 16, 2026
00120f7
Integrate some of the changes from #161
jprotopopov-ut Jan 16, 2026
395bb4e
Integrate test cases from #161
jprotopopov-ut Jan 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion src/cfg.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

(*------------------------------------------------------------*)

Expand All @@ -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
;;

Expand All @@ -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

Expand Down
18 changes: 15 additions & 3 deletions src/check.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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");
"<missing label>"
in
(* Remember it as a target *)
gotoTargets := (lab, !gref) :: !gotoTargets
) gotos
| Instr il -> List.iter checkInstr il)
() (* argument of withContext *)

Expand Down Expand Up @@ -885,8 +899,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 _ -> ()
Expand Down
202 changes: 115 additions & 87 deletions src/cil.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -823,6 +823,27 @@ 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.*)
Expand Down Expand Up @@ -856,26 +877,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 *)



Expand Down Expand Up @@ -1136,7 +1137,6 @@ let get_instrLoc (inst : instr) =
match inst with
Set(_, _, loc, _) -> loc
| Call(_, _, _, loc, _) -> loc
| Asm(_, _, _, _, _, loc) -> loc
| VarDecl(_,loc) -> loc
let get_globalLoc (g : global) =
match g with
Expand Down Expand Up @@ -1166,6 +1166,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 *)
Expand Down Expand Up @@ -1364,8 +1365,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 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
Expand Down Expand Up @@ -3749,54 +3749,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 *)
Expand Down Expand Up @@ -4018,6 +3970,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 ***)
Expand Down Expand Up @@ -4372,6 +4393,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 ->
Expand Down Expand Up @@ -5371,16 +5393,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 =
Expand Down Expand Up @@ -5443,6 +5455,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 *)
Expand Down Expand Up @@ -5934,7 +5955,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 *)
Expand Down Expand Up @@ -5962,7 +5983,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


Expand Down Expand Up @@ -6055,8 +6076,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 -> Asm([], [sprint ~width:!lineLength d], [], [], [], 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)
Expand Down Expand Up @@ -6429,6 +6450,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;
Expand Down Expand Up @@ -6470,7 +6495,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)
Expand Down Expand Up @@ -6541,6 +6566,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 _ ->
Expand Down Expand Up @@ -6631,7 +6659,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 ->
Expand Down
Loading