Skip to content
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

Add support for parsing asm goto #92

Closed
wants to merge 2 commits into from
+65 −32
Closed

Add support for parsing asm goto #92

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4bbf8ad
track in cil if a asm is basic
bottbenj Apr 4, 2022
242c744
bring back asm goto parsing
bottbenj Apr 5, 2022
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
33 changes: 23 additions & 10 deletions src/cil.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -839,7 +839,7 @@ and instr =
| Asm of attributes * (* Really only const and volatile can appear
* here *)
string list * (* templates (CR-separated) *)
(string option * string * lval) list *
((string option * string * lval) list *
(* outputs must be lvals with
* optional names and constraints.
* I would like these
Expand All @@ -849,6 +849,7 @@ and instr =
(string option * string * exp) list *
(* inputs with optional names and constraints *)
string list * (* register clobbers *)
string list) option * (* goto locations *)
location
(** An inline assembly instruction. The arguments are (1) a list of
attributes (only const and volatile can appear here and only for
Expand Down Expand Up @@ -1113,7 +1114,7 @@ let get_instrLoc (inst : instr) =
match inst with
Set(_, _, loc, _) -> loc
| Call(_, _, _, loc, _) -> loc
| Asm(_, _, _, _, _, loc) -> loc
| Asm(_, _, _, loc) -> loc
| VarDecl(_,loc) -> loc
let get_globalLoc (g : global) =
match g with
Expand Down Expand Up @@ -1341,7 +1342,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 = (Asm([], ["dummy statement!!"], None, lu))
let dummyStmt = mkStmt (Instr [dummyInstr])

let compactStmts (b: stmt list) : stmt list =
Expand Down Expand Up @@ -3673,7 +3674,8 @@ class defaultCilPrinterClass : cilPrinter = object (self)
++ unalign)
++ text (")" ^ printInstrTerminator)

| Asm(attrs, tmpls, outs, ins, clobs, l) ->
| Asm(attrs, tmpls, details, l) ->
let (outs, ins, clobs, gotos) = Option.value ~default:([],[],[],[]) details in
self#pLineDirective l
++ text ("__asm__ ")
++ self#pAttrs () attrs
Expand All @@ -3683,7 +3685,9 @@ class defaultCilPrinterClass : cilPrinter = object (self)
(fun x -> text ("\"" ^ escape_string x ^ "\""))
() tmpls)
++
(if outs = [] && ins = [] && clobs = [] then
(if details = None then
nil
else if outs = [] && ins = [] && clobs = [] && gotos = [] then
chr ':'
else
(text ": "
Expand All @@ -3697,7 +3701,7 @@ class defaultCilPrinterClass : cilPrinter = object (self)
++ self#pLval () lv
++ text ")") () outs)))
++
(if ins = [] && clobs = [] then
(if ins = [] && clobs = [] && gotos = [] then
nil
else
(text ": "
Expand All @@ -3711,13 +3715,21 @@ class defaultCilPrinterClass : cilPrinter = object (self)
++ self#pExp () e
++ text ")") () ins)))
++
(if clobs = [] then nil
(if clobs = [] && gotos = [] then nil
else
(text ": "
++ (docList ~sep:(chr ',' ++ break)
(fun c -> text ("\"" ^ escape_string c ^ "\""))
()
clobs)))
++
(if gotos = [] then nil
else
(text ": "
++ (docList ~sep:(chr ',' ++ break)
text
()
gotos)))
++ unalign)
++ text (")" ^ printInstrTerminator)

