Browse files

Add ComputedGoto and AddrOfLabel constructors

  • Loading branch information...
1 parent 3ea3a53 commit 103d8c76e3536932c91bc8316606e33d22d873ad @kerneis kerneis committed Aug 1, 2012
Showing with 62 additions and 8 deletions.
  1. +1 −1 ocamlutil/Makefile.ocaml
  2. +18 −2 src/check.ml
  3. +36 −3 src/cil.ml
  4. +4 −0 src/cil.mli
  5. +2 −2 src/frontc/cabs2cil.ml
  6. +1 −0 src/mergecil.ml
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
39 src/cil.ml
@@ -497,6 +497,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
@@ -728,6 +729,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
@@ -1103,6 +1107,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
@@ -1783,6 +1788,7 @@ let getParenthLevel (e: exp) =
(* Unary *)
| CastE(_,_) -> 30
| AddrOf(_) -> 30
+ | AddrOfLabel(_) -> 30
| StartOf(_) -> 30
| UnOp((Neg|BNot|LNot),_,_) -> 30
@@ -1883,6 +1889,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)
@@ -3320,6 +3327,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
@@ -3764,6 +3784,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;"
@@ -4623,6 +4649,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
@@ -5116,6 +5143,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
@@ -5254,6 +5282,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
@@ -5799,7 +5830,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 *)
@@ -5833,7 +5864,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
@@ -6008,6 +6039,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
@@ -6448,6 +6480,7 @@ and succpred_stmt s fallthrough =
Instr _ -> trylink s fallthrough
| Return _ -> ()
| Goto(dest,l) -> link s !dest
+ | ComputedGoto(e,l) -> failwith "not implemented yet" (* XXX *)
| Break _
| Continue _
| Switch _ ->
@@ -6517,7 +6550,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 ->
View
4 src/cil.mli
@@ -606,6 +606,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
@@ -942,6 +944,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 *)
View
4 src/frontc/cabs2cil.ml
@@ -6002,7 +6002,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, _) ->
@@ -6064,7 +6064,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
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)

0 comments on commit 103d8c7

Please sign in to comment.