diff options
Diffstat (limited to 'cparser')
-rw-r--r-- | cparser/Bitfields.ml | 388 | ||||
-rw-r--r-- | cparser/Cutil.ml | 23 | ||||
-rw-r--r-- | cparser/Cutil.mli | 4 | ||||
-rw-r--r-- | cparser/Elab.ml | 31 | ||||
-rw-r--r-- | cparser/PackedStructs.ml | 2 | ||||
-rw-r--r-- | cparser/Parse.ml | 2 | ||||
-rw-r--r-- | cparser/StructReturn.ml | 6 | ||||
-rw-r--r-- | cparser/Transform.ml | 33 | ||||
-rw-r--r-- | cparser/Transform.mli | 6 | ||||
-rw-r--r-- | cparser/Unblock.ml | 8 |
10 files changed, 304 insertions, 199 deletions
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 99b93c25..570572fa 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -15,8 +15,7 @@ (* Elimination of bit fields in structs *) -(* Assumes: unblocked code. - Preserves: unblocked code. *) +(* Assumes: nothing. *) open Printf open Machine @@ -46,6 +45,10 @@ type bitfield_info = let bitfield_table = (Hashtbl.create 57: (ident * string, bitfield_info) Hashtbl.t) +let is_bitfield structid fieldname = + try Some (Hashtbl.find bitfield_table (structid, fieldname)) + with Not_found -> None + (* Signedness issues *) let unsigned_ikind_for_carrier nbits = @@ -218,6 +221,78 @@ let bitfield_assign env bf carrier newval = and oldval_masked = ebinint env Oand carrier notmsk in ebinint env Oor oldval_masked newval_masked +(* Initialize a bitfield *) + +(* Reference C code: + +unsigned int bitfield_init(int ofs, int sz, unsigned int y) +{ + unsigned int mask = (1U << sz) - 1; + return (y & mask) << ofs; +} +*) + +let bitfield_initializer bf i = + match i with + | Init_single e -> + let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in + let e_mask = + {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); + etyp = TInt(IUInt, [])} in + let e_and = + {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[])); + etyp = TInt(IUInt,[])} in + {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt, + TInt(IUInt, [])); + etyp = TInt(IUInt, [])} + | _ -> + assert false + +(* Associate to the left so that it prints more nicely *) + +let or_expr_list = function + | [] -> intconst 0L IUInt + | [e] -> e + | e1 :: el -> + List.fold_left + (fun accu e -> + {edesc = EBinop(Oor, accu, e, TInt(IUInt,[])); + etyp = TInt(IUInt,[])}) + e1 el + +(* Initialize the carrier for consecutive bitfields *) + +let rec pack_bitfield_init id carrier fld_init_list = + match fld_init_list with + | [] -> ([], []) + | (fld, i) :: rem -> + match is_bitfield id fld.fld_name with + | None -> + ([], fld_init_list) + | Some bf -> + if bf.bf_carrier <> carrier then + ([], fld_init_list) + else begin + let (el, rem') = pack_bitfield_init id carrier rem in + (bitfield_initializer bf i :: el, rem') + end + +let rec transf_struct_init id fld_init_list = + match fld_init_list with + | [] -> [] + | (fld, i) :: rem -> + match is_bitfield id fld.fld_name with + | None -> + (fld, i) :: transf_struct_init id rem + | Some bf -> + let (el, rem') = + pack_bitfield_init id bf.bf_carrier fld_init_list in + ({fld_name = bf.bf_carrier; fld_typ = bf.bf_carrier_typ; + fld_bitfield = None}, + Init_single {edesc = ECast(bf.bf_carrier_typ, or_expr_list el); + etyp = bf.bf_carrier_typ}) + :: transf_struct_init id rem' + (* Check whether a field access (e.f or e->f) is a bitfield access. If so, return carrier expression (e and *e, respectively) and bitfield_info *) @@ -246,194 +321,134 @@ let rec is_bitfield_access env e = (* Expressions *) -let transf_expr env ctx e = - - let rec texp ctx e = - match e.edesc with - | EConst _ -> e - | ESizeof _ -> e - | EAlignof _ -> e - | EVar _ -> e - - | EUnop(Odot s, e1) -> - begin match is_bitfield_access env e with - | None -> - {edesc = EUnop(Odot s, texp Val e1); etyp = e.etyp} - | Some(ex, bf) -> - transf_read ex bf - end - | EUnop(Oarrow s, e1) -> - begin match is_bitfield_access env e with - | None -> - {edesc = EUnop(Oarrow s, texp Val e1); etyp = e.etyp} - | Some(ex, bf) -> - transf_read ex bf - end - | EUnop((Opreincr|Opredecr) as op, e1) -> - begin match is_bitfield_access env e1 with - | None -> - {edesc = EUnop(op, texp Val e1); etyp = e.etyp} - | Some(ex, bf) -> - transf_pre ctx (op_for_incr_decr op) ex bf e1.etyp - end - | EUnop((Opostincr|Opostdecr) as op, e1) -> - begin match is_bitfield_access env e1 with - | None -> - {edesc = EUnop(op, texp Val e1); etyp = e.etyp} - | Some(ex, bf) -> - transf_post ctx (op_for_incr_decr op) ex bf e1.etyp - end - | EUnop(op, e1) -> - {edesc = EUnop(op, texp Val e1); etyp = e.etyp} - - | EBinop(Oassign, e1, e2, ty) -> - begin match is_bitfield_access env e1 with - | None -> - {edesc = EBinop(Oassign, texp Val e1, texp Val e2, ty); - etyp = e.etyp} - | Some(ex, bf) -> - transf_assign ctx ex bf e2 +let rec transf_exp env ctx e = + match e.edesc with + | EConst _ -> e + | ESizeof _ -> e + | EAlignof _ -> e + | EVar _ -> e + + | EUnop(Odot s, e1) -> + begin match is_bitfield_access env e with + | None -> + {edesc = EUnop(Odot s, transf_exp env Val e1); etyp = e.etyp} + | Some(ex, bf) -> + transf_read env ex bf + end + | EUnop(Oarrow s, e1) -> + begin match is_bitfield_access env e with + | None -> + {edesc = EUnop(Oarrow s, transf_exp env Val e1); etyp = e.etyp} + | Some(ex, bf) -> + transf_read env ex bf end - | EBinop((Oadd_assign|Osub_assign|Omul_assign|Odiv_assign - |Omod_assign|Oand_assign|Oor_assign|Oxor_assign - |Oshl_assign|Oshr_assign) as op, - e1, e2, ty) -> - begin match is_bitfield_access env e1 with - | None -> - {edesc = EBinop(op, texp Val e1, texp Val e2, ty); etyp = e.etyp} - | Some(ex, bf) -> - transf_assignop ctx (op_for_assignop op) ex bf e2 ty + | EUnop((Opreincr|Opredecr) as op, e1) -> + begin match is_bitfield_access env e1 with + | None -> + {edesc = EUnop(op, transf_exp env Val e1); etyp = e.etyp} + | Some(ex, bf) -> + transf_pre env ctx (op_for_incr_decr op) ex bf e1.etyp end - | EBinop(Ocomma, e1, e2, ty) -> - {edesc = EBinop(Ocomma, texp Effects e1, texp Val e2, ty); - etyp = e.etyp} - | EBinop(op, e1, e2, ty) -> - {edesc = EBinop(op, texp Val e1, texp Val e2, ty); etyp = e.etyp} - - | EConditional(e1, e2, e3) -> - {edesc = EConditional(texp Val e1, texp ctx e2, texp ctx e3); - etyp = e.etyp} - | ECast(ty, e1) -> - {edesc = ECast(ty, texp Val e1); etyp = e.etyp} - | ECompound _ -> - assert false (* does not occur in unblocked code *) - | ECall(e1, el) -> - {edesc = ECall(texp Val e1, List.map (texp Val) el); etyp = e.etyp} - - and transf_read e bf = - bitfield_extract env bf - {edesc = EUnop(Odot bf.bf_carrier, texp Val e); etyp = bf.bf_carrier_typ} - - and transf_assign ctx e1 bf e2 = - bind_lvalue env (texp Val e1) (fun base -> - let carrier = - {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in - let asg = - eassign carrier (bitfield_assign env bf carrier (texp Val e2)) in - if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg) - - and transf_assignop ctx op e1 bf e2 tyres = - bind_lvalue env (texp Val e1) (fun base -> + | EUnop((Opostincr|Opostdecr) as op, e1) -> + begin match is_bitfield_access env e1 with + | None -> + {edesc = EUnop(op, transf_exp env Val e1); etyp = e.etyp} + | Some(ex, bf) -> + transf_post env ctx (op_for_incr_decr op) ex bf e1.etyp + end + | EUnop(op, e1) -> + {edesc = EUnop(op, transf_exp env Val e1); etyp = e.etyp} + + | EBinop(Oassign, e1, e2, ty) -> + begin match is_bitfield_access env e1 with + | None -> + {edesc = EBinop(Oassign, transf_exp env Val e1, + transf_exp env Val e2, ty); + etyp = e.etyp} + | Some(ex, bf) -> + transf_assign env ctx ex bf e2 + end + | EBinop((Oadd_assign|Osub_assign|Omul_assign|Odiv_assign + |Omod_assign|Oand_assign|Oor_assign|Oxor_assign + |Oshl_assign|Oshr_assign) as op, + e1, e2, ty) -> + begin match is_bitfield_access env e1 with + | None -> + {edesc = EBinop(op, transf_exp env Val e1, + transf_exp env Val e2, ty); etyp = e.etyp} + | Some(ex, bf) -> + transf_assignop env ctx (op_for_assignop op) ex bf e2 ty + end + | EBinop(Ocomma, e1, e2, ty) -> + {edesc = EBinop(Ocomma, transf_exp env Effects e1, + transf_exp env Val e2, ty); + etyp = e.etyp} + | EBinop(op, e1, e2, ty) -> + {edesc = EBinop(op, transf_exp env Val e1, transf_exp env Val e2, ty); + etyp = e.etyp} + + | EConditional(e1, e2, e3) -> + {edesc = EConditional(transf_exp env Val e1, + transf_exp env ctx e2, transf_exp env ctx e3); + etyp = e.etyp} + | ECast(ty, e1) -> + {edesc = ECast(ty, transf_exp env Val e1); etyp = e.etyp} + | ECompound(ty, i) -> + {edesc = ECompound(ty, transf_init env i); etyp = e.etyp} + | ECall(e1, el) -> + {edesc = ECall(transf_exp env Val e1, List.map (transf_exp env Val) el); + etyp = e.etyp} + +and transf_read env e bf = + bitfield_extract env bf + {edesc = EUnop(Odot bf.bf_carrier, transf_exp env Val e); + etyp = bf.bf_carrier_typ} + +and transf_assign env ctx e1 bf e2 = + bind_lvalue env (transf_exp env Val e1) (fun base -> + let carrier = + {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in + let asg = + eassign carrier (bitfield_assign env bf carrier (transf_exp env Val e2)) in + if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg) + +and transf_assignop env ctx op e1 bf e2 tyres = + bind_lvalue env (transf_exp env Val e1) (fun base -> + let carrier = + {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in + let rhs = + {edesc = EBinop(op, bitfield_extract env bf carrier, transf_exp env Val e2, tyres); + etyp = tyres} in + let asg = + eassign carrier (bitfield_assign env bf carrier rhs) in + if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg) + +and transf_pre env ctx op e1 bf tyfield = + transf_assignop env ctx op e1 bf (intconst 1L IInt) + (unary_conversion env tyfield) + +and transf_post env ctx op e1 bf tyfield = + if ctx = Effects then + transf_pre env ctx op e1 bf tyfield + else begin + bind_lvalue env (transf_exp env Val e1) (fun base -> let carrier = {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in + let temp = mk_temp env tyfield in + let tyres = unary_conversion env tyfield in + let settemp = eassign temp (bitfield_extract env bf carrier) in let rhs = - {edesc = EBinop(op, bitfield_extract env bf carrier, texp Val e2, tyres); - etyp = tyres} in + {edesc = EBinop(op, temp, intconst 1L IInt, tyres); etyp = tyres} in let asg = eassign carrier (bitfield_assign env bf carrier rhs) in - if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg) - - and transf_pre ctx op e1 bf tyfield = - transf_assignop ctx op e1 bf (intconst 1L IInt) - (unary_conversion env tyfield) - - and transf_post ctx op e1 bf tyfield = - if ctx = Effects then - transf_pre ctx op e1 bf tyfield - else begin - bind_lvalue env (texp Val e1) (fun base -> - let carrier = - {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in - let temp = mk_temp env tyfield in - let tyres = unary_conversion env tyfield in - let settemp = eassign temp (bitfield_extract env bf carrier) in - let rhs = - {edesc = EBinop(op, temp, intconst 1L IInt, tyres); etyp = tyres} in - let asg = - eassign carrier (bitfield_assign env bf carrier rhs) in - ecomma (ecomma settemp asg) temp) - end - - in texp ctx e - -(* Statements *) - -let transf_stmt env s = - Transform.stmt (fun loc env ctx e -> transf_expr env ctx e) env s - -(* Functions *) - -let transf_fundef env f = - Transform.fundef transf_stmt env f + ecomma (ecomma settemp asg) temp) + end (* Initializers *) -let bitfield_initializer bf i = - match i with - | Init_single e -> - let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in - let e_mask = - {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); - etyp = TInt(IUInt, [])} in - let e_and = - {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[])); - etyp = TInt(IUInt,[])} in - {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt, - TInt(IUInt, [])); - etyp = TInt(IUInt, [])} - | _ -> assert false - -let rec pack_bitfield_init id carrier fld_init_list = - match fld_init_list with - | [] -> ([], []) - | (fld, i) :: rem -> - try - let bf = Hashtbl.find bitfield_table (id, fld.fld_name) in - if bf.bf_carrier <> carrier then - ([], fld_init_list) - else begin - let (el, rem') = pack_bitfield_init id carrier rem in - (bitfield_initializer bf i :: el, rem') - end - with Not_found -> - ([], fld_init_list) - -let rec or_expr_list = function - | [] -> assert false - | [e] -> e - | e1 :: el -> - {edesc = EBinop(Oor, e1, or_expr_list el, TInt(IUInt,[])); - etyp = TInt(IUInt,[])} - -let rec transf_struct_init id fld_init_list = - match fld_init_list with - | [] -> [] - | (fld, i) :: rem -> - try - let bf = Hashtbl.find bitfield_table (id, fld.fld_name) in - let (el, rem') = - pack_bitfield_init id bf.bf_carrier fld_init_list in - ({fld_name = bf.bf_carrier; fld_typ = bf.bf_carrier_typ; - fld_bitfield = None}, - Init_single {edesc = ECast(bf.bf_carrier_typ, or_expr_list el); - etyp = bf.bf_carrier_typ}) - :: transf_struct_init id rem' - with Not_found -> - (fld, i) :: transf_struct_init id rem - -let rec transf_init env i = +and transf_init env i = match i with - | Init_single e -> Init_single (transf_expr env Val e) + | Init_single e -> Init_single (transf_exp env Val e) | Init_array il -> Init_array (List.map (transf_init env) il) | Init_struct(id, fld_init_list) -> let fld_init_list' = @@ -441,10 +456,25 @@ let rec transf_init env i = Init_struct(id, transf_struct_init id fld_init_list') | Init_union(id, fld, i) -> Init_union(id, fld, transf_init env i) +(* Declarations *) + let transf_decl env (sto, id, ty, init_opt) = (sto, id, ty, match init_opt with None -> None | Some i -> Some(transf_init env i)) +(* Statements *) + +let transf_stmt env s = + Transform.stmt + ~expr:(fun loc env ctx e -> transf_exp env ctx e) + ~decl:transf_decl + env s + +(* Functions *) + +let transf_fundef env f = + Transform.fundef transf_stmt env f + (* Programs *) let program p = diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 4d6d2137..221bd7cc 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -574,6 +574,19 @@ let is_function_type env t = | TFun _ -> true | _ -> false +(* Find the info for a field access *) + +let field_of_dot_access env t m = + match unroll env t with + | TStruct(id, _) -> Env.find_struct_member env (id, m) + | TUnion(id, _) -> Env.find_union_member env (id, m) + | _ -> assert false + +let field_of_arrow_access env t m = + match unroll env t with + | TPtr(t, _) | TArray(t, _, _) -> field_of_dot_access env t m + | _ -> assert false + (* Ranking of integer kinds *) let integer_rank = function @@ -964,8 +977,7 @@ let rec subst_stmt phi s = | Sskip | Sbreak | Scontinue - | Sgoto _ - | Sasm _ -> s.sdesc + | Sgoto _ -> s.sdesc | Sdo e -> Sdo (subst_expr phi e) | Sseq(s1, s2) -> Sseq (subst_stmt phi s1, subst_stmt phi s2) | Sif(e, s1, s2) -> @@ -981,6 +993,13 @@ let rec subst_stmt phi s = | Sreturn (Some e) -> Sreturn (Some (subst_expr phi e)) | Sblock sl -> Sblock (List.map (subst_stmt phi) sl) | Sdecl d -> Sdecl (subst_decl phi d) + | Sasm(attr, template, outputs, inputs, clob) -> + let subst_asm_operand (lbl, cstr, e) = + (lbl, cstr, subst_expr phi e) in + Sasm(attr, template, + List.map subst_asm_operand outputs, + List.map subst_asm_operand inputs, + clob) } diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 9d41f8fa..b1f77944 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -195,6 +195,10 @@ val fundef_typ: fundef -> typ val int_representable: int64 -> int -> bool -> bool (* Is the given int64 representable with the given number of bits and signedness? *) +val field_of_dot_access: Env.t -> typ -> string -> field + (* Return the field info for a [x.field] access *) +val field_of_arrow_access: Env.t -> typ -> string -> field + (* Return the field info for a [x->field] access *) (* Constructors *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index a1dd552b..10af10a1 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -365,6 +365,14 @@ let typespec_rank = function (* Don't change this *) let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2) +(* Is a specifier an anonymous struct/union in the sense of ISO C2011? *) + +let is_anonymous_composite spec = + List.exists + (function SpecType(Tstruct_union(_, None, Some _, _)) -> true + | _ -> false) + spec + (* Elaboration of a type specifier. Returns 5-tuple: (storage class, "inline" flag, "typedef" flag, elaborated type, new env) Optional argument "only" is true if this is a standalone @@ -617,6 +625,7 @@ and elab_init_name_group loc env (spec, namelist) = (* Elaboration of a field group *) and elab_field_group env (Field_group (spec, fieldlist, loc)) = + let fieldlist = List.map ( function | (None, x) -> (Name ("", JUSTBASE, [], cabslu), x) @@ -629,6 +638,11 @@ and elab_field_group env (Field_group (spec, fieldlist, loc)) = if sto <> Storage_default then error loc "non-default storage in struct or union"; + if fieldlist = [] then + if is_anonymous_composite spec then + error loc "ISO C99 does not support anonymous structs/unions" + else + warning loc "declaration does not declare any members"; let elab_bitfield (Name (_, _, _, loc), optbitsize) (id, ty) = let optbitsize' = @@ -1406,6 +1420,23 @@ let elab_expr loc env a = let b1 = elab a1 in if not (is_lvalue b1 || is_function_type env b1.etyp) then err "argument of '&' is not an l-value"; + begin match b1.edesc with + | EVar id -> + begin match wrap Env.find_ident loc env id with + | Env.II_ident(Storage_register, _) -> + err "address of register variable '%s' requested" id.name + | _ -> () + end + | EUnop(Odot f, b2) -> + let fld = wrap2 field_of_dot_access loc env b2.etyp f in + if fld.fld_bitfield <> None then + err "address of bit-field '%s' requested" f + | EUnop(Oarrow f, b2) -> + let fld = wrap2 field_of_arrow_access loc env b2.etyp f in + if fld.fld_bitfield <> None then + err "address of bit-field '%s' requested" f + | _ -> () + end; { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.etyp, []) } | UNARY(MEMOF, a1) -> diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index 1f602fc1..ca6c9da5 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -317,7 +317,7 @@ let transf_expr loc env ctx e = (* Statements *) let transf_stmt env s = - Transform.stmt transf_expr env s + Transform.stmt ~expr:transf_expr env s (* Functions *) diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 645465c3..317847a7 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -21,8 +21,8 @@ let transform_program t p name = let run_pass pass flag p = if CharSet.mem flag t then pass p else p in let p1 = (run_pass StructReturn.program 's' (run_pass PackedStructs.program 'p' - (run_pass Bitfields.program 'f' (run_pass Unblock.program 'b' + (run_pass Bitfields.program 'f' p)))) in let debug = if !Clflags.option_g && Configuration.advanced_debug then diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml index 8bfc6954..660f1d9b 100644 --- a/cparser/StructReturn.ml +++ b/cparser/StructReturn.ml @@ -423,6 +423,7 @@ let transf_decl env (sto, id, ty, init) = let transf_funbody env body optres = let transf_expr ctx e = transf_expr env ctx e in +let transf_asm_operand (lbl, cstr, e) = (lbl, cstr, transf_expr Val e) in (* Function returns: return kind scalar -> return e @@ -484,7 +485,10 @@ let rec transf_stmt s = {s with sdesc = Sblock(List.map transf_stmt sl)} | Sdecl d -> {s with sdesc = Sdecl(transf_decl env d)} - | Sasm _ -> s + | Sasm(attr, template, outputs, inputs, clob) -> + {s with sdesc = Sasm(attr, template, + List.map transf_asm_operand outputs, + List.map transf_asm_operand inputs, clob)} in transf_stmt body diff --git a/cparser/Transform.ml b/cparser/Transform.ml index 3b6f10f6..6cdd8a6b 100644 --- a/cparser/Transform.ml +++ b/cparser/Transform.ml @@ -138,37 +138,46 @@ let expand_postincrdecr ~read ~write env ctx op l = ecomma (eassign tmp (read l)) (ecomma (write l newval) tmp)) (* Generic transformation of a statement, transforming expressions within - and preserving the statement structure. Applies only to unblocked code. *) + and preserving the statement structure. + If [decl] is not given, it applies only to unblocked code. *) -let stmt trexpr env s = +let stmt ~expr ?(decl = fun env decl -> assert false) env s = let rec stm s = match s.sdesc with | Sskip -> s | Sdo e -> - {s with sdesc = Sdo(trexpr s.sloc env Effects e)} + {s with sdesc = Sdo(expr s.sloc env Effects e)} | Sseq(s1, s2) -> {s with sdesc = Sseq(stm s1, stm s2)} | Sif(e, s1, s2) -> - {s with sdesc = Sif(trexpr s.sloc env Val e, stm s1, stm s2)} + {s with sdesc = Sif(expr s.sloc env Val e, stm s1, stm s2)} | Swhile(e, s1) -> - {s with sdesc = Swhile(trexpr s.sloc env Val e, stm s1)} + {s with sdesc = Swhile(expr s.sloc env Val e, stm s1)} | Sdowhile(s1, e) -> - {s with sdesc = Sdowhile(stm s1, trexpr s.sloc env Val e)} + {s with sdesc = Sdowhile(stm s1, expr s.sloc env Val e)} | Sfor(s1, e, s2, s3) -> - {s with sdesc = Sfor(stm s1, trexpr s.sloc env Val e, stm s2, stm s3)} + {s with sdesc = Sfor(stm s1, expr s.sloc env Val e, stm s2, stm s3)} | Sbreak -> s | Scontinue -> s | Sswitch(e, s1) -> - {s with sdesc = Sswitch(trexpr s.sloc env Val e, stm s1)} + {s with sdesc = Sswitch(expr s.sloc env Val e, stm s1)} | Slabeled(lbl, s) -> {s with sdesc = Slabeled(lbl, stm s)} | Sgoto lbl -> s | Sreturn None -> s | Sreturn (Some e) -> - {s with sdesc = Sreturn(Some(trexpr s.sloc env Val e))} - | Sasm _ -> s - | Sblock _ | Sdecl _ -> - assert false (* should not occur in unblocked code *) + {s with sdesc = Sreturn(Some(expr s.sloc env Val e))} + | Sasm(attr, template, outputs, inputs, clob) -> + let asm_operand (lbl, cstr, e) = + (lbl, cstr, expr s.sloc env Val e) in + {s with sdesc = Sasm(attr, template, + List.map asm_operand outputs, + List.map asm_operand inputs, clob)} + | Sblock sl -> + {s with sdesc = Sblock (List.map stm sl)} + | Sdecl d -> + {s with sdesc = Sdecl (decl env d)} + in stm s (* Generic transformation of a function definition *) diff --git a/cparser/Transform.mli b/cparser/Transform.mli index 718a2f9c..57a4737b 100644 --- a/cparser/Transform.mli +++ b/cparser/Transform.mli @@ -50,8 +50,10 @@ val expand_postincrdecr : (** Generic transformation of a statement *) -val stmt : (C.location -> Env.t -> context -> C.exp -> C.exp) -> - Env.t -> C.stmt -> C.stmt +val stmt : + expr: (C.location -> Env.t -> context -> C.exp -> C.exp) -> + ?decl: (Env.t -> C.decl -> C.decl) -> + Env.t -> C.stmt -> C.stmt (** Generic transformation of a function definition *) diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 4013db9b..91f50552 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -225,7 +225,13 @@ let rec unblock_stmt env s = {s with sdesc = Sreturn(Some (expand_expr true env e))} | Sblock sl -> unblock_block env sl | Sdecl d -> assert false - | Sasm _ -> s + | Sasm(attr, template, outputs, inputs, clob) -> + let expand_asm_operand (lbl, cstr, e) = + (lbl, cstr, expand_expr true env e) in + {s with sdesc = Sasm(attr, template, + List.map expand_asm_operand outputs, + List.map expand_asm_operand inputs, clob)} + and unblock_block env = function | [] -> sskip |