From 4bbf8ad1689e3a83c6b2a5bc08fa1c86790b29c6 Mon Sep 17 00:00:00 2001 From: Benjamin Bott Date: Tue, 5 Apr 2022 00:07:28 +0200 Subject: [PATCH 1/2] track in cil if a asm is basic --- src/cil.ml | 22 +++++++++++++--------- src/cil.mli | 4 ++-- src/ext/liveness/usedef.ml | 2 +- src/ext/zrapp/availexps.ml | 2 +- src/ext/zrapp/availexpslv.ml | 2 +- src/ext/zrapp/deadcodeelim.ml | 2 +- src/ext/zrapp/reachingdefs.ml | 4 ++-- src/ext/zrapp/rmciltmps.ml | 2 +- src/frontc/cabs2cil.ml | 8 ++++---- 9 files changed, 26 insertions(+), 22 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 288c49ce4..6a8a57310 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -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 @@ -848,7 +848,7 @@ and instr = * in the Linux sources *) (string option * string * exp) list * (* inputs with optional names and constraints *) - string list * (* register clobbers *) + string list) option * (* 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 @@ -1113,7 +1113,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 @@ -1341,7 +1341,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 = @@ -3673,7 +3673,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) = Option.value ~default:([],[],[]) details in self#pLineDirective l ++ text ("__asm__ ") ++ self#pAttrs () attrs @@ -3683,7 +3684,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 = [] then chr ':' else (text ": " @@ -5290,7 +5293,7 @@ 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),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 @@ -5298,7 +5301,8 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr = 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),l) else i + | Asm _ -> i (* visit all nodes in a Cil statement tree in preorder *) @@ -5971,7 +5975,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) diff --git a/src/cil.mli b/src/cil.mli index 57d0be532..0959e9394 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -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 @@ -1043,7 +1043,7 @@ and instr = * in the Linux sources *) (string option * string * exp) list * (* inputs with optional names and constraints *) - string list * (* register clobbers *) + string list) option * (* register clobbers *) location (** There are for storing inline assembly. They follow the GCC * specification: diff --git a/src/ext/liveness/usedef.ml b/src/ext/liveness/usedef.ml index f313e11e9..1c4066b85 100644 --- a/src/ext/liveness/usedef.ml +++ b/src/ext/liveness/usedef.ml @@ -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; diff --git a/src/ext/zrapp/availexps.ml b/src/ext/zrapp/availexps.ml index 2763989c8..0ab0e1142 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(_,_,_,_,_,_) -> + | Asm(_,_,_,_) -> 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 5901403a3..c7faed700 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 + | Asm(_,_,_,_) -> 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 d1e754b08..8ec7af0d7 100644 --- a/src/ext/zrapp/deadcodeelim.ml +++ b/src/ext/zrapp/deadcodeelim.ml @@ -102,7 +102,7 @@ class usedDefsCollectorClass = object(self) 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) -> match lv with (Var v, off) -> if s.[0] = '+' then self#add_defids iosh (Lval(Var v, off)) (UD.VS.singleton v) diff --git a/src/ext/zrapp/reachingdefs.ml b/src/ext/zrapp/reachingdefs.ml index 23b4b0d14..b99205c76 100644 --- a/src/ext/zrapp/reachingdefs.ml +++ b/src/ext/zrapp/reachingdefs.ml @@ -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 @@ -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 -> diff --git a/src/ext/zrapp/rmciltmps.ml b/src/ext/zrapp/rmciltmps.ml index 4af909fc6..1344586da 100644 --- a/src/ext/zrapp/rmciltmps.ml +++ b/src/ext/zrapp/rmciltmps.ml @@ -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,_) -> diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index c60c29727..46486cdc2 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -6833,7 +6833,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', details) = match details with | None -> let tmpls' = @@ -6841,7 +6841,7 @@ and doStatement (s : A.statement) : chunk = let escape = Str.global_replace pattern "%%" in Util.list_map escape tmpls in - (tmpls', [], [], []) + (tmpls', None) | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs } -> let outs' = Util.list_map @@ -6865,10 +6865,10 @@ and doStatement (s : A.statement) : chunk = (id, c, e')) ins in - (tmpls, outs', ins', clobs) + (tmpls, Some (outs', ins', clobs)) 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))); From 242c7449f02690e38fe505d1642de288b52a8ddc Mon Sep 17 00:00:00 2001 From: Benjamin Bott Date: Tue, 5 Apr 2022 09:59:35 +0200 Subject: [PATCH 2/2] bring back asm goto parsing --- src/cil.ml | 23 ++++++++++++++++------- src/cil.mli | 3 ++- src/ext/liveness/usedef.ml | 2 +- src/ext/zrapp/deadcodeelim.ml | 2 +- src/ext/zrapp/reachingdefs.ml | 2 +- src/ext/zrapp/rmciltmps.ml | 2 +- src/frontc/cabs.ml | 3 ++- src/frontc/cabs2cil.ml | 4 ++-- src/frontc/cabsvisit.ml | 4 ++-- src/frontc/cparser.mly | 24 +++++++++++++++++++----- src/frontc/cprint.ml | 6 +++++- 11 files changed, 52 insertions(+), 23 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 6a8a57310..e8fea5787 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -848,7 +848,8 @@ and instr = * in the Linux sources *) (string option * string * exp) list * (* inputs with optional names and constraints *) - string list) option * (* register clobbers *) + 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 @@ -3674,7 +3675,7 @@ class defaultCilPrinterClass : cilPrinter = object (self) ++ text (")" ^ printInstrTerminator) | Asm(attrs, tmpls, details, l) -> - let (outs, ins, clobs) = Option.value ~default:([],[],[]) details in + let (outs, ins, clobs, gotos) = Option.value ~default:([],[],[],[]) details in self#pLineDirective l ++ text ("__asm__ ") ++ self#pAttrs () attrs @@ -3686,7 +3687,7 @@ class defaultCilPrinterClass : cilPrinter = object (self) ++ (if details = None then nil - else if outs = [] && ins = [] && clobs = [] then + else if outs = [] && ins = [] && clobs = [] && gotos = [] then chr ':' else (text ": " @@ -3700,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 ": " @@ -3714,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) @@ -5293,7 +5302,7 @@ 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,Some(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 @@ -5301,7 +5310,7 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr = 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,Some(outs',ins',clobs),l) else i + Asm(sl,isvol,Some(outs',ins',clobs,gotos),l) else i | Asm _ -> i diff --git a/src/cil.mli b/src/cil.mli index 0959e9394..13dd2da19 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -1043,7 +1043,8 @@ and instr = * in the Linux sources *) (string option * string * exp) list * (* inputs with optional names and constraints *) - string list) option * (* register clobbers *) + string list * (* register clobbers *) + string list) option * (* goto locations *) location (** There are for storing inline assembly. They follow the GCC * specification: diff --git a/src/ext/liveness/usedef.ml b/src/ext/liveness/usedef.ml index 1c4066b85..e139f5bf5 100644 --- a/src/ext/liveness/usedef.ml +++ b/src/ext/liveness/usedef.ml @@ -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(_,_,Some(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; diff --git a/src/ext/zrapp/deadcodeelim.ml b/src/ext/zrapp/deadcodeelim.ml index 8ec7af0d7..1dbbaa9ea 100644 --- a/src/ext/zrapp/deadcodeelim.ml +++ b/src/ext/zrapp/deadcodeelim.ml @@ -102,7 +102,7 @@ class usedDefsCollectorClass = object(self) method! vinst i = let handle_inst iosh i = match i with - | Asm(_,_,Some(slvl,_,_),_) -> List.iter (fun (_,s,lv) -> + | Asm(_,_,Some(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) diff --git a/src/ext/zrapp/reachingdefs.ml b/src/ext/zrapp/reachingdefs.ml index b99205c76..8cde80533 100644 --- a/src/ext/zrapp/reachingdefs.ml +++ b/src/ext/zrapp/reachingdefs.ml @@ -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(_,_,Some(sll,_,_),_) -> List.exists + | Asm(_,_,Some(sll,_,_,_),_) -> List.exists (function (_,_,(Var vi',NoOffset)) -> vi'.vid = vid | _ -> false) sll | _ -> false) | None -> false) iihl in diff --git a/src/ext/zrapp/rmciltmps.ml b/src/ext/zrapp/rmciltmps.ml index 1344586da..6a2365ac9 100644 --- a/src/ext/zrapp/rmciltmps.ml +++ b/src/ext/zrapp/rmciltmps.ml @@ -994,7 +994,7 @@ class unusedRemoverClass : cilVisitor = object(self) (match IH.find iioh vi.vid with None -> true | Some _ -> false) end - | Asm(_,_,Some(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,_) -> diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index a46cb2e7c..e6489a084 100644 --- a/src/frontc/cabs.ml +++ b/src/frontc/cabs.ml @@ -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 = diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 46486cdc2..9eb880be7 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -6842,7 +6842,7 @@ and doStatement (s : A.statement) : chunk = Util.list_map escape tmpls in (tmpls', None) - | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs } -> + | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs; agotos = gotos } -> let outs' = Util.list_map (fun (id, c, e) -> @@ -6865,7 +6865,7 @@ and doStatement (s : A.statement) : chunk = (id, c, e')) ins in - (tmpls, Some (outs', ins', clobs)) + (tmpls, Some (outs', ins', clobs, gotos)) in !stmts @@ (i2c (Asm(attr', tmpls', details, loc'))) diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml index a2dd69d1b..528927d55 100644 --- a/src/frontc/cabsvisit.ml +++ b/src/frontc/cabsvisit.ml @@ -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 diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 7e76f54c0..7784fffa9 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -1644,6 +1644,7 @@ asmattr: /* empty */ { [] } | VOLATILE asmattr { ("volatile", []) :: $2 } | CONST asmattr { ("const", []) :: $2 } +| GOTO asmattr { ("goto", []) :: $2 } ; asmtemplate: one_string_constant { [$1] } @@ -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 */ { [] } @@ -1670,7 +1671,7 @@ asmoperand: ; asminputs: - /* empty */ { ([], []) } + /* empty */ { ([], ([], [])) } | COLON asmoperands asmclobber { ($2, $3) } ; @@ -1680,8 +1681,8 @@ asmopname: ; asmclobber: - /* empty */ { [] } -| COLON asmcloberlst { $2 } + /* empty */ { ([], []) } +| COLON asmcloberlst asmgoto { ($2, $3) } ; asmcloberlst: /* empty */ { [] } @@ -1692,4 +1693,17 @@ asmcloberlst_ne: | one_string_constant COMMA asmcloberlst_ne { $1 :: $3 } ; +asmgoto: + /* empty */ { [] } +| COLON asmgotolst { $2 } +; +asmgotolst: + /* empty */ { [] } +| asmgotolst_ne { $1 } +; +asmgotolst_ne: + IDENT { [ fst $1 ] } +| IDENT COMMA asmgotolst_ne { ( fst $1 ) :: $3 } +; + %% diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index fae86f0b4..3e9a31ace 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -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 @@ -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 ");"