Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Merge branch 'labelasvalue' into develop

  • Loading branch information...
commit 49f06059be695475d133a7b904d9e6597c4c9c73 2 parents 8eef4a1 + 65e6952
@kerneis kerneis authored
View
2  ocamlutil/Makefile.ocaml
@@ -186,7 +186,7 @@ CAMLP4 = camlp4 pa_o.cmo pa_op.cmo pr_o.cmo
# Internal versions of COMPILEFLAGS and LINKFLAGS. We'll add additional flags
# to these.
-COMPILE_FLAGS := $(COMPILEFLAGS)
+COMPILE_FLAGS := $(COMPILEFLAGS) -warn-error +a
LINK_FLAGS := $(LINKFLAGS)
COMPILE_FLAGS += -I $(OBJDIR)
View
20 src/check.ml
@@ -570,6 +570,20 @@ and checkExp (isconst: bool) (e: exp) : typ =
| _ -> E.s (bug "AddrOf on unknown type")
end
+ | AddrOfLabel (gref) -> begin
+ (* Find a label *)
+ let lab =
+ match List.filter (function Label _ -> true | _ -> false)
+ !gref.labels with
+ Label (lab, _, _) :: _ -> lab
+ | _ ->
+ ignore (warn "Address of label to block without a label");
+ "<missing label>"
+ in
+ (* Remember it as a target *)
+ gotoTargets := (lab, !gref) :: !gotoTargets;
+ voidPtrType
+ end
| StartOf lv -> begin
let tlv = checkLval isconst true lv in
match unrollType tlv with
@@ -727,8 +741,10 @@ and checkStmt (s: stmt) =
in
(* Remember it as a target *)
gotoTargets := (lab, !gref) :: !gotoTargets
-
-
+ | ComputedGoto (e, l) ->
+ currentLoc := l;
+ let te = checkExp false e in
+ typeMatch te voidPtrType
| Return (re,l) -> begin
currentLoc := l;
match re, !currentReturnType with
View
79 src/cil.ml
@@ -77,6 +77,8 @@ let makeStaticGlobal = ref true
let useLogicalOperators = ref false
+let useComputedGoto = ref false
+
module M = Machdep
(* Cil.initCil will set this to the current machine description.
@@ -504,6 +506,7 @@ and exp =
* construct one of these. Apply to an
* lvalue of type [T] yields an
* expression of type [TPtr(T)] *)
+ | AddrOfLabel of stmt ref
| StartOf of lval (** There is no C correspondent for this. C has
* implicit coercions from an array to the address
@@ -735,6 +738,9 @@ and stmtkind =
| Goto of stmt ref * location (** A goto statement. Appears from
actual goto's in the code. *)
+
+ | ComputedGoto of exp * location
+
| Break of location (** A break to the end of the nearest
enclosing Loop or Switch *)
| Continue of location (** A continue to the start of the
@@ -1110,6 +1116,7 @@ let rec get_stmtLoc (statement : stmtkind) =
| Instr(hd::tl) -> get_instrLoc(hd)
| Return(_, loc) -> loc
| Goto(_, loc) -> loc
+ | ComputedGoto(_, loc) -> loc
| Break(loc) -> loc
| Continue(loc) -> loc
| If(_, _, _, loc) -> loc
@@ -1790,6 +1797,7 @@ let getParenthLevel (e: exp) =
(* Unary *)
| CastE(_,_) -> 30
| AddrOf(_) -> 30
+ | AddrOfLabel(_) -> 30
| StartOf(_) -> 30
| UnOp((Neg|BNot|LNot),_,_) -> 30
@@ -1890,6 +1898,7 @@ let rec typeOf (e: exp) : typ =
| Question (_, _, _, t)
| CastE (t, _) -> t
| AddrOf (lv) -> TPtr(typeOfLval lv, [])
+ | AddrOfLabel (lv) -> voidPtrType
| StartOf (lv) -> begin
match unrollType (typeOfLval lv) with
TArray (t,_, a) -> TPtr(t, a)
@@ -3327,6 +3336,19 @@ class defaultCilPrinterClass : cilPrinter = object (self)
text "__alignof__(" ++ self#pExp () e ++ chr ')'
| AddrOf(lv) ->
text "& " ++ (self#pLvalPrec addrOfLevel () lv)
+ | AddrOfLabel(sref) -> begin
+ (* Grab one of the labels *)
+ let rec pickLabel = function
+ [] -> None
+ | Label (l, _, _) :: _ -> Some l
+ | _ :: rest -> pickLabel rest
+ in
+ match pickLabel !sref.labels with
+ Some lbl -> text ("&& " ^ lbl)
+ | None ->
+ ignore (error "Cannot find label for target of address of label");
+ text "&& __invalid_label"
+ end
| StartOf(lv) -> self#pLval () lv
@@ -3771,6 +3793,12 @@ class defaultCilPrinterClass : cilPrinter = object (self)
text "goto __invalid_label;"
end
+ | ComputedGoto(e, l) ->
+ self#pLineDirective l
+ ++ text "goto *("
+ ++ self#pExp () e
+ ++ text ");"
+
| Break l ->
self#pLineDirective l
++ text "break;"
@@ -4634,6 +4662,7 @@ class plainCilPrinterClass =
| StartOf lv -> dprintf "StartOf(%a)" self#pLval lv
| AddrOf (lv) -> dprintf "AddrOf(%a)" self#pLval lv
+ | AddrOfLabel (sref) -> dprintf "AddrOfLabel(%a)" self#pStmt !sref
@@ -5128,6 +5157,7 @@ and childrenExp (vis: cilVisitor) (e: exp) : exp =
| AddrOf lv ->
let lv' = vLval lv in
if lv' != lv then AddrOf lv' else e
+ | AddrOfLabel _ -> e
| StartOf lv ->
let lv' = vLval lv in
if lv' != lv then StartOf lv' else e
@@ -5266,6 +5296,9 @@ and childrenStmt (toPrepend: instr list ref) : cilVisitor -> stmt -> stmt =
let skind' =
match s.skind with
Break _ | Continue _ | Goto _ | Return (None, _) -> s.skind
+ | ComputedGoto (e, l) ->
+ let e' = fExp e in
+ if e' != e then ComputedGoto (e', l) else s.skind
| Return (Some e, l) ->
let e' = fExp e in
if e' != e then Return (Some e', l) else s.skind
@@ -5810,7 +5843,7 @@ let rec peepHole1 (* Process one instruction and possibly replace it *)
peepHole1 doone b.bstmts;
peepHole1 doone h.bstmts;
s.skind <- TryExcept(b, (doInstrList il, e), h, l);
- | Return _ | Goto _ | Break _ | Continue _ -> ())
+ | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ -> ())
ss
let rec peepHole2 (* Process two instructions and possibly replace them both *)
@@ -5844,7 +5877,7 @@ let rec peepHole2 (* Process two instructions and possibly replace them both *)
peepHole2 dotwo h.bstmts;
s.skind <- TryExcept (b, (doInstrList il, e), h, l)
- | Return _ | Goto _ | Break _ | Continue _ -> ())
+ | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ -> ())
ss
@@ -6019,6 +6052,7 @@ let rec isConstant = function
-> vi.vglob && isConstantOffset off
| AddrOf (Mem e, off) | StartOf(Mem e, off)
-> isConstant e && isConstantOffset off
+ | AddrOfLabel _ -> true
and isConstantOffset = function
NoOffset -> true
@@ -6444,21 +6478,22 @@ let trylink source dest_option = match dest_option with
(** Cmopute the successors and predecessors of a block, given a fallthrough *)
-let rec succpred_block b fallthrough =
+let rec succpred_block b fallthrough rlabels =
let rec handle sl = match sl with
[] -> ()
- | [a] -> succpred_stmt a fallthrough
+ | [a] -> succpred_stmt a fallthrough rlabels
| hd :: ((next :: _) as tl) ->
- succpred_stmt hd (Some next) ;
+ succpred_stmt hd (Some next) rlabels;
handle tl
in handle b.bstmts
-and succpred_stmt s fallthrough =
+and succpred_stmt s fallthrough rlabels =
match s.skind with
Instr _ -> trylink s fallthrough
| Return _ -> ()
| Goto(dest,l) -> link s !dest
+ | ComputedGoto(e,l) -> List.iter (link s) rlabels
| Break _
| Continue _
| Switch _ ->
@@ -6467,23 +6502,23 @@ and succpred_stmt s fallthrough =
| If(e1,b1,b2,l) ->
(match b1.bstmts with
[] -> trylink s fallthrough
- | hd :: tl -> (link s hd ; succpred_block b1 fallthrough )) ;
+ | hd :: tl -> (link s hd ; succpred_block b1 fallthrough rlabels )) ;
(match b2.bstmts with
[] -> trylink s fallthrough
- | hd :: tl -> (link s hd ; succpred_block b2 fallthrough ))
+ | hd :: tl -> (link s hd ; succpred_block b2 fallthrough rlabels ))
| Loop(b,l,_,_) ->
begin match b.bstmts with
[] -> failwith "computeCFGInfo: empty loop"
| hd :: tl ->
link s hd ;
- succpred_block b (Some(hd))
+ succpred_block b (Some(hd)) rlabels
end
| Block(b) -> begin match b.bstmts with
[] -> trylink s fallthrough
| hd :: tl -> link s hd ;
- succpred_block b fallthrough
+ succpred_block b fallthrough rlabels
end
| TryExcept _ | TryFinally _ ->
failwith "computeCFGInfo: structured exception handling not implemented"
@@ -6528,7 +6563,7 @@ let rec xform_switch_stmt s break_dest cont_dest = begin
| Default(l) -> Label(freshLabel "switch_default",l,false)
) s.labels ;
match s.skind with
- | Instr _ | Return _ | Goto _ -> ()
+ | Instr _ | Return _ | Goto _ | ComputedGoto _ -> ()
| Break(l) -> begin try
s.skind <- Goto(break_dest (),l)
with e ->
@@ -6678,6 +6713,25 @@ class registerLabelsVisitor : cilVisitor = object
method vinst _ = SkipChildren
end
+(* Find all labels-as-value in a function to use them as successors of computed
+ * gotos. Duplicated in src/ext/cfg.ml. *)
+class addrOfLabelFinder slr = object(self)
+ inherit nopCilVisitor
+
+ method vexpr e = match e with
+ | AddrOfLabel sref ->
+ slr := !sref :: (!slr);
+ SkipChildren
+ | _ -> DoChildren
+
+end
+
+let findAddrOfLabelStmts (b : block) : stmt list =
+ let slr = ref [] in
+ let vis = new addrOfLabelFinder slr in
+ ignore(visitCilBlock vis b);
+ !slr
+
(* prepare a function for computeCFGInfo by removing break, continue,
* default and switch statements/labels and replacing them with Ifs and
* Gotos. *)
@@ -6698,7 +6752,8 @@ let computeCFGInfo (f : fundec) (global_numbering : bool) : unit =
let clear_it = new clear in
ignore (visitCilBlock clear_it f.sbody) ;
f.smaxstmtid <- Some (!sid_counter) ;
- succpred_block f.sbody (None);
+ let rlabels = findAddrOfLabelStmts f.sbody in
+ succpred_block f.sbody None rlabels;
let res = List.rev !statements in
statements := [];
f.sallstmts <- res;
View
8 src/cil.mli
@@ -613,6 +613,8 @@ and exp =
* {!Cil.mkAddrOrStartOf} to make one of these if you are not sure which
* one to use. *)
+ | AddrOfLabel of stmt ref
+
| StartOf of lval
(** Conversion from an array to a pointer to the beginning of the array.
* Given an lval of type [TArray(T)] produces an expression of type
@@ -949,6 +951,8 @@ and stmtkind =
* you have to update the reference whenever you replace the target
* statement. The target statement MUST have at least a label. *)
+ | ComputedGoto of exp * location
+
| Break of location
(** A break to the end of the nearest enclosing Loop or Switch *)
@@ -2015,6 +2019,10 @@ val makeStaticGlobal: bool ref
* their operands *)
val useLogicalOperators: bool ref
+(** Whether to use GCC's computed gotos. By default, do not use them and
+ * replace them by a switch. *)
+val useComputedGoto: bool ref
+
(** Set this to true to get old-style handling of gcc's extern inline C extension:
old-style: the extern inline definition is used until the actual definition is
seen (as long as optimization is enabled)
View
10 src/ciloptions.ml
@@ -313,6 +313,16 @@ let options : (string * Arg.spec * string) list =
("Transform &&, || and ?: to If statements" ^
is_default (not !Cil.useLogicalOperators));
+ "--useComputedGoto",
+ Arg.Set Cil.useComputedGoto,
+ (" Retain GCC's computed goto" ^
+ is_default !Cil.useComputedGoto);
+
+ "--noUseComputedGoto",
+ Arg.Clear Cil.useComputedGoto,
+ (" Transform computed goto to Switch statements" ^
+ is_default (not !Cil.useComputedGoto));
+
"--keepunused",
Arg.Set Rmtmps.keepUnused,
(" Do not remove the unused variables and types" ^
View
51 src/ext/cfg.ml
@@ -68,6 +68,8 @@ module E=Errormsg
cont = succ of any Continue in this block
None means the succ is the function return. It does not mean the break/cont
is invalid. We assume the validity has already been checked.
+ rlabels = list of potential successors of computed gotos (ie. every labelled
+ statement whose address is retained)
*)
let start_id = ref 0 (* for unique ids across many functions *)
@@ -95,6 +97,23 @@ let findCaseLabeledStmts (b : block) : stmt list =
ignore(visitCilBlock vis b);
!slr
+class addrOfLabelFinder slr = object(self)
+ inherit nopCilVisitor
+
+ method vexpr e = match e with
+ | AddrOfLabel sref ->
+ slr := !sref :: (!slr);
+ SkipChildren
+ | _ -> DoChildren
+
+end
+
+let findAddrOfLabelStmts (b : block) : stmt list =
+ let slr = ref [] in
+ let vis = new addrOfLabelFinder slr in
+ ignore(visitCilBlock vis b);
+ !slr
+
(* entry point *)
(** Compute a control flow graph for fd. Stmts in fd have preds and succs
@@ -103,8 +122,9 @@ let rec cfgFun (fd : fundec): int =
begin
let initial_id = !start_id in
let nodeList = ref [] in
+ let rlabels = findAddrOfLabelStmts fd.sbody in
- cfgBlock fd.sbody None None None nodeList;
+ cfgBlock fd.sbody None None None nodeList rlabels;
fd.smaxstmtid <- Some(!start_id);
fd.sallstmts <- List.rev !nodeList;
@@ -115,25 +135,25 @@ let rec cfgFun (fd : fundec): int =
and cfgStmts (ss: stmt list)
(next:stmt option) (break:stmt option) (cont:stmt option)
- (nodeList:stmt list ref) =
+ (nodeList:stmt list ref) (rlabels: stmt list) =
match ss with
[] -> ();
- | [s] -> cfgStmt s next break cont nodeList
+ | [s] -> cfgStmt s next break cont nodeList rlabels
| hd::tl ->
- cfgStmt hd (Some (List.hd tl)) break cont nodeList;
- cfgStmts tl next break cont nodeList
+ cfgStmt hd (Some (List.hd tl)) break cont nodeList rlabels;
+ cfgStmts tl next break cont nodeList rlabels
and cfgBlock (blk: block)
(next:stmt option) (break:stmt option) (cont:stmt option)
- (nodeList:stmt list ref) =
- cfgStmts blk.bstmts next break cont nodeList
+ (nodeList:stmt list ref) (rlabels: stmt list) =
+ cfgStmts blk.bstmts next break cont nodeList rlabels
(* Fill in the CFG info for a stmt
Meaning of next, break, cont should be clear from earlier comment
*)
and cfgStmt (s: stmt) (next:stmt option) (break:stmt option) (cont:stmt option)
- (nodeList:stmt list ref) =
+ (nodeList:stmt list ref) (rlabels: stmt list) =
incr start_id;
s.sid <- !start_id;
nodeList := s :: !nodeList; (* Future traversals can be made in linear time. e.g. *)
@@ -175,17 +195,18 @@ and cfgStmt (s: stmt) (next:stmt option) (break:stmt option) (cont:stmt option)
()
| Return _ -> ()
| Goto (p,_) -> addSucc !p
+ | ComputedGoto (e,_) -> List.iter addSucc rlabels
| Break _ -> addOptionSucc break
| Continue _ -> addOptionSucc cont
| If (_, blk1, blk2, _) ->
(* The succs of If is [true branch;false branch] *)
addBlockSucc blk2 next;
addBlockSucc blk1 next;
- cfgBlock blk1 next break cont nodeList;
- cfgBlock blk2 next break cont nodeList
+ cfgBlock blk1 next break cont nodeList rlabels;
+ cfgBlock blk2 next break cont nodeList rlabels
| Block b ->
addBlockSucc b next;
- cfgBlock b next break cont nodeList
+ cfgBlock b next break cont nodeList rlabels
| Switch(_,blk,l,_) ->
let bl = findCaseLabeledStmts blk in
List.iter addSucc (List.rev bl(*l*)); (* Add successors in order *)
@@ -197,11 +218,11 @@ and cfgStmt (s: stmt) (next:stmt option) (break:stmt option) (cont:stmt option)
bl)
then
addOptionSucc next;
- cfgBlock blk next next cont nodeList
+ cfgBlock blk next next cont nodeList rlabels
| Loop(blk, loc, s1, s2) ->
s.skind <- Loop(blk, loc, (Some s), next);
addBlockSucc blk (Some s);
- cfgBlock blk (Some s) next (Some s) nodeList
+ 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 *)
| TryExcept _ | TryFinally _ ->
@@ -228,7 +249,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 _ | Instr _) -> ()
+ | (Return _ | Break _ | Continue _ | Goto _ | ComputedGoto _ | Instr _) -> ()
| TryExcept _ | TryFinally _ -> E.s (E.unimp "try/except/finally")
end
;;
@@ -247,7 +268,7 @@ let d_cfgnodelabel () (s : stmt) =
| Loop _ -> "loop"
| Break _ -> "break"
| Continue _ -> "continue"
- | Goto _ -> "goto"
+ | Goto _ | ComputedGoto _ -> "goto"
| Instr _ -> "instr"
| Switch _ -> "switch"
| Block _ -> "block"
View
2  src/ext/dataflow.ml
@@ -220,7 +220,7 @@ module ForwardsDataFlow =
(* Handle instructions starting with the first one *)
List.fold_left handleInstruction curr il
- | Goto _ | Break _ | Continue _ | If _
+ | Goto _ | ComputedGoto _ | Break _ | Continue _ | If _
| TryExcept _ | TryFinally _
| Switch _ | Loop _ | Return _ | Block _ -> curr
in
View
2  src/ext/oneret.ml
@@ -148,7 +148,7 @@ let oneret (f: Cil.fundec) : unit =
| ({skind=Block b} as s) :: rests ->
s.skind <- Block (scanBlock false b);
s :: scanStmts mainbody rests
- | ({skind=(Goto _ | Instr _ | Continue _ | Break _
+ | ({skind=(Goto _ | ComputedGoto _ | Instr _ | Continue _ | Break _
| TryExcept _ | TryFinally _)} as s)
:: rests -> s :: scanStmts mainbody rests
View
10 src/ext/partial.ml
@@ -686,7 +686,7 @@ struct
let y = stmt_fun a x in
match x.skind with
Instr _
- | Return _ | Goto _ | Break _ | Continue _ -> y
+ | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ -> y
| If (_expr, then_block, else_block, _loc) ->
visit_block
stmt_fun
@@ -709,6 +709,10 @@ struct
and gather_gotos acc stmt =
match stmt.skind with
Goto (stmt_ref, _loc) -> gather_labels acc !stmt_ref
+ | ComputedGoto _ ->
+ (* Assume that CFG fills successors correctly *)
+ List.fold_left (fun a s -> gather_labels a s)
+ acc stmt.succs
| _ -> acc
and transitive_closure ini_stmt =
let rec iter trace acc stmt =
@@ -727,6 +731,10 @@ struct
(fun a x ->
match x.skind with
Goto (stmt_ref, _loc) -> gather_labels a !stmt_ref
+ | ComputedGoto _ ->
+ (* Assume that CFG fills successors correctly *)
+ List.fold_left (fun a s -> gather_labels a s)
+ a x.succs
| Block block -> visit_block gather_gotos a block
| _ -> a)
LabelSet.empty
View
2  src/ext/predabst.ml
@@ -221,6 +221,8 @@ module Solver = functor(T:TRANSLATOR) ->
(* Cast should check if signed type, and if so, make an ite term *)
| AddrOf lv -> T.mkVar (sprint 80 (d_exp () e))
| StartOf lv -> T.mkVar (sprint 80 (d_exp () e))
+ | AddrOfLabel _ ->
+ raise (E.s "Address of label not supported in Predabst\n") (* XXX *)
let isValid e1 e2 =
let e_imp = T.mkImp e1 e2 in
View
2  src/ext/pta/ptranal.ml
@@ -250,6 +250,7 @@ and analyze_expr (e : exp ) : A.tau =
if !fun_ptrs_as_funs && isFunctionType (typeOfLval l) then
A.rvalue (analyze_lval l)
else A.address (analyze_lval l)
+ | AddrOfLabel _ -> failwith "not implemented yet" (* XXX *)
| StartOf l -> A.address (analyze_lval l)
| AlignOfE _ -> A.bottom ()
| SizeOfE _ -> A.bottom ()
@@ -314,6 +315,7 @@ let rec analyze_stmt (s : stmt ) : unit =
| None -> ()
end
| Goto (s', l) -> () (* analyze_stmt(!s') *)
+ | ComputedGoto (e, l) -> ()
| If (e, b, b', l) ->
(* ignore the expression e; expressions can't be side-effecting *)
analyze_block b;
View
1  src/ext/simplify.ml
@@ -124,6 +124,7 @@ let rec makeThreeAddress
constFold true e
| Const _ -> e
| AddrOf (Var _, NoOffset) -> e
+ | AddrOfLabel (_) -> e
| Lval lv -> Lval (simplifyLval setTemp lv)
| BinOp(bo, e1, e2, tres) ->
BinOp(bo, makeBasic setTemp e1, makeBasic setTemp e2, tres)
View
4 src/ext/usedef.ml
@@ -196,6 +196,7 @@ let computeUseDefStmtKind ?(acc_used=VS.empty)
| Return (Some e, _) -> ve e
| If (e, _, _, _) -> ve e
| Break _ | Goto _ | Continue _ -> ()
+ | ComputedGoto (e, _) -> ve e
| Loop (_, _, _, _) -> ()
| Switch (e, _, _, _) -> ve e
| Instr il ->
@@ -231,6 +232,9 @@ let rec computeDeepUseDefStmtKind ?(acc_used=VS.empty)
let u'', d'' = handle_block fb in
(VS.union (VS.union u u') u'', VS.union (VS.union d d') d'')
| Break _ | Goto _ | Continue _ -> !varUsed, !varDefs
+ | ComputedGoto (e, _) ->
+ let _ = ve e in
+ !varUsed, !varDefs
| Loop (b, _, _, _) -> handle_block b
| Switch (e, b, _, _) ->
let _ = ve e in
View
19 src/frontc/cabs2cil.ml
@@ -4592,7 +4592,13 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
| Some (e, t) -> finishExp se e t
end
- | A.LABELADDR l -> begin (* GCC's taking the address of a label *)
+ | A.LABELADDR l when !Cil.useComputedGoto -> begin (* GCC's taking the address of a label *)
+ let ln = lookupLabel l in
+ let gref = ref dummyStmt in
+ addGoto ln gref;
+ finishExp empty (AddrOfLabel gref) voidPtrType
+ end
+ | A.LABELADDR l -> begin
let l = lookupLabel l in (* To support locallly declared labels *)
let addrval =
try H.find gotoTargetHash l
@@ -6012,7 +6018,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function
List.fold_left (fun acc elt ->
acc && instrFallsThrough elt) true il
| Return _ | Break _ | Continue _ -> false
- | Goto _ -> false
+ | Goto _ | ComputedGoto _ -> false
| If (_, b1, b2, _) ->
blockFallsThrough b1 || blockFallsThrough b2
| Switch (e, b, targets, _) ->
@@ -6074,7 +6080,7 @@ and doDecl (isglobal: 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 _ -> false
+ Instr _ | Return _ | Continue _ | Goto _ | ComputedGoto _ -> false
| Break _ -> true
| If (_, b1, b2, _) ->
blockCanBreak b1 || blockCanBreak b2
@@ -6484,6 +6490,13 @@ and doStatement (s : A.statement) : chunk =
(* Maybe we need to rename this label *)
gotoChunk (lookupLabel l) loc'
+ | A.COMPGOTO (e, loc) when !Cil.useComputedGoto -> begin
+ let loc' = convLoc loc in
+ currentLoc := loc';
+ (* Do the expression *)
+ let se, e', t' = doExp false e (AExp (Some voidPtrType)) in
+ se @@ s2c(mkStmt(ComputedGoto (e', loc')))
+ end
| A.COMPGOTO (e, loc) -> begin
let loc' = convLoc loc in
currentLoc := loc';
View
1  src/mergecil.ml
@@ -1146,6 +1146,7 @@ begin
| Instr(l) -> 13 + 67*(List.length l)
| Return(_) -> 17
| Goto(_) -> 19
+ | ComputedGoto(_) -> 131
| Break(_) -> 23
| Continue(_) -> 29
| If(_,b1,b2,_) -> 31 + 37*(stmtListSum b1.bstmts)
View
17 src/rmtmps.ml
@@ -667,10 +667,15 @@ class markUsedLabels (labelMap: (string, unit) H.t) = object
| _ -> DoChildren
- (* No need to go into expressions or instructions *)
- method vexpr _ = SkipChildren
- method vinst _ = SkipChildren
- method vtype _ = SkipChildren
+ method vexpr e = match e with
+ | AddrOfLabel dest ->
+ let (ln, _, _), _ = labelsToKeep !dest.labels in
+ if ln = "" then
+ E.s (E.bug "rmtmps: destination of address of label does not have labels");
+ (* Mark it as used *)
+ H.replace labelMap ln ();
+ SkipChildren
+ | _ -> DoChildren
end
class removeUnusedLabels (labelMap: (string, unit) H.t) = object
@@ -769,7 +774,9 @@ let removeUnmarked file =
* marking the used labels *)
let usedLabels:(string, unit) H.t = H.create 13 in
ignore (visitCilFunction (new removeUnusedGoto) func);
- ignore (visitCilBlock (new markUsedLabels usedLabels) func.sbody);
+ (* scan the function, not only the body, since there might be
+ * AddrOfLabel in initializers *)
+ ignore (visitCilFunction (new markUsedLabels usedLabels) func);
(* And now we scan again and we remove them *)
ignore (visitCilBlock (new removeUnusedLabels usedLabels) func.sbody);
true
View
7 test/Makefile
@@ -144,6 +144,13 @@ endif
ifdef CABSONLY
CILLY+= --cabsonly
endif
+ifdef COMPUTEDGOTO
+ CILLY+= --useComputedGoto
+endif
+ifdef LOCALINIT
+ CILLY+= --noMakeStaticGlobal
+endif
+
# This is a way to enable the stats, allowing the command line to override it
View
29 test/small1/label2b.c
@@ -0,0 +1,29 @@
+// Example with computed labels
+#include "testharness.h"
+
+int main() {
+
+ void *nextstate = && Loop;
+ int x = 0;
+ int acc = 0;
+ int count = 5;
+
+ Loop:
+ if(x == 10) nextstate = && Done;
+ acc += x; x ++;
+ goto *nextstate;
+ Done:
+
+ if(acc != 11 * 10 / 2) {
+ printf("Bad result: %d\n", acc);
+ return 1;
+ }
+
+ if(count <= 0) return 0;
+
+ acc = 0; x = 0;
+ nextstate = && Loop;
+ count --;
+
+ goto *nextstate;
+}
View
13 test/small1/label3b.c
@@ -0,0 +1,13 @@
+
+
+
+int main() {
+ static void* array[] = { && L1, && L2, && L3 };
+ int acc = 0;
+
+ L1: acc += 1; goto * array[1];
+ L2: acc += 2; goto * array[2];
+ L3: acc += 3;
+
+ return acc - 6;
+}
View
41 test/small1/label4b.c
@@ -0,0 +1,41 @@
+#include "testharness.h"
+extern void abort(void);
+// From c-torture
+
+int expect_do1 = 1, expect_do2 = 2;
+
+static int doit(int x){
+ __label__ lbl1;
+ __label__ lbl2;
+ static int jtab_init = 0;
+ static void *jtab[2];
+
+ if(!jtab_init) {
+ jtab[0] = &&lbl1;
+ jtab[1] = &&lbl2;
+ jtab_init = 1;
+ }
+ goto *jtab[x];
+lbl1:
+ return 1;
+lbl2:
+ return 2;
+}
+
+static void do1(void) {
+ if (doit(0) != expect_do1)
+ abort ();
+}
+
+static void do2(void){
+ if (doit(1) != expect_do2)
+ abort ();
+}
+
+int main(void){
+#ifndef NO_LABEL_VALUES
+ do1();
+ do2();
+#endif
+ exit(0);
+}
View
3  test/testcil.pl
@@ -399,6 +399,9 @@ sub addToGroup {
addTest("testrun/label2");
addTest("testrun/label3");
addTest("testrun/label4 _GNUCC=1");
+addTest("testrun/label2b COMPUTEDGOTO=1");
+addTest("testrun/label3b COMPUTEDGOTO=1 LOCALINIT=1");
+addTest("testrun/label4b COMPUTEDGOTO=1 _GNUCC=1");
addTest("test/label5");
addTest("testrun/label6");
addTest("test/label7");
Please sign in to comment.
Something went wrong with that request. Please try again.