Expand Down Expand Up @@ -5290,15 +5302,16 @@ 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) ->
| Asm(sl,isvol,Some(outs,ins,clobs,gotos),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
Asm(sl,isvol,Some(outs',ins',clobs,gotos),l) else i
| Asm _ -> i


(* visit all nodes in a Cil statement tree in preorder *)
Expand Down Expand Up @@ -5971,7 +5984,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 -> Asm([], [sprint ~width:!lineLength d], None, l)

let dGlobal: doc -> location -> global =
fun d l -> GAsm(sprint ~width:!lineLength d, l)
Expand Down
3 changes: 2 additions & 1 deletion src/cil.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1034,7 +1034,7 @@ and instr =
| Asm of attributes * (* Really only const and volatile can appear
* here *)
string list * (* templates (CR-separated) *)
(string option * string * lval) list *
((string option * string * lval) list *
(* outputs must be lvals with
* optional names and constraints.
* I would like these
Expand All @@ -1044,6 +1044,7 @@ and instr =
(string option * string * exp) list *
(* inputs with optional names and constraints *)
string list * (* register clobbers *)
string list) option * (* goto locations *)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not clear from here, why this additional option wrapping is necessary or what the None then means.

location
(** There are for storing inline assembly. They follow the GCC
* specification:
Expand Down
2 changes: 1 addition & 1 deletion src/ext/liveness/usedef.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -151,7 +151,7 @@ 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) ->
| Asm(_,_,Some(slvl,_,_,_),_) -> List.iter (fun (_,s,lv) ->
match lv with (Var v, off) ->
if s.[0] = '+' then
varUsed := VS.add v !varUsed;
Expand Down
2 changes: 1 addition & 1 deletion src/ext/zrapp/availexps.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -243,7 +243,7 @@ let eh_handle_inst i eh =
(eh_kill_mem eh;
eh_kill_addrof_or_global eh;
eh)
| Asm(_,_,_,_,_,_) ->
| Asm(_,_,_,_) ->
let _,d = UD.computeUseDefInstr i in
(UD.VS.iter (fun vi ->
eh_kill_vi eh vi) d;
Expand Down
2 changes: 1 addition & 1 deletion src/ext/zrapp/availexpslv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -305,7 +305,7 @@ let lvh_handle_inst i lvh =
end;
lvh
end
| Asm(_,_,_,_,_,_) -> begin
| Asm(_,_,_,_) -> begin
let _,d = UD.computeUseDefInstr i in
UD.VS.iter (fun vi ->
lvh_kill_vi lvh vi) d;
Expand Down
2 changes: 1 addition & 1 deletion src/ext/zrapp/deadcodeelim.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ class usedDefsCollectorClass = object(self)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Commenting here since I can only comment on the diff: We should check if these zrapp analysis potentially break after this change (quite likely).
Unless we're super sure that they don't break, we should comment that they assume no asm gotos. We mostly have these for historical reasons anyway (came from original CIL), so it's not worth adding proper handling here (as our focus is on Goblint).

Nevertheless, let's add comments that make it clear we have not patched them to support these new constructs.

method! vinst i =
let handle_inst iosh i = match i with
| Asm(_,_,slvl,_,_,_) -> List.iter (fun (_,s,lv) ->
| Asm(_,_,Some(slvl,_,_,_),_) -> List.iter (fun (_,s,lv) ->
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is just ignoring the None case the same that we would have had for the dummy statement before?

match lv with (Var v, off) ->
if s.[0] = '+' then
self#add_defids iosh (Lval(Var v, off)) (UD.VS.singleton v)
Expand Down
4 changes: 2 additions & 2 deletions src/ext/zrapp/reachingdefs.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -270,7 +270,7 @@ 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
| Asm(_,_,Some(sll,_,_,_),_) -> List.exists
(function (_,_,(Var vi',NoOffset)) -> vi'.vid = vid | _ -> false) sll
| _ -> false)
| None -> false) iihl in
Expand All @@ -284,7 +284,7 @@ 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
| Asm(a,sl,_,_) -> None
| VarDecl _ -> None
) (* ? *)
with Not_found ->
Expand Down
2 changes: 1 addition & 1 deletion src/ext/zrapp/rmciltmps.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -994,7 +994,7 @@ class unusedRemoverClass : cilVisitor = object(self)
(match IH.find iioh vi.vid with
None -> true | Some _ -> false)
end
| Asm(_,_,slvlst,_,_,_) -> begin
| Asm(_,_,Some(slvlst,_,_,_),_) -> begin
(* make sure the outputs are in the locals list *)
List.iter (fun (_,s,lv) ->
match lv with (Var vi,_) ->
Expand Down
3 changes: 2 additions & 1 deletion src/frontc/cabs.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -209,7 +209,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; (* asm goto locations *)
}

and statement =
Expand Down
10 changes: 5 additions & 5 deletions src/frontc/cabs2cil.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6833,16 +6833,16 @@ 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', details) =
match details with
| None ->
let tmpls' =
let pattern = Str.regexp "%" in
let escape = Str.global_replace pattern "%%" in
Util.list_map escape tmpls
in
(tmpls', [], [], [])
| Some { aoutputs = outs; ainputs = ins; aclobbers = clobs } ->
(tmpls', None)
| Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; agotos = gotos } ->
let outs' =
Util.list_map
(fun (id, c, e) ->
Expand All @@ -6865,10 +6865,10 @@ and doStatement (s : A.statement) : chunk =
(id, c, e'))
ins
in
(tmpls, outs', ins', clobs)
(tmpls, Some (outs', ins', clobs, gotos))
in
!stmts @@
(i2c (Asm(attr', tmpls', outs', ins', clobs', loc')))
(i2c (Asm(attr', tmpls', details, loc')))

with e when continueOnError -> begin
(ignore (E.log "Error in doStatement (%s)\n" (Printexc.to_string e)));
Expand Down
4 changes: 2 additions & 2 deletions src/frontc/cabsvisit.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -440,13 +440,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
Expand Down
24 changes: 19 additions & 5 deletions src/frontc/cparser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1644,6 +1644,7 @@ asmattr:
/* empty */ { [] }
| VOLATILE asmattr { ("volatile", []) :: $2 }
| CONST asmattr { ("const", []) :: $2 }
| GOTO asmattr { ("goto", []) :: $2 }
;
asmtemplate:
one_string_constant { [$1] }
Expand All @@ -1652,8 +1653,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 */ { [] }
Expand All @@ -1670,7 +1671,7 @@ asmoperand:
;

asminputs:
/* empty */ { ([], []) }
/* empty */ { ([], ([], [])) }
| COLON asmoperands asmclobber
{ ($2, $3) }
;
Expand All @@ -1680,8 +1681,8 @@ asmopname:
;

asmclobber:
/* empty */ { [] }
| COLON asmcloberlst { $2 }
/* empty */ { ([], []) }
| COLON asmcloberlst asmgoto { ($2, $3) }
;
asmcloberlst:
/* empty */ { [] }
Expand All @@ -1692,4 +1693,17 @@ asmcloberlst_ne:
| one_string_constant COMMA asmcloberlst_ne { $1 :: $3 }
;

asmgoto:
/* empty */ { [] }
| COLON asmgotolst { $2 }
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is just COLON a valid asmgoto?

;
asmgotolst:
/* empty */ { [] }
| asmgotolst_ne { $1 }
;
asmgotolst_ne:
IDENT { [ fst $1 ] }
| IDENT COMMA asmgotolst_ne { ( fst $1 ) :: $3 }
;

%%
6 changes: 5 additions & 1 deletion src/frontc/cprint.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -718,7 +718,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
Expand All @@ -728,6 +728,10 @@ and print_statement stat =
print ":"; space ();
print_commas false print_string clobs
end;
if gotos <> [] then begin
print ":"; space ();
print_commas false print gotos
end;
end
end;
print ");"
Expand Down