Skip to content

Commit

Permalink
Add Real (and Imag) to CIL
Browse files Browse the repository at this point in the history
and make connection with cabs
References #8, References #9
  • Loading branch information
michael-schwarz committed Jan 14, 2020
1 parent caac4f3 commit e1471d0
Show file tree
Hide file tree
Showing 10 changed files with 83 additions and 8 deletions.
11 changes: 10 additions & 1 deletion src/check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -173,6 +173,7 @@ type ctxType =
* in a cast *)
| CTSizeof (* In a sizeof *)
| CTDecl (* In a typedef, or a declaration *)
| CTNumeric (* As an argument to __real__ or __imag__ *)

let d_context () = function
CTStruct -> text "CTStruct"
Expand All @@ -184,6 +185,7 @@ let d_context () = function
| CTExp -> text "CTExp"
| CTSizeof -> text "CTSizeof"
| CTDecl -> text "CTDecl"
| CTNumeric -> text "CTNumeric"


(* Keep track of all tags that we use. For each tag remember also the info
Expand Down Expand Up @@ -225,7 +227,9 @@ let rec checkType (t: typ) (ctx: ctxType) =
(ignore(warn "sizeof(function) is not defined in MSVC."); false)
else
ctx = CTPtr || ctx = CTDecl || ctx = CTSizeof
| _ -> true
| TInt _ -> true
| TFloat _ -> true
| _ -> ctx <> CTNumeric
in
if not (checkContext t) then
ignore (warn "Type (%a) used in wrong context. Expected context: %a"
Expand Down Expand Up @@ -491,6 +495,11 @@ and checkExp (isconst: bool) (e: exp) : typ =

| SizeOfStr s -> typeOf e

| Real e ->
let te = checkExp isconst e in
typeOfReal te
| Imag e -> E.s (E.bug "unimplemented")

| AlignOf(t) -> begin
(* Sizeof cannot be applied to certain types *)
checkType t CTSizeof;
Expand Down
42 changes: 37 additions & 5 deletions src/cil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -492,7 +492,8 @@ and exp =
* not turned into a constant because
* some transformations might want to
* change types *)

| Real of exp (** __real__(<expression>) *)
| Imag of exp (** __imag__(<expression>) *)
| SizeOfE of exp (** sizeof(<expression>) *)
| SizeOfStr of string
(** sizeof(string_literal). We separate this case out because this is the
Expand Down Expand Up @@ -1596,6 +1597,21 @@ let isVoidPtrType t =
TPtr(tau,_) when isVoidType tau -> true
| _ -> false

(* get the typ of __real__(e) for e of typ t*)
let typeOfReal t =
match unrollType t with
| TInt _ -> t
| TFloat (fkind, attrs) ->
let newfkind = function
| FFloat -> FFloat (** [float] *)
| FDouble -> FDouble (** [double] *)
| FLongDouble -> FLongDouble (** [long double] *)
| FComplexFloat -> FFloat
| FComplexDouble -> FDouble
| FComplexLongDouble -> FLongDouble
in TFloat (newfkind fkind, attrs)
| _ -> E.s (E.bug "unexpected non-numerical type for argument to __real__")

let var vi : lval = (Var vi, NoOffset)
(* let assign vi e = Instrs(Set (var vi, e), lu) *)

Expand Down Expand Up @@ -1798,6 +1814,8 @@ let getParenthLevel (e: exp) =
| BinOp((Div|Mod|Mult),_,_,_) -> 40

(* Unary *)
| Real _ -> 30
| Imag _ -> 30
| CastE(_,_) -> 30
| AddrOf(_) -> 30
| AddrOfLabel(_) -> 30
Expand Down Expand Up @@ -1892,7 +1910,8 @@ let rec typeOf (e: exp) : typ =
| Const(CReal (_, fk, _)) -> TFloat(fk, [])

| Const(CEnum(tag, _, ei)) -> typeOf tag

| Real e -> typeOfReal @@ typeOf e
| Imag e -> E.s (E.bug "unsupported")
| Lval(lv) -> typeOfLval lv
| SizeOf _ | SizeOfE _ | SizeOfStr _ -> !typeOfSizeOf
| AlignOf _ | AlignOfE _ -> !typeOfSizeOf
Expand Down Expand Up @@ -2755,6 +2774,8 @@ let rec isConstant = function
| Lval (Var vi, NoOffset) ->
(vi.vglob && isArrayType vi.vtype || isFunctionType vi.vtype)
| Lval _ -> false
| Real e -> isConstant e
| Imag e -> isConstant e
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ -> true
| CastE (_, e) -> isConstant e
| AddrOf (Var vi, off) | StartOf (Var vi, off)
Expand Down Expand Up @@ -3432,7 +3453,10 @@ class defaultCilPrinterClass : cilPrinter = object (self)
text "__builtin_va_arg_pack()"
| SizeOfE (e) ->
text "sizeof(" ++ self#pExp () e ++ chr ')'

| Imag e ->
text "__imag__(" ++ self#pExp () e ++ chr ')'
| Real e ->
text "__real__(" ++ self#pExp () e ++ chr ')'
| SizeOfStr s ->
text "sizeof(" ++ d_const () (CStr s) ++ chr ')'

Expand Down Expand Up @@ -4800,7 +4824,10 @@ class plainCilPrinterClass =
text "__alignof__(" ++ self#pType None () t ++ chr ')'
| AlignOfE (e) ->
text "__alignof__(" ++ self#pExp () e ++ chr ')'

| Imag e ->
text "__imag__(" ++ self#pExp () e ++ chr ')'
| Real e ->
text "__real__(" ++ self#pExp () e ++ chr ')'
| StartOf lv -> dprintf "StartOf(%a)" self#pLval lv
| AddrOf (lv) -> dprintf "AddrOf(%a)" self#pLval lv
| AddrOfLabel (sref) -> dprintf "AddrOfLabel(%a)" self#pStmt !sref
Expand Down Expand Up @@ -5283,7 +5310,12 @@ and childrenExp (vis: cilVisitor) (e: exp) : exp =
let e1' = vExp e1 in
if e1' != e1 then SizeOfE e1' else e
| SizeOfStr s -> e

| Real e1 ->
let e1' = vExp e1 in
if e1' != e1 then Real e1' else e
| Imag e1 ->
let e1' = vExp e1 in
if e1' != e1 then Imag e1' else e
| AlignOf t ->
let t' = vTyp t in
if t' != t then AlignOf t' else e
Expand Down
6 changes: 5 additions & 1 deletion src/cil.mli
Original file line number Diff line number Diff line change
Expand Up @@ -586,7 +586,8 @@ and exp =
(** sizeof(<type>). Has [unsigned int] type (ISO 6.5.3.4). This is not
* turned into a constant because some transformations might want to
* change types *)

| Real of exp (** __real__(<expression>) *)
| Imag of exp (** __imag__(<expression>) *)
| SizeOfE of exp
(** sizeof(<expression>) *)

Expand Down Expand Up @@ -1323,6 +1324,9 @@ val isVoidType: typ -> bool
(** is the given type "void *"? *)
val isVoidPtrType: typ -> bool

(** for numerical __complex types return type of corresponding real part *)
val typeOfReal: typ -> typ

(** int *)
val intType: typ

Expand Down
2 changes: 2 additions & 0 deletions src/ext/ccl/ccl.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1078,6 +1078,8 @@ let rec evaluateExp (e : exp) (state : state) : summary =
| StartOf lv -> evaluateLval lv state
| Question _ -> E.s (E.unimp "ternary operator ?:")
| AddrOfLabel _ -> E.s (E.unimp "address of label")
| Real _ -> E.s (E.unimp "real")
| Imag _ -> E.s (E.unimp "imag")

and evaluateLval (lv : lval) (state : state) : summary =
match lv with
Expand Down
2 changes: 2 additions & 0 deletions src/ext/llvm/llvmgen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1000,6 +1000,8 @@ class llvmGeneratorClass : llvmGenerator = object (self)
| CastE (t, e) -> iCast t e
| AddrOf lv -> iAddrOf lv
| StartOf lv -> iStartOf lv
| Imag e -> raise (Unimplemented "Imag")
| Real e -> raise (Unimplemented "Real")
| AddrOfLabel _ -> raise (Unimplemented "AddrOfLabel")
| Question _ -> raise (Unimplemented "Question")

Expand Down
2 changes: 2 additions & 0 deletions src/ext/pta/ptranal.ml
Original file line number Diff line number Diff line change
Expand Up @@ -255,6 +255,8 @@ and analyze_expr (e : exp ) : A.tau =
| StartOf l -> A.address (analyze_lval l)
| AlignOfE _ -> A.bottom ()
| SizeOfE _ -> A.bottom ()
| Imag __ -> failwith "not implemented yet"
| Real __ -> failwith "not implemented yet"
in
H.add expressions e result;
result
Expand Down
4 changes: 4 additions & 0 deletions src/ext/simplify/simplify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -131,6 +131,10 @@ let rec makeThreeAddress
BinOp(bo, makeBasic setTemp e1, makeBasic setTemp e2, tres)
| Question _ ->
E.s (bug "Simplify: There should not be a \"?:\" operator here.")
| Real e1 ->
Real (makeBasic setTemp e1)
| Imag e1 ->
Imag (makeBasic setTemp e1)
| UnOp(uo, e1, tres) ->
UnOp(uo, makeBasic setTemp e1, tres)
| CastE(t, e) ->
Expand Down
6 changes: 5 additions & 1 deletion src/frontc/cabs2cil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3641,7 +3641,11 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
| _ -> SizeOfE e'
in
finishExp empty size !typeOfSizeOf

| A.REAL e ->
let (se, e', t) = doExp false e (AExp None) in
let real = Real e' in
finishExp se real (typeOfReal t)
| A.IMAG e -> E.s (bug "cabs2cil: unsupported")
| A.TYPE_ALIGNOF (bt, dt) ->
let typ = doOnlyType bt dt in
finishExp empty (AlignOf(typ)) !typeOfSizeOf
Expand Down
6 changes: 6 additions & 0 deletions src/frontc/cabsvisit.ml
Original file line number Diff line number Diff line change
Expand Up @@ -506,6 +506,12 @@ and childrenExpression vis e =
| EXPR_SIZEOF (e1) ->
let e1' = ve e1 in
if e1' != e1 then EXPR_SIZEOF (e1') else e
| REAL e1 ->
let e1' = ve e1 in
if e1' != e1 then REAL (e1') else e
| IMAG e1 ->
let e1' = ve e1 in
if e1' != e1 then IMAG (e1') else e
| TYPE_SIZEOF (s, dt) ->
let s' = visitCabsSpecifier vis s in
let dt' = visitCabsDeclType vis false dt in
Expand Down
10 changes: 10 additions & 0 deletions src/frontc/cprint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -403,6 +403,8 @@ and get_operator exp =
| TYPE_SIZEOF _ -> ("", 16)
| EXPR_ALIGNOF exp -> ("", 16)
| TYPE_ALIGNOF _ -> ("", 16)
| IMAG exp -> ("", 16)
| REAL exp -> ("", 16)
| INDEX (exp, idx) -> ("", 15)
| MEMBEROF (exp, fld) -> ("", 15)
| MEMBEROFPTR (exp, fld) -> ("", 15)
Expand Down Expand Up @@ -530,6 +532,14 @@ and print_expression_level (lvl: int) (exp : expression) =
printl ["__alignof__";"("];
print_onlytype (bt, dt);
print ")"
| IMAG exp ->
printl ["__imag__";"("];
print_expression_level 0 exp;
print ")"
| REAL exp ->
printl ["__real__";"("];
print_expression_level 0 exp;
print ")"
| INDEX (exp, idx) ->
print_expression_level 16 exp;
print "[";
Expand Down

0 comments on commit e1471d0

Please sign in to comment.