diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml
index bd68e4e9f103884dfda6827bc98f901cb8aa0ab7..73bba3df3e4578ceeab586eeea19df61a2694e66 100644
--- a/src/kernel_services/ast_building/cil_builder.ml
+++ b/src/kernel_services/ast_building/cil_builder.ml
@@ -22,6 +22,11 @@
let unknown_loc = Cil_datatype.Location.unknown
+exception BuildError of string
+
+let error format =
+ Format.kasprintf (fun s -> raise (BuildError s)) format
+
(* --- Types --- *)
@@ -32,6 +37,7 @@ struct
type ('value,'shape) morphology =
| Single : ('value,'value) morphology
| Listed : ('value,'shape) typ -> ('value,'shape list) morphology
+ | Record : (Cil_types.fieldinfo -> 'a -> 'value) -> ('value,'a) morphology
and ('value,'shape) typ = ('value,'shape) morphology * Cil_types.logic_type
@@ -75,6 +81,8 @@ struct
Ctype (TArray (t, size, []))
| _, _ -> raise NotACType
+ let structure compinfo f =
+ Record f, Ctype (TComp (compinfo, []))
(* Attrbutes *)
@@ -112,6 +120,34 @@ struct
end
+(* --- Variables scoping --- *)
+
+module Scope =
+struct
+ type id = int64
+
+ let new_id : unit -> id =
+ let last_id = ref Int64.zero in
+ fun () ->
+ last_id := Int64.(add !last_id one);
+ !last_id
+
+ module IdMap = Map.Make (Int64)
+
+ type t = Cil_types.varinfo IdMap.t
+
+ exception OutOfScope of string
+
+ let empty : t = IdMap.empty
+ let add : id -> Cil_types.varinfo -> t -> t = IdMap.add
+
+ let resolve (scope : t) (id : id) (name : string) : Cil_types.varinfo =
+ match IdMap.find_opt id scope with
+ | Some vi -> vi
+ | None -> raise (OutOfScope name)
+end
+
+
(* --- C & Logic expressions builder --- *)
module Exp =
@@ -135,7 +171,8 @@ struct
| Integer of Integer.t
| CilConstant of Cil_types.constant
and var' =
- Cil_types.varinfo
+ | CilVar of Cil_types.varinfo
+ | NewVar of Scope.id * string * Cil_types.typ
and lval' =
| CilLval of Cil_types.lval
| Var of var'
@@ -169,7 +206,8 @@ struct
and init' =
| CilInit of Cil_types.init
| SingleInit of exp'
- | CompoundInit of Cil_types.typ * init' list
+ | ArrayInit of Cil_types.typ * init' list
+ | StructInit of Cil_types.typ * (Cil_types.fieldinfo * init') list (* ordered *)
type const = [ `const of const' ]
type var = [ `var of var' ]
@@ -183,8 +221,9 @@ struct
| Int i -> Format.pp_print_int fmt i
| Integer i -> Integer.pretty fmt i
| CilConstant c -> Printer.pp_constant fmt c
- and pretty_var fmt v =
- Printer.pp_varinfo fmt v
+ and pretty_var fmt = function
+ | CilVar vi -> Printer.pp_varinfo fmt vi
+ | NewVar (_id,name,_typ) -> Format.pp_print_string fmt name
and pretty_lval fmt = function
| CilLval lv -> Printer.pp_lval fmt lv
| Var v -> pretty_var fmt v
@@ -233,8 +272,11 @@ struct
and pretty_init fmt = function
| CilInit init -> Printer.pp_init fmt init
| SingleInit e -> pretty_exp fmt e
- | CompoundInit (_,l) ->
+ | ArrayInit (_,l) ->
Format.fprintf fmt "{%a}" (Pretty_utils.pp_list ~sep:",@ " pretty_init) l
+ | StructInit (_,l) ->
+ Format.fprintf fmt "{%a}" (Pretty_utils.pp_list ~sep:",@ " pretty_init) @@
+ List.map snd l
let pretty fmt = function
| `none -> ()
@@ -305,13 +347,14 @@ struct
(* Lvalues *)
- let var v = `var v
+ let var v = `var (CilVar v)
let of_lval lv = `lval (CilLval lv)
(* Expressions *)
let of_exp e = `exp (CilExp e)
let of_exp_copy e = `exp (CilExpCopy e)
+ let of_exp_list l = List.map of_exp l
let unop op e = `exp (Unop (op, harden_exp e))
let neg e = unop Cil_types.Neg e
let lognot e = unop Cil_types.LNot e
@@ -381,13 +424,31 @@ struct
(* Initializations *)
let of_init i = `init (CilInit i)
- let compound t l = `init (CompoundInit (t, List.map harden_init l))
+ let compound t l =
+ match t with
+ | Cil_types.TArray _ ->
+ `init (ArrayInit (t, List.map harden_init l))
+ | Cil_types.TComp (comp,_) ->
+ let field_init field init =
+ field, harden_init init
+ in
+ `init (StructInit (t, List.map2 field_init (Option.get comp.cfields) l ))
+ | _ -> invalid_arg "compound: type must be a C array, struct or union"
let rec values : type a. (init, a) typ -> a -> [> init] =
fun ty x ->
match ty with
| Single, Ctype _ -> x
| Listed sub, Ctype t-> compound t (List.map (values sub) x)
+ | Record f, Ctype (TComp (comp,_) as t) ->
+ let field_init field =
+ field, harden_init (f field x)
+ in
+ `init (StructInit (t, List.map field_init (Option.get comp.cfields)))
+ | Record _, _ ->
+ (* invariant: Record initializers can only be associated with C structures
+ or unions. *)
+ assert false
| _, _ -> raise NotACType
(* Operators *)
@@ -396,6 +457,7 @@ struct
let (<<), (>>) = shiftl, shiftr
let (<), (>), (<=), (>=), (==), (!=) = lt, gt, le, ge, eq, ne
let (--) = range
+ let (.@[]) = index
(* Convert *)
@@ -405,6 +467,7 @@ struct
exception NotAPredicate of exp
exception NotAFunction of Cil_types.logic_info
exception Typing_error of string
+ exception OutOfScope = Scope.OutOfScope
let typing_error s =
raise (Typing_error s)
@@ -421,16 +484,20 @@ struct
| Int i -> build_constant (Integer (Integer.of_int i))
| Integer i -> Cil_types.(CInt64 (i, IInt, None))
- and build_lval ~loc = function
+ and build_var ~scope = function
+ | CilVar vi -> vi
+ | NewVar (vid, name,_typ) -> Scope.resolve scope vid name
+
+ and build_lval ~scope ~loc = function
| Result as lv -> raise (LogicInC (`lval lv))
| CilLval lval -> lval
- | Var v -> Cil_types.(Var v, NoOffset)
+ | Var v -> Cil_types.(Var (build_var ~scope v), NoOffset)
| Mem e ->
- let e' = build_exp ~loc e in
+ let e' = build_exp ~scope ~loc e in
Cil.mkMem ~addr:e' ~off:Cil_types.NoOffset
| Index (lv, e) ->
- let (host, offset) as lv' = build_lval ~loc lv
- and e' = build_exp ~loc e in
+ let (host, offset) as lv' = build_lval ~scope ~loc lv
+ and e' = build_exp ~scope ~loc e in
begin match Cil.(unrollType (typeOfLval lv')) with
| TArray _ ->
let offset' = Cil_types.Index (e', NoOffset) in
@@ -443,7 +510,7 @@ struct
or a pointer"
end
| (Field (lv,_) | FieldNamed (lv,_)) as e ->
- let (host, offset) as lv' = build_lval ~loc lv in
+ let (host, offset) as lv' = build_lval ~scope ~loc lv in
let host', offset', ci = match Cil.(unrollTypeDeep (typeOfLval lv')) with
| TComp (ci,_) -> host, offset, ci
| TPtr (TComp (ci,_),_) ->
@@ -459,16 +526,16 @@ struct
let offset'' = Cil_types.(Field (f, NoOffset)) in
host', Cil.addOffset offset'' offset'
- and build_exp ~loc = function
+ and build_exp ~scope ~loc = function
| CilTerm _ | Range _ | App _ | Pred _ as e -> raise (LogicInC (`exp e))
| CilExp exp -> exp
| CilExpCopy exp -> Cil.copy_exp exp
| Const c->
Cil.new_exp ~loc (Cil_types.Const (build_constant c))
| Lval lval ->
- Cil.new_exp ~loc (Cil_types.Lval (build_lval ~loc lval))
+ Cil.new_exp ~loc (Cil_types.Lval (build_lval ~scope ~loc lval))
| Unop (op,e) ->
- let e' = build_exp ~loc e in
+ let e' = build_exp ~scope ~loc e in
let oldt = Cil.typeOf e' in
let newt = Cil.integralPromotion oldt in
Cil.(new_exp ~loc (Cil_types.UnOp (op, mkCastT ~oldt ~newt e', oldt)))
@@ -476,8 +543,8 @@ struct
let is_pointer_type e =
Cil.(isPointerType (typeOf e))
in
- let e1' = build_exp ~loc e1
- and e2' = build_exp ~loc e2 in
+ let e1' = build_exp ~scope ~loc e1
+ and e2' = build_exp ~scope ~loc e2 in
let op' = match op with (* Normalize operation *)
| PlusA when is_pointer_type e1' -> Cil_types.PlusPI
| MinusA when is_pointer_type e1' -> Cil_types.MinusPI
@@ -487,22 +554,23 @@ struct
in
Cil.mkBinOp ~loc op' e1' e2'
| Cast (Cil_types.Ctype newt, e) ->
- Cil.mkCast ~force:false ~newt (build_exp ~loc e)
+ Cil.mkCast ~force:false ~newt (build_exp ~scope ~loc e)
| Cast _ ->
raise NotACType
| Addr lv ->
- Cil.mkAddrOrStartOf ~loc (build_lval ~loc lv)
+ Cil.mkAddrOrStartOf ~loc (build_lval ~scope ~loc lv)
- let rec build_term_lval ~loc ~restyp = function
+ let rec build_term_lval ~scope ~loc ~restyp = function
| Result -> Cil_types.(TResult (Option.get restyp), TNoOffset)
| CilLval _ as lv -> raise (CInLogic (`lval lv))
- | Var v -> Cil_types.(TVar (Cil.cvar_to_lvar v), TNoOffset)
+ | Var v ->
+ Cil_types.(TVar (Cil.cvar_to_lvar (build_var ~scope v)), TNoOffset)
| Mem t ->
- let t' = build_term ~loc ~restyp t in
+ let t' = build_term ~scope ~loc ~restyp t in
Cil_types.(TMem t', TNoOffset)
| Index (tlv, t) ->
- let (host, offset) as tlv' = build_term_lval ~loc ~restyp tlv
- and t' = build_term ~loc ~restyp t in
+ let (host, offset) as tlv' = build_term_lval ~scope ~loc ~restyp tlv
+ and t' = build_term ~scope ~loc ~restyp t in
let lty = Cil.typeOfTermLval tlv' in
begin match Logic_utils.unroll_type lty with
| Ctype (TArray _) ->
@@ -516,7 +584,7 @@ struct
array or a C pointer"
end
| (Field (tlv,_) | FieldNamed (tlv,_)) as t ->
- let (host, offset) as tlv' = build_term_lval ~loc ~restyp tlv in
+ let (host, offset) as tlv' = build_term_lval ~scope ~loc ~restyp tlv in
let lty = match Logic_utils.unroll_type (Cil.typeOfTermLval tlv') with
| Ctype cty -> Cil_types.Ctype (Cil.unrollTypeDeep cty)
| lty -> lty
@@ -536,7 +604,7 @@ struct
let offset'' = Cil_types.(TField (f, TNoOffset)) in
host', Logic_const.addTermOffset offset'' offset'
- and build_term ~loc ~restyp = function
+ and build_term ~scope ~loc ~restyp = function
| Const (CilConstant _) | CilExp _ | CilExpCopy _ as e ->
raise (CInLogic (`exp e))
| Pred _ as e ->
@@ -547,16 +615,16 @@ struct
| Const (Integer i) ->
Logic_const.tint ~loc i
| Lval lval ->
- let tlval = build_term_lval ~loc ~restyp lval in
+ let tlval = build_term_lval ~scope ~loc ~restyp lval in
Logic_const.term ~loc Cil_types.(TLval tlval) (Cil.typeOfTermLval tlval)
| Unop (op,t) ->
- let t' = build_term t ~loc ~restyp in
+ let t' = build_term t ~scope ~loc ~restyp in
let ty = t'.Cil_types.term_type in
(* TODO: type conversion *)
Logic_const.term ~loc Cil_types.(TUnOp (op,t')) ty
| Binop (op,t1,t2) ->
- let t1' = build_term ~loc ~restyp t1
- and t2' = build_term ~loc ~restyp t2 in
+ let t1' = build_term ~scope ~loc ~restyp t1
+ and t2' = build_term ~scope ~loc ~restyp t2 in
let ty = t1'.Cil_types.term_type in
let op' = match op with (* Normalize operation *)
| PlusA when Logic_utils.isLogicPointer t1' -> Cil_types.PlusPI
@@ -568,25 +636,25 @@ struct
(* TODO: type conversion *)
Logic_const.term ~loc Cil_types.(TBinOp (op',t1',t2')) ty
| Cast (Ctype ct, t) ->
- let t' = build_term ~loc ~restyp t in
+ let t' = build_term ~scope ~loc ~restyp t in
Logic_utils.mk_cast ~loc ct t'
| Cast (ty, t) ->
- let t' = build_term ~loc ~restyp t in
+ let t' = build_term ~scope ~loc ~restyp t in
Logic_utils.numeric_coerce ty t'
| Addr lval ->
- let tlval = build_term_lval ~loc ~restyp lval in
+ let tlval = build_term_lval ~scope ~loc ~restyp lval in
let ty = Cil.typeOfTermLval tlval in
Logic_utils.mk_logic_AddrOf ~loc tlval ty
| Range (t1,t2) ->
- let t1' = Option.map (build_term ~loc ~restyp) t1
- and t2' = Option.map (build_term ~loc ~restyp) t2 in
+ let t1' = Option.map (build_term ~scope ~loc ~restyp) t1
+ and t2' = Option.map (build_term ~scope ~loc ~restyp) t2 in
Logic_const.trange ~loc (t1',t2')
| App (logic_info, labels, args) ->
let ty = match logic_info.l_type with
| None -> raise (NotAFunction logic_info)
| Some ty -> ty
in
- let args' = List.map (build_term ~loc ~restyp) args in
+ let args' = List.map (build_term ~scope ~loc ~restyp) args in
Logic_const.term ~loc (Tapp (logic_info, labels, args')) ty
and build_relation e = function
@@ -598,83 +666,97 @@ struct
| Cil_types.Ne -> Cil_types.Rneq
| _ -> raise (NotAPredicate (`exp e))
- and build_pred_node ~loc ~restyp = function
+ and build_pred_node ~scope ~loc ~restyp = function
| Unop (Cil_types.LNot, p) ->
- let p' = build_pred ~loc ~restyp p in
+ let p' = build_pred ~scope ~loc ~restyp p in
Cil_types.Pnot p'
| Binop (Cil_types.LAnd, p1, p2) ->
- let p1' = build_pred ~loc ~restyp p1
- and p2' = build_pred ~loc ~restyp p2 in
+ let p1' = build_pred ~scope ~loc ~restyp p1
+ and p2' = build_pred ~scope ~loc ~restyp p2 in
Cil_types.Pand (p1',p2')
| Binop (Cil_types.LOr, p1, p2) ->
- let p1' = build_pred ~loc ~restyp p1
- and p2' = build_pred ~loc ~restyp p2 in
+ let p1' = build_pred ~scope ~loc ~restyp p1
+ and p2' = build_pred ~scope ~loc ~restyp p2 in
Cil_types.Por (p1',p2')
| Binop (binop, t1, t2) as e ->
let rel = build_relation e binop
- and t1' = build_term ~loc ~restyp t1
- and t2' = build_term ~loc ~restyp t2 in
+ and t1' = build_term ~scope ~loc ~restyp t1
+ and t2' = build_term ~scope ~loc ~restyp t2 in
Cil_types.Prel (rel, t1', t2')
| Const _ | CilExp _ | CilExpCopy _ | CilTerm _
| Lval _ | Unop _ | Cast _ | Addr _ | Range _ as e ->
raise (NotAPredicate (`exp e))
| App (logic_info, labels, args) ->
- let args' = List.map (build_term ~loc ~restyp) args in
+ let args' = List.map (build_term ~scope ~loc ~restyp) args in
Cil_types.Papp (logic_info, labels, args')
| Pred (ObjectPointer (l, t)) ->
- Cil_types.Pobject_pointer (l, build_term ~loc ~restyp t)
+ Cil_types.Pobject_pointer (l, build_term ~scope ~loc ~restyp t)
| Pred (Valid (l, t)) ->
- Cil_types.Pvalid (l, build_term ~loc ~restyp t)
+ Cil_types.Pvalid (l, build_term ~scope ~loc ~restyp t)
| Pred (ValidRead (l, t)) ->
- Cil_types.Pvalid_read (l, build_term ~loc ~restyp t)
+ Cil_types.Pvalid_read (l, build_term ~scope ~loc ~restyp t)
| Pred (Initialized (l, t)) ->
- Cil_types.Pinitialized (l, build_term ~loc ~restyp t)
+ Cil_types.Pinitialized (l, build_term ~scope ~loc ~restyp t)
| Pred (Dangling (l, t)) ->
- Cil_types.Pdangling (l, build_term ~loc ~restyp t)
+ Cil_types.Pdangling (l, build_term ~scope ~loc ~restyp t)
| Pred (Allocable (l, t)) ->
- Cil_types.Pallocable (l, build_term ~loc ~restyp t)
+ Cil_types.Pallocable (l, build_term ~scope ~loc ~restyp t)
| Pred (Freeable (l, t)) ->
- Cil_types.Pfreeable (l, build_term ~loc ~restyp t)
+ Cil_types.Pfreeable (l, build_term ~scope ~loc ~restyp t)
| Pred (Fresh (l1, l2, t1, t2)) ->
- let t1' = build_term ~loc ~restyp t1
- and t2' = build_term ~loc ~restyp t2 in
+ let t1' = build_term ~scope ~loc ~restyp t1
+ and t2' = build_term ~scope ~loc ~restyp t2 in
Cil_types.Pfresh (l1, l2, t1', t2')
- and build_pred ~loc ~restyp t =
- Logic_const.unamed ~loc (build_pred_node ~loc ~restyp t)
+ and build_pred ~scope ~loc ~restyp t =
+ Logic_const.unamed ~loc (build_pred_node ~scope ~loc ~restyp t)
- let rec build_init ~loc = function
+ let rec build_init ~scope ~loc = function
| CilInit init -> init
| SingleInit e ->
- Cil_types.SingleInit (build_exp ~loc e)
- | CompoundInit (typ,l) ->
+ Cil_types.SingleInit (build_exp ~scope ~loc e)
+ | ArrayInit (typ,l) ->
let index i = Cil_types.(Index (Cil.integer ~loc i, NoOffset)) in
- let initl = List.mapi (fun i sub -> index i, build_init ~loc sub) l in
+ let initl =
+ List.mapi (fun i sub -> index i, build_init ~scope ~loc sub) l
+ in
+ Cil_types.CompoundInit (typ, initl)
+ | StructInit (typ,l) ->
+ let field fi = Cil_types.(Field (fi,NoOffset)) in
+ let initl =
+ List.map (fun (fi,sub) -> field fi, build_init ~scope ~loc sub) l
+ in
Cil_types.CompoundInit (typ, initl)
(* Export *)
let cil_logic_label label = label
- let cil_varinfo v = harden_var v
let cil_constant c = build_constant (harden_const c)
- let cil_lval ~loc lv = build_lval ~loc (harden_lval lv)
+ let cil_varinfo v = build_var ~scope:Scope.empty (harden_var v)
+ let cil_lval ~loc lv = build_lval ~scope:Scope.empty ~loc (harden_lval lv)
let cil_lval_opt ~loc lv =
- Option.map (build_lval ~loc) (harden_lval_opt lv)
- let cil_exp ~loc e = build_exp ~loc (harden_exp e)
- let cil_exp_opt ~loc e = Option.map (build_exp ~loc) (harden_exp_opt e)
+ Option.map (build_lval ~scope:Scope.empty ~loc) (harden_lval_opt lv)
+ let cil_exp ~loc e = build_exp ~scope:Scope.empty ~loc (harden_exp e)
+ let cil_exp_opt ~loc e =
+ Option.map (build_exp ~scope:Scope.empty ~loc) (harden_exp_opt e)
let cil_exp_list ~loc l = List.map (cil_exp ~loc) l
let cil_term_lval ~loc ?restyp lv =
- build_term_lval ~loc ~restyp (harden_lval lv)
- let cil_term ~loc ?restyp e = build_term ~loc ~restyp (harden_exp e)
+ build_term_lval ~scope:Scope.empty ~loc ~restyp (harden_lval lv)
+ let cil_term ~loc ?restyp e =
+ build_term ~scope:Scope.empty ~loc ~restyp (harden_exp e)
let cil_iterm ~loc ?restyp e =
Logic_const.new_identified_term (cil_term ~loc ?restyp e)
- let cil_pred ~loc ?restyp e = build_pred ~loc ~restyp (harden_exp e)
+ let cil_pred ~loc ?restyp e =
+ build_pred ~scope:Scope.empty ~loc ~restyp (harden_exp e)
let cil_ipred ~loc ?restyp e =
Logic_const.new_predicate (cil_pred ~loc ?restyp e)
- let cil_init ~loc i = build_init ~loc (harden_init i)
+ let cil_init ~loc i = build_init ~scope:Scope.empty ~loc (harden_init i)
- let cil_typeof (`var vi) = vi.Cil_types.vtype
+ let cil_typeof (`var v) =
+ match v with
+ | CilVar vi -> vi.Cil_types.vtype
+ | NewVar (_id,_name,typ) -> typ
end
@@ -684,33 +766,32 @@ module Pure =
struct
include Exp
+ exception DeclarationOutsideOfFunction
+
+ type ghost = NoGhost | Ghost
+
type instr' =
| CilInstr of Cil_types.instr
| Skip
| Assign of lval' * exp'
| Call of lval' option * exp' * exp' list
+ | Local of var' * init' option * ghost
+ | LocalCopy of Cil_types.varinfo * var' * init' option * ghost
type stmt' =
| CilStmt of Cil_types.stmt
| CilStmtkind of Cil_types.stmtkind
| Instr of instr'
| Sequence of stmt' list
- | Ghost of stmt'
+ | Block of stmt' list
+ | GhostSection of stmt'
+ | If of exp' * block * block
+
+ and block = stmt' list * Cil_types.attributes
type instr = [ `instr of instr' ]
type stmt = [ instr | `stmt of stmt' ]
- (* Sequences *)
-
- let flatten_sequences l =
- let rec add_one acc = function
- | Sequence l -> add_list acc l
- | stmt -> stmt :: acc
- and add_list acc l =
- List.fold_left add_one acc l
- in
- List.rev (add_list [] l)
-
(* Depolymorphize *)
let harden_instr i =
@@ -722,6 +803,9 @@ struct
| #instr as instr -> Instr (harden_instr instr)
| `stmt stmt -> stmt
+ let harden_block l attributes : block =
+ List.map harden_stmt l, attributes
+
(* Build *)
let of_instr i = `instr (CilInstr i)
@@ -734,48 +818,173 @@ struct
let of_stmtkind sk = `stmt (CilStmtkind sk)
let of_stmt s = `stmt (CilStmt s)
let of_stmts l = `stmt (Sequence (List.map (fun s -> CilStmt s) l))
- let block l = `stmt (Sequence (List.map harden_stmt l))
- let ghost s = `stmt (Ghost (harden_stmt s))
+ let sequence l = `stmt (Sequence (List.map harden_stmt l))
+ let block l = `stmt (Block (List.map harden_stmt l))
+ let ghost s = `stmt (GhostSection (harden_stmt s))
+
+ let if_ ?(ghost_else=false) cond ~then_ ~else_ =
+ let else_attributes =
+ if ghost_else
+ then [Cil_types.Attr (Cil.frama_c_ghost_else,[])]
+ else []
+ in
+ `stmt (If (
+ harden_exp cond,
+ harden_block then_ [],
+ harden_block else_ else_attributes))
+ let local' ?(ghost=false) ?init typ name =
+ let var = NewVar (Scope.new_id (), name, typ) in
+ let ghost = if ghost then Ghost else NoGhost in
+ let instr = Local (var, Option.map harden_init init, ghost) in
+ `var var, `instr instr
+
+ let local ?ghost ?init ty name =
+ let init = Option.map (values ty) init in
+ local' ?ghost ?init (cil_typ ty) name
+
+ let local_copy ?(ghost=false) ?(suffix="_tmp") v =
+ let name, typ, vi =
+ match harden_var v with
+ | NewVar (_id, name, typ) -> name, typ, None
+ | CilVar vi -> vi.vname, vi.vtype, Some vi
+ in
+ let var = NewVar (Scope.new_id (), name ^ suffix, typ) in
+ let ghost = if ghost then Ghost else NoGhost in
+ let instr = match vi with
+ | None -> Local (var, None, ghost)
+ | Some vi -> LocalCopy (vi, var, None, ghost)
+ in
+ `var var, `instr instr
(* Convert *)
- let build_instr ~loc = function
- | CilInstr i -> i
+ (* block: refers to the innermost englobing block where locals must be added
+ fundec: refers to the owner function where locals must also be added *)
+
+ let build_local_definition ~scope ~loc ~block ~fundec v init ghost copied_vi =
+ let vi, scope = match v with
+ | CilVar vi -> vi, scope
+ | NewVar (id, name, typ) ->
+ let temp = false and global = false and formal = false in
+ let ghost = match ghost with Ghost -> true | NoGhost -> false in
+ let vi =
+ match copied_vi with
+ | None -> Cil.makeVarinfo ~temp ~ghost global formal name typ
+ | Some vi -> Cil.copyVarinfo vi name
+ in
+ let block, fundec = match block, fundec with
+ | Some block, Some fundec -> block, fundec
+ | None, _ | _, None -> raise DeclarationOutsideOfFunction
+ in
+ (* Register the variable *)
+ Cil.refresh_local_name fundec vi;
+ vi.vdecl <- loc;
+ fundec.slocals <- fundec.slocals @ [vi];
+ block.Cil_types.blocals <- vi :: block.Cil_types.blocals;
+ vi, Scope.add id vi scope
+ in
+ (* Initialization *)
+ let initialization =
+ match init with
+ | None -> Cil_types.Skip loc
+ | Some init ->
+ vi.vdefined <- true;
+ let local_init = Cil_types.AssignInit (build_init ~scope ~loc init) in
+ Cil_types.Local_init (vi, local_init, loc)
+ in
+ initialization, scope
+
+ let build_instr ~scope ~loc ~block ~fundec = function
+ | CilInstr i -> i, scope
| Skip ->
- Cil_types.Skip (loc)
+ Cil_types.Skip (loc), scope
| Assign (dest,src) ->
- let dest' = build_lval ~loc dest
- and src' = build_exp ~loc src in
+ let dest' = build_lval ~scope ~loc dest
+ and src' = build_exp ~scope ~loc src in
let src' = Cil.mkCast ~newt:(Cil.typeOfLval dest') src' in
- Cil_types.Set (dest', src', loc)
+ Cil_types.Set (dest', src', loc), scope
| Call (dest,callee,args) ->
- let dest' = Option.map (build_lval ~loc) dest
- and callee' = build_exp ~loc callee
- and args' = List.map (build_exp ~loc) args in
- Cil_types.Call (dest', callee', args', loc)
-
- let rec build_stmtkind ~loc ~ghost = function
- | CilStmt s -> s.Cil_types.skind
- | CilStmtkind sk -> sk
- | Instr i -> Cil_types.Instr (build_instr ~loc i)
- | Sequence l -> Cil_types.Block (build_block ~loc ~ghost l)
- | Ghost s -> Cil_types.Block (build_block ~loc ~ghost:true [s])
-
- and build_stmt ~loc ~ghost = function
- | CilStmt s -> s
- | Ghost s -> build_stmt ~loc ~ghost:true s
- | stmt -> Cil.mkStmt ~ghost (build_stmtkind ~loc ~ghost stmt)
-
- and build_block ~loc ~ghost l =
- let bstmts = List.map (build_stmt ~ghost ~loc) (flatten_sequences l) in
- Cil.mkBlock bstmts
+ let dest' = Option.map (build_lval ~scope ~loc) dest
+ and callee' = build_exp ~scope ~loc callee
+ and args' = List.map (build_exp ~scope ~loc) args in
+ Cil_types.Call (dest', callee', args', loc), scope
+ | Local (v, init, ghost) ->
+ build_local_definition ~scope ~loc ~block ~fundec v init ghost None
+ | LocalCopy (vi, v, init, ghost) ->
+ build_local_definition ~scope ~loc ~block ~fundec v init ghost (Some vi)
+
+ let rec build_stmtkind ~scope ~loc ~ghost ~block ~fundec = function
+ | CilStmtkind sk -> sk, scope
+ | Instr i ->
+ let instr, scope = build_instr ~scope ~loc ~block ~fundec i in
+ Cil_types.Instr instr, scope
+ | If (exp, then_stmts, else_stmt) ->
+ Cil_types.If (
+ build_exp ~scope ~loc exp,
+ build_block ~scope ~loc ~ghost ~fundec then_stmts,
+ build_block ~scope ~loc ~ghost ~fundec else_stmt,
+ loc
+ ),
+ scope
+ | Sequence s | Block s ->
+ Cil_types.Block (build_block ~scope ~loc ~ghost ~fundec (s,[])), scope
+ | (CilStmt _) as s | GhostSection s ->
+ let ghost = true in
+ Cil_types.Block (build_block ~scope ~loc ~ghost ~fundec ([s],[])), scope
+
+ and build_stmtlist_rev ~scope ~loc ~ghost ~block ~fundec acc l =
+ let add_one (acc,scope) stmt =
+ match stmt with
+ | CilStmt s -> s :: acc, scope
+ | Sequence s -> (* do not build a block if unecessary *)
+ build_stmtlist_rev ~scope ~loc ~ghost ~block ~fundec acc s
+ | GhostSection stmt -> (* do not build a block if unecessary *)
+ build_stmtlist_rev ~scope ~loc ~ghost:true ~block ~fundec acc [stmt]
+ | _ ->
+ let stmtkind, scope =
+ build_stmtkind ~scope ~loc ~ghost ~block ~fundec stmt
+ in
+ match stmtkind with
+ | Instr (Cil_types.Skip _) -> acc, scope (* Filter skips out *)
+ | stmtkind ->
+ Cil.mkStmt ~ghost stmtkind :: acc, scope
+ in
+ List.fold_left add_one (acc,scope) l
+
+ and build_stmt ~scope ~loc ~ghost ~block ~fundec = function
+ | CilStmt s -> s, scope
+ | GhostSection s -> build_stmt ~scope ~loc ~ghost:true ~block ~fundec s
+ | stmt ->
+ let stmtkind, scope =
+ build_stmtkind ~scope ~loc ~ghost ~block ~fundec stmt
+ in
+ Cil.mkStmt ~ghost stmtkind, scope
+
+ and build_block ~scope ~loc ~ghost ~fundec (l, attributes) =
+ let block = Cil.mkBlock [] in
+ let bstmts, _scope =
+ build_stmtlist_rev ~scope ~loc ~ghost ~block:(Some block) ~fundec [] l
+ in
+ block.battrs <- attributes;
+ block.bstmts <- List.rev bstmts;
+ block
+
(* Export *)
- let cil_instr ~loc i = build_instr ~loc (harden_instr i)
- let cil_stmtkind ~loc s = build_stmtkind ~loc ~ghost:false (harden_stmt s)
- let cil_stmt ~loc s = build_stmt ~loc ~ghost:false (harden_stmt s)
+ let top_block =
+ Option.map (fun fundec -> fundec.Cil_types.sbody)
+
+ let cil_instr ?into:fundec ~loc i =
+ let scope = Scope.empty and block = top_block fundec in
+ fst (build_instr ~scope ~loc ~block ~fundec (harden_instr i))
+ let cil_stmtkind ?into:fundec ~loc s =
+ let scope = Scope.empty and block = top_block fundec in
+ fst (build_stmtkind ~scope ~loc ~block ~fundec ~ghost:false (harden_stmt s))
+ let cil_stmt ?into:fundec ~loc s =
+ let scope = Scope.empty and block = top_block fundec in
+ fst (build_stmt ~scope ~loc ~block ~fundec ~ghost:false (harden_stmt s))
(* Operators *)
@@ -783,6 +992,9 @@ struct
let (:=) = assign
let (+=) lv e = assign lv (add lv e)
let (-=) lv e = assign lv (sub lv e)
+
+ let (let+) (var, stmt) f = stmt :: f var
+ let (and+) var1 var2 = (var1, var2)
end
@@ -790,14 +1002,7 @@ end
let dkey = Kernel.register_category "cil-builder"
-exception WrongContext of string
-
-module type T =
-sig
- val loc : Cil_types.location
-end
-
-module Stateful (Location : T) =
+module Stateful () =
struct
include Exp
@@ -809,6 +1014,7 @@ struct
type scope =
{
+ loc: Cil_types.location;
scope_type: scope_type;
ghost: bool;
mutable stmts: stmt list; (* In reverse order *)
@@ -817,25 +1023,26 @@ struct
and scope_type =
| Block
| IfThen of {ifthen_exp: Cil_types.exp}
- | IfThenElse of {ifthenelse_exp: Cil_types.exp; then_block: Cil_types.block}
+ | IfThenElse of {
+ ifthenelse_exp: Cil_types.exp;
+ then_block: Cil_types.block;
+ ghost_else: bool;
+ }
| Switch of {switch_exp: Cil_types.exp}
| Function of {fundec: Cil_types.fundec}
- let loc = Location.loc
-
-
(* Conversion to Cil *)
let build_instr_list l =
let rev_build_one acc = function
| Label _ | CilStmt _ | CilStmtkind _ ->
- raise (WrongContext "not convertible to instr")
+ error "the statement is not an instruction"
| CilInstr instr -> instr :: acc
in
List.fold_left rev_build_one [] l
- let build_stmt_list ~ghost l =
+ let build_stmt_list { loc ; ghost ; stmts } =
let rev_build_one acc = function
| Label l ->
begin match acc with
@@ -854,10 +1061,10 @@ struct
| CilInstr instr ->
Cil.mkStmt ~ghost (Cil_types.Instr instr) :: acc
in
- List.fold_left rev_build_one [] l
+ List.fold_left rev_build_one [] stmts
let build_block b =
- let block = Cil.mkBlock (build_stmt_list ~ghost:b.ghost b.stmts) in
+ let block = Cil.mkBlock (build_stmt_list b) in
block.Cil_types.blocals <- List.rev b.vars;
block
@@ -867,9 +1074,11 @@ struct
| Block ->
Cil_types.Block block
| IfThen { ifthen_exp } ->
- Cil_types.If (ifthen_exp, block, Cil.mkBlock [], loc)
- | IfThenElse { ifthenelse_exp; then_block } ->
- Cil_types.If (ifthenelse_exp, then_block, block, loc)
+ Cil_types.If (ifthen_exp, block, Cil.mkBlock [], b.loc)
+ | IfThenElse { ifthenelse_exp; then_block; ghost_else } ->
+ if ghost_else then
+ block.battrs <- [Cil_types.Attr (Cil.frama_c_ghost_else,[])];
+ Cil_types.If (ifthenelse_exp, then_block, block, b.loc)
| Switch { switch_exp } ->
let open Cil_types in
(* Cases are only allowed in the current block by the case function *)
@@ -877,9 +1086,9 @@ struct
List.exists (function Case _ -> true | _ -> false) stmt.labels
in
let case_stmts = List.filter contains_case block.bstmts in
- Cil_types.Switch (switch_exp, block, case_stmts , loc)
+ Cil_types.Switch (switch_exp, block, case_stmts , b.loc)
| Function _ ->
- raise (WrongContext "not convertible to stmtkind")
+ error "the function block is not convertible to Cil_types.stmtkind"
(* State management *)
@@ -891,12 +1100,12 @@ struct
let set_owner o =
if Option.is_some !owner then
- raise (WrongContext "already in a function");
+ error "already in a function context";
owner := Some o
let get_owner () =
match !owner with
- | None -> raise (WrongContext "function context not set")
+ | None -> error "function context not set"
| Some fundec -> fundec
@@ -916,15 +1125,15 @@ struct
let check_empty () =
if !stack <> [] then
- raise (WrongContext "some contextes have not been closed")
+ error "some contextes have not been closed: %t" pretty_stack !stack
let check_not_empty () =
if !stack = [] then
- raise (WrongContext "only a finish_* function can close all contextes")
+ error "only a finish_* function can close all contextes"
let top () =
match !stack with
- | [] -> raise (WrongContext "not in an opened context")
+ | [] -> error "not in an opened context"
| state :: _ -> state
let push state =
@@ -938,7 +1147,7 @@ struct
let pop () =
Kernel.debug ~dkey "pop from %t" pretty_stack;
match !stack with
- | [] -> raise (WrongContext "not in an opened context")
+ | [] -> error "not in an opened context"
| hd :: tail ->
stack := tail;
hd
@@ -946,9 +1155,9 @@ struct
let finish () =
reset_owner ();
match !stack with
- | [] -> raise (WrongContext "not in an opened context")
- | [b] -> b
- | _ :: _ :: _ -> raise (WrongContext "all contextes have not been closed")
+ | [] -> error "not in an opened context"
+ | [b] -> stack := []; b
+ | _ :: _ :: _ -> error "all contextes have not been closed"
let append_stmt b s =
b.stmts <- s :: b.stmts
@@ -961,6 +1170,11 @@ struct
fundec.Cil_types.slocals <- fundec.Cil_types.slocals @ [v];
b.vars <- v :: b.vars
+ let current_loc () =
+ match !stack with
+ | [] -> Cil_datatype.Location.unknown
+ | state :: _ -> state.loc
+
(* Statements *)
@@ -976,68 +1190,72 @@ struct
append_stmt b (CilStmtkind sk)
let break () =
+ let loc = current_loc () in
of_stmtkind (Cil_types.Break loc)
let return exp =
+ let loc = current_loc () in
of_stmtkind (Cil_types.Return (cil_exp_opt ~loc exp, loc))
(* Blocks *)
- let new_block ?(ghost=false) scope_type = {
- scope_type;
- ghost;
- stmts = [];
- vars = [];
- }
+ let new_block ?(loc=current_loc ()) ?(ghost=false) scope_type =
+ {
+ loc;
+ scope_type;
+ ghost;
+ stmts = [];
+ vars = [];
+ }
let extract_ifthen_block b =
match b.scope_type with
| IfThen {ifthen_exp} -> ifthen_exp
- | _ -> raise (WrongContext "not in an opened if-then-else context")
+ | _ -> error "not in an opened if-then-else context"
let extract_switch_block b =
match b.scope_type with
| Switch {switch_exp} -> switch_exp
- | _ -> raise (WrongContext "not in a opened switch context")
+ | _ -> error "not in a opened switch context"
let extract_function_block b =
match b.scope_type with
| Function {fundec} -> fundec
- | _ -> raise (WrongContext "not in a opened function context")
+ | _ -> error "not in a opened function context"
- let open_function ?ghost ?vorig_name name =
+ let open_function ?(loc=current_loc ()) ?ghost ?vorig_name name =
check_empty ();
let vorig_name = Option.value ~default:name vorig_name in
let fundec = Cil.emptyFunction vorig_name in
fundec.svar.vdecl <- loc;
fundec.svar.vname <- name;
set_owner fundec;
- push (new_block ?ghost (Function {fundec}));
- `var fundec.Cil_types.svar
+ push (new_block ~loc ?ghost (Function {fundec}));
+ `var (CilVar fundec.Cil_types.svar)
- let open_block ?into ?ghost () =
+ let open_block ?(loc=current_loc ()) ?into ?ghost () =
Option.iter set_owner into;
- push (new_block ?ghost Block)
+ push (new_block ~loc ?ghost Block)
- let open_ghost ?into () =
- open_block ?into ~ghost:true ()
+ let open_ghost ?(loc=current_loc ()) ?into () =
+ open_block ~loc ?into ~ghost:true ()
- let open_switch ?into exp =
+ let open_switch ?(loc=current_loc ()) ?into exp =
Option.iter set_owner into;
let switch_exp = cil_exp ~loc exp in
- push (new_block (Switch {switch_exp}))
+ push (new_block ~loc (Switch {switch_exp}))
- let open_if ?into exp =
+ let open_if ?(loc=current_loc ()) ?into exp =
Option.iter set_owner into;
let ifthen_exp = cil_exp ~loc exp in
- push (new_block (IfThen {ifthen_exp}))
+ push (new_block ~loc (IfThen {ifthen_exp}))
- let open_else () =
+ let open_else ?(ghost=false) () =
let b = pop () in
let ifthenelse_exp = extract_ifthen_block b in
let then_block = build_block b in
- push (new_block (IfThenElse {ifthenelse_exp; then_block}))
+ push (new_block (IfThenElse {ifthenelse_exp; then_block; ghost_else=ghost}))
let close () =
let above = pop () in
@@ -1048,7 +1266,7 @@ struct
let b = finish () in
match build_stmtkind b with
| Cil_types.Block b -> b
- | _ -> raise (WrongContext "not in an opened simple block context")
+ | _ -> error "not in an opened simple block context"
let finish_instr_list ?scope () =
let b = finish () in
@@ -1057,7 +1275,7 @@ struct
| Some block, vars ->
block.Cil_types.blocals <- List.rev vars @ block.Cil_types.blocals
| None, _ :: _ ->
- raise (WrongContext "a scope must be provided to insert local variables")
+ error "a scope must be provided to insert local variables"
end;
build_instr_list b.stmts
@@ -1074,12 +1292,12 @@ struct
vi.vdefined <- true;
vi.vghost <- b.ghost;
if register then begin
- Globals.Functions.replace_by_definition spec fundec loc;
+ Globals.Functions.replace_by_definition spec fundec b.loc;
let keepSwitch = Kernel.KeepSwitch.get () in
Cfg.prepareCFG ~keepSwitch fundec;
Cfg.cfgFun fundec;
end;
- GFun (fundec,loc)
+ GFun (fundec,b.loc)
let finish_declaration ?(register=true) () =
let b = finish () in
@@ -1087,17 +1305,18 @@ struct
let open Cil_types in
let vi = fundec.svar and spec = fundec.sspec in
if b.stmts <> [] then
- raise (WrongContext "there must not be any built statements");
+ error "there must not be any built statements";
vi.vdefined <- false;
vi.vghost <- b.ghost;
if register then begin
- Globals.Functions.replace_by_declaration spec vi loc;
+ Globals.Functions.replace_by_declaration spec vi b.loc;
end;
- GFunDecl (spec, vi, loc)
+ GFunDecl (spec, vi, b.loc)
let case exp =
let b = top () in
let _ = extract_switch_block b in
+ let loc = b.loc in
let label = Cil_types.Case (cil_exp ~loc exp, loc) in
append_stmt b (Label label)
@@ -1147,7 +1366,8 @@ struct
let assigns dests sources =
let open Cil_types in
let b = current_behavior ()
- and restyp = get_return_type () in
+ and restyp = get_return_type ()
+ and loc = current_loc () in
let map_source src =
match (src :> source) with
| #Exp.exp as e ->
@@ -1170,13 +1390,15 @@ struct
let requires pred =
let open Cil_types in
let b = current_behavior ()
- and restyp = get_return_type () in
+ and restyp = get_return_type ()
+ and loc = current_loc () in
b.b_requires <- b.b_requires @ [cil_ipred ~loc ~restyp pred]
let ensures pred =
let open Cil_types in
let b = current_behavior ()
- and restyp = get_return_type () in
+ and restyp = get_return_type ()
+ and loc = current_loc () in
b.b_post_cond <- b.b_post_cond @ [Normal, cil_ipred ~loc ~restyp pred]
@@ -1185,6 +1407,7 @@ struct
let local' ?(ghost=false) ?init typ name =
let fundec = get_owner () and b = top () in
let ghost = ghost || b.ghost in
+ let loc = current_loc () in
let v = Cil.makeLocalVar ~insert:false ~ghost ~loc fundec name typ in
begin match init with
| None -> ()
@@ -1194,27 +1417,41 @@ struct
v.vdefined <- true
end;
append_local v;
- `var v
+ `var (CilVar v)
let local ?ghost ?init ty name =
let init = Option.map (values ty) init in
local' ?ghost ?init (cil_typ ty) name
- let local_copy ?(ghost=false) ?(suffix="_tmp") (`var vi) =
+ let local_copy ?(ghost=false) ?(suffix="_tmp") v =
+ let name, typ, vi =
+ match harden_var v with
+ | NewVar (_id, name, typ) -> name, typ, None
+ | CilVar vi -> vi.vname, vi.vtype, Some vi
+ in
+ let name = name ^ suffix in
let fundec = get_owner () and b = top () in
let ghost = ghost || b.ghost in
- let v = Cil.copyVarinfo vi (vi.Cil_types.vname ^ suffix) in
+ let v =
+ match vi with
+ | None ->
+ let temp = false and global = false and formal = false in
+ Cil.makeVarinfo ~temp ~ghost global formal name typ
+ | Some vi ->
+ Cil.copyVarinfo vi name
+ in
v.vghost <- v.vghost || ghost;
Cil.refresh_local_name fundec v;
append_local v;
- `var v
+ `var (CilVar v)
let parameter ?(ghost=false) ?(attributes=[]) typ name =
let fundec = get_owner () and b = top () in
let ghost = ghost || b.ghost in
+ let loc = current_loc () in
let v = Cil.makeFormalVar ~ghost ~loc fundec name typ in
v.Cil_types.vattr <- attributes;
- `var v
+ `var (CilVar v)
(* Instructions *)
@@ -1224,6 +1461,7 @@ struct
append_instr b i
let assign lval exp =
+ let loc = current_loc () in
let lval' = cil_lval ~loc lval
and exp' = cil_exp ~loc exp in
of_instr (Cil_types.Set (lval', exp', loc))
@@ -1232,17 +1470,22 @@ struct
assign lval (add lval (of_int 1))
let call dest callee args =
+ let loc = current_loc () in
let dest' = cil_lval_opt ~loc dest
and callee' = cil_exp ~loc callee
and args' = cil_exp_list ~loc args in
of_instr (Cil_types.Call (dest', callee', args', loc))
let pure exp =
+ let loc = current_loc () in
let exp' = cil_exp ~loc exp in
- let `var v = local' (Cil.typeOf exp') "tmp" ~init:(Exp.of_exp exp') in
- v.vdescr <- Some (Format.asprintf "%a" !Cil.pp_exp_ref exp')
+ match local' (Cil.typeOf exp') "tmp" ~init:(Exp.of_exp exp') with
+ | `var (CilVar v) ->
+ v.vdescr <- Some (Format.asprintf "%a" !Cil.pp_exp_ref exp')
+ | _ -> assert false
let skip () =
+ let loc = current_loc () in
of_instr (Cil_types.Skip (loc))
diff --git a/src/kernel_services/ast_building/cil_builder.mli b/src/kernel_services/ast_building/cil_builder.mli
index 30d69d5165fb1d372b9cff7fb8058e675ede1a20..7027e5475ba3c3d171747a280d0fd66baccb7ec5 100644
--- a/src/kernel_services/ast_building/cil_builder.mli
+++ b/src/kernel_services/ast_building/cil_builder.mli
@@ -57,6 +57,8 @@ sig
val ptr : ('v,'s) typ -> ('v,'v) typ
val array : ?size:int -> ('v,'s) typ -> ('v,'s list) typ
+ val structure :
+ Cil_types.compinfo -> (Cil_types.fieldinfo -> 'a -> 'v) -> ('v, 'a) typ
(* Attributes *)
val attribute : ('v,'s) typ -> string -> Cil_types.attrparam list
@@ -122,6 +124,7 @@ sig
val of_exp : Cil_types.exp -> [> exp]
val of_exp_copy : Cil_types.exp -> [> exp]
+ val of_exp_list : Cil_types.exp list -> [> exp] list
val unop : Cil_types.unop -> [< exp] -> [> exp]
val neg : [< exp] -> [> exp]
val lognot : [< exp] -> [> exp]
@@ -177,7 +180,6 @@ sig
val compound : Cil_types.typ -> init list -> [> init]
val values : (init,'values) typ -> 'values -> init
-
(* Redefined operators *)
val (+) : [< exp] -> [< exp] -> [> exp]
@@ -194,6 +196,7 @@ sig
val (==) : [< exp] -> [< exp] -> [> exp]
val (!=) : [< exp] -> [< exp] -> [> exp]
val (--) : [< exp] -> [< exp] -> [> exp]
+ val (.@[]) : [< lval] -> [< exp] -> [> exp] (* C index operator [] *)
(* Export CIL objects from built expressions *)
@@ -203,6 +206,7 @@ sig
exception NotAPredicate of exp
exception NotAFunction of Cil_types.logic_info
exception Typing_error of string
+ exception OutOfScope of string
val cil_logic_label : label -> Cil_types.logic_label
val cil_constant : [< const] -> Cil_types.constant
@@ -244,18 +248,38 @@ sig
val incr : [< lval] -> [> instr]
val call : [< lval | `none] -> [< exp] -> [< exp] list -> [> instr]
+ val local : ?ghost:bool -> ?init:'v -> (init,'v) typ -> string ->
+ [> var] * [> instr]
+ val local' : ?ghost:bool -> ?init:init -> Cil_types.typ -> string ->
+ [> var] * [> instr]
+ val local_copy : ?ghost:bool -> ?suffix:string -> [< var] ->
+ [> var] * [> instr]
+
(* Statements *)
val of_stmtkind : Cil_types.stmtkind -> [> stmt]
val of_stmt : Cil_types.stmt -> [> stmt]
val of_stmts : Cil_types.stmt list -> [> stmt]
val block : [< stmt] list -> [> stmt]
+ val sequence : [< stmt] list -> [> stmt] (* does not generate block *)
val ghost : [< stmt] -> [> stmt]
+ val if_ : ?ghost_else:bool ->
+ [< exp] -> then_:[< stmt] list -> else_:[< stmt] list -> [> stmt]
- val cil_instr : loc:Cil_types.location -> instr -> Cil_types.instr
- val cil_stmtkind : loc:Cil_types.location -> stmt -> Cil_types.stmtkind
- val cil_stmt : loc:Cil_types.location -> stmt -> Cil_types.stmt
+ (* Conversion to Cil *)
+
+ (* for the three following function into is mandatory if the built ast
+ contains locals declarations *)
+ val cil_instr : ?into:Cil_types.fundec ->
+ loc:Cil_types.location -> instr -> Cil_types.instr
+ val cil_stmtkind : ?into:Cil_types.fundec ->
+ loc:Cil_types.location -> stmt -> Cil_types.stmtkind
+ val cil_stmt : ?into:Cil_types.fundec ->
+ loc:Cil_types.location -> stmt -> Cil_types.stmt
(* Operators *)
+ val (let+) : var * stmt -> (var -> stmt list) -> stmt list
+ val (and+) : var -> var -> var * var
+
val (:=) : [< lval] -> [< exp] -> [> instr] (* assign *)
val (+=) : [< lval] -> [< exp] -> [> instr]
val (-=) : [< lval] -> [< exp] -> [> instr]
@@ -264,19 +288,23 @@ end
(* --- Stateful builder --- *)
-exception WrongContext of string
-
-module type T =
-sig
- val loc : Cil_types.location
-end
+exception BuildError of string
-module Stateful (Location : T) :
+module Stateful () :
sig
include module type of Exp
+ with type ('v,'s) typ = ('v,'s) Type.typ
+ and type const' = Exp.const'
+ and type var' = Exp.var'
+ and type lval' = Exp.lval'
+ and type exp' = Exp.exp'
+ and type init' = Exp.init'
+ and type label = Exp.label
(* Functions *)
- val open_function : ?ghost:bool -> ?vorig_name:string -> string -> [> var]
+ val open_function :
+ ?loc:Cil_types.location -> ?ghost:bool -> ?vorig_name:string ->
+ string -> [> var]
val set_return_type : ('s,'v) typ -> unit
val set_return_type' : Cil_types.typ -> unit
val add_attribute : Cil_types.attribute -> unit
@@ -296,11 +324,19 @@ sig
val of_stmtkind : Cil_types.stmtkind -> unit
val of_stmt : Cil_types.stmt -> unit
val of_stmts : Cil_types.stmt list -> unit
- val open_block : ?into:Cil_types.fundec -> ?ghost:bool -> unit -> unit
- val open_ghost : ?into:Cil_types.fundec -> unit -> unit
- val open_switch : ?into:Cil_types.fundec -> [< exp] -> unit
- val open_if : ?into:Cil_types.fundec -> [< exp] -> unit
- val open_else : unit -> unit
+ val open_block :
+ ?loc:Cil_types.location -> ?into:Cil_types.fundec -> ?ghost:bool ->
+ unit -> unit
+ val open_ghost :
+ ?loc:Cil_types.location -> ?into:Cil_types.fundec ->
+ unit -> unit
+ val open_switch :
+ ?loc:Cil_types.location -> ?into:Cil_types.fundec ->
+ [< exp] -> unit
+ val open_if :
+ ?loc:Cil_types.location -> ?into:Cil_types.fundec ->
+ [< exp] -> unit
+ val open_else : ?ghost:bool -> unit -> unit
val close : unit -> unit
val finish_block : unit -> Cil_types.block
val finish_instr_list : ?scope:Cil_types.block -> unit -> Cil_types.instr list
diff --git a/src/plugins/variadic/builder.ml b/src/plugins/variadic/builder.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3ae49a9946778b6bb9bdc6106fbb3ab759592be6
--- /dev/null
+++ b/src/plugins/variadic/builder.ml
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* A Builder.S module is a stateful module that
+ 1. extends Cil_builder.Stateful which already contains building utilities and
+ 2. stores the current state of the building process with instructions,
+ variables and globals that remains to be added to the AST. It . *)
+
+module type S =
+sig
+ include (module type of Cil_builder.Stateful ())
+
+ (* The loc of the call being translated *)
+ val loc : Cil_types.location
+
+ (* These two following function stores the built global for later addition
+ to the AST *)
+ val finish_function : unit -> unit
+ val finish_declaration : unit -> unit
+
+ (** Start the translation of the call. Call this before declaring variables
+ or inserting statements. *)
+ val start_translation : unit -> unit
+ (* Build a call or a Local_init with constructor depending on the currently
+ translated instruction *)
+ val translated_call : [< exp] -> [< exp] list -> unit
+end
+
+type t = (module S)
diff --git a/src/plugins/variadic/generic.ml b/src/plugins/variadic/generic.ml
index ccebe30ee1bd538471b9a7a63cf6e699ad397776..91ef3f8f89201b1717172d37e531222dfb834ca8 100644
--- a/src/plugins/variadic/generic.ml
+++ b/src/plugins/variadic/generic.ml
@@ -136,7 +136,10 @@ let translate_va_builtin caller inst =
(* Translation of calls to variadic functions *)
-let translate_call ~fundec ~ghost block loc mk_call callee pars =
+let translate_call ~builder callee pars =
+ let module Build = (val builder : Builder.S) in
+ Build.start_translation ();
+
(* Log translation *)
Self.result ~current:true ~level:2
"Generic translation of call to variadic function.";
@@ -148,10 +151,6 @@ let translate_call ~fundec ~ghost block loc mk_call callee pars =
let variadic_size = (List.length r_exps) - (List.length g_params) in
let v_exps, g_exps = List.break variadic_size r_exps in
- (* Start build *)
- let module Build = Cil_builder.Stateful (struct let loc = loc end) in
- Build.open_block ~into:fundec ~ghost ();
-
(* Create temporary variables to hold parameters *)
let add_var i e =
let name = "__va_arg" ^ string_of_int i in
@@ -161,14 +160,13 @@ let translate_call ~fundec ~ghost block loc mk_call callee pars =
(* Build an array to store addresses *)
let init = match vis with (* C standard forbids arrays of size 0 *)
- | [] -> [Build.of_init (Cil.makeZeroInit ~loc Cil.voidPtrType)]
+ | [] -> [Build.(of_init (Cil.makeZeroInit ~loc Cil.voidPtrType))]
| l -> List.map Build.addr l
in
let ty = Build.(array (ptr void) ~size:(List.length init)) in
let vargs = Build.(local ty "__va_args" ~init) in
(* Translate the call *)
- let new_arg = Build.(cil_exp ~loc (cast' (vpar_typ []) (addr vargs))) in
- let new_args = (s_exps @ [new_arg] @ g_exps) in
- Build.of_instr (mk_call callee new_args);
- Build.finish_instr_list ~scope:block ()
+ let new_arg = Build.(cast' (vpar_typ []) (addr vargs)) in
+ let new_args = Build.(of_exp_list s_exps @ [new_arg] @ of_exp_list g_exps) in
+ Build.(translated_call (of_exp callee) new_args)
diff --git a/src/plugins/variadic/generic.mli b/src/plugins/variadic/generic.mli
index 0aa62b46738d81bf7dafaf1c748e453f7dcb758d..a14cc0183a9e5f018db85f63ef2dc94526bf9d64 100644
--- a/src/plugins/variadic/generic.mli
+++ b/src/plugins/variadic/generic.mli
@@ -30,12 +30,9 @@ val translate_type : Cil_types.typ -> Cil_types.typ
val add_vpar : Cil_types.varinfo -> unit
(* Translation of va_* builtins *)
-val translate_va_builtin : Cil_types.fundec -> Cil_types.instr ->
- Cil_types.instr list
+val translate_va_builtin :
+ Cil_types.fundec -> Cil_types.instr -> Cil_types.instr list
(* Generic translation of calls *)
-val translate_call : fundec:Cil_types.fundec -> ghost:bool ->
- Cil_types.block -> Cil_types.location ->
- (Cil_types.exp -> Cil_types.exp list -> Cil_types.instr) ->
- Cil_types.exp -> Cil_types.exp list ->
- Cil_types.instr list
+val translate_call :
+ builder:Builder.t -> Cil_types.exp -> Cil_types.exp list -> unit
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index f133c2ed8ea71781042f084531aa05ba2a77d080..8733877def3bb374bf902cdfccb60efcbc396b98 100644
--- a/src/plugins/variadic/standard.ml
+++ b/src/plugins/variadic/standard.ml
@@ -26,8 +26,6 @@ open Options
module List = Extends.List
module Typ = Extends.Typ
-type call_builder = Cil_types.exp -> Cil_types.exp list -> Cil_types.instr
-
let pp_prototype name fmt tparams =
Format.fprintf fmt "%s(%a)"
name
@@ -38,8 +36,6 @@ let pp_overload name fmt l =
Pretty_utils.pp_list ~sep:"@\n" (pp_prototype name) fmt prototypes
-let new_globals : (global list) ref = ref []
-
(* State to store the number of fallback functions generated for a particular
function name. This number is used to generate a unique function name. *)
module Fallback_counts =
@@ -169,73 +165,66 @@ let match_args ~callee tparams args =
(* translate a call by applying argument matching/pruning and changing
callee *)
-let match_call ~loc ~fundec scope mk_call new_callee new_tparams args =
+let match_call ~builder new_callee new_tparams args =
+ let module Build = (val builder : Builder.S) in
+
let new_args, unused_args = match_args ~callee:new_callee new_tparams args in
- let call = mk_call (Cil.evar ~loc new_callee) new_args in
- let reads =
- List.map (fun e -> Cil.mkPureExprInstr ~fundec ~scope e) unused_args
- in
- reads @ [call]
+ Build.start_translation ();
+ Build.(List.iter pure (of_exp_list unused_args));
+ Build.(translated_call (var new_callee) (of_exp_list new_args))
(* ************************************************************************ *)
(* Fallback calls *)
(* ************************************************************************ *)
-let fallback_fun_call ~callee loc mk_call vf args =
- let build_fallback_fun ~vf args =
- let module Build =
- Cil_builder.Stateful (struct let loc = vf.vf_decl.vdecl end)
- in
+let fallback_fun_call ~builder ~callee vf args =
+ let module Build = (val builder : Builder.S) in
- (* Choose function name *)
- let name = callee.vname in
- let vorig_name = callee.vorig_name in
- let count =
- try Fallback_counts.find name
- with Not_found -> 0
- in
- let count = count + 1 in
- Fallback_counts.replace name count;
- let new_name = name ^ "_fallback_" ^ (string_of_int count) in
-
- (* Start building the function *)
- let funvar = Build.open_function ~vorig_name new_name in
-
- (* Set function return type and attributes *)
- let ret_typ, params, _, attrs = Cil.splitFunctionType vf.vf_original_type in
- Build.set_return_type' ret_typ;
- List.iter Build.add_attribute attrs;
- Build.add_stdlib_generated ();
-
- (* Add parameters *)
- let fixed_params_count = Typ.params_count vf.vf_original_type in
- let add_static_param (name,typ,attributes) =
- ignore (Build.parameter ~attributes typ name)
- and add_variadic_param i e =
- let typ = Cil.typeOf e in
- ignore (Build.parameter typ ("param" ^ string_of_int i))
- in
- List.iter add_static_param (Option.get params);
- List.iteri add_variadic_param (List.drop fixed_params_count args);
+ (* Choose function name *)
+ let name = callee.vname in
+ let vorig_name = callee.vorig_name in
+ let count =
+ try Fallback_counts.find name
+ with Not_found -> 0
+ in
+ let count = count + 1 in
+ Fallback_counts.replace name count;
+ let new_name = name ^ "_fallback_" ^ (string_of_int count) in
+
+ (* Start building the function *)
+ let loc = vf.vf_decl.vdecl in
+ let new_callee = Build.open_function ~loc ~vorig_name new_name in
+
+ (* Set function return type and attributes *)
+ let ret_typ, params, _, attrs = Cil.splitFunctionType vf.vf_original_type in
+ Build.set_return_type' ret_typ;
+ List.iter Build.add_attribute attrs;
+ Build.add_stdlib_generated ();
- (* Build the default behaviour *)
- let glob = Build.finish_declaration ~register:false () in
- glob, Build.cil_varinfo funvar
+ (* Add parameters *)
+ let fixed_params_count = Typ.params_count vf.vf_original_type in
+ let add_static_param (name,typ,attributes) =
+ ignore (Build.parameter ~attributes typ name)
+ and add_variadic_param i e =
+ let typ = Cil.typeOf e in
+ ignore (Build.parameter typ ("param" ^ string_of_int i))
in
+ List.iter add_static_param (Option.get params);
+ List.iteri add_variadic_param (List.drop fixed_params_count args);
- (* Create the new callee *)
- let glob, new_callee = build_fallback_fun ~vf args in
- new_globals := glob :: !new_globals;
+ (* Build the default behaviour *)
+ Build.finish_declaration ();
(* Store the translation *)
- Replacements.add new_callee vf.vf_decl;
+ Replacements.add (Build.cil_varinfo new_callee) vf.vf_decl;
(* Translate the call *)
+ Build.start_translation ();
Self.result ~current:true ~level:2
- "Fallback translation of call %s to a call to the specialized version %s."
- vf.vf_decl.vorig_name new_callee.vname;
- let call = mk_call (Cil.evar ~loc new_callee) args in
- [call]
+ "Fallback translation of call %s to a call to the specialized version %a."
+ vf.vf_decl.vorig_name Build.pretty new_callee;
+ Build.(translated_call new_callee (List.map of_exp args))
+
(* ************************************************************************ *)
(* Aggregator calls *)
@@ -245,7 +234,9 @@ let find_null exp_list =
List.ifind (fun e -> Cil.isZero (Cil.constFold false e)) exp_list
-let aggregator_call ~fundec ~ghost aggregator scope loc mk_call vf args =
+let aggregator_call ~builder aggregator vf args =
+ let module Build = (val builder : Builder.S) in
+
let {a_target; a_pos; a_type; a_param} = aggregator in
let name = vf.vf_decl.vorig_name
and tparams = Typ.params_types a_target.vtype
@@ -289,19 +280,17 @@ let aggregator_call ~fundec ~ghost aggregator scope loc mk_call vf args =
name a_target.vorig_name;
let pname = if pname = "" then "param" else pname in
- let module Build = Cil_builder.Stateful (struct let loc = loc end) in
- Build.open_block ~into:fundec ~ghost ();
+ Build.start_translation ();
let init = match args_middle with (* C standard forbids arrays of size 0 *)
- | [] -> [Build.of_init (Cil.makeZeroInit ~loc ptyp)]
+ | [] -> [Build.(of_init (Cil.makeZeroInit ~loc ptyp))]
| l -> List.map Build.of_exp l
in
let size = List.length init in
let vaggr = Build.(local (array ~size (of_ctyp ptyp)) pname ~init) in
let new_args = args_left @ [Build.(cil_exp ~loc (addr vaggr))] @ args_right in
let new_args,_ = match_args ~callee:vf.vf_decl tparams new_args in
- Build.(List.iter pure (List.map of_exp unused_args));
- Build.of_instr (mk_call (Cil.evar ~loc a_target) new_args);
- Build.finish_instr_list ~scope ()
+ Build.(List.iter pure (of_exp_list unused_args));
+ Build.(translated_call (var a_target) (of_exp_list new_args))
(* ************************************************************************ *)
@@ -338,7 +327,7 @@ let filter_matching_prototypes overload args =
List.filter check overload
-let overloaded_call ~fundec overload block loc mk_call vf args =
+let overloaded_call ~builder overload vf args =
let name = vf.vf_decl.vorig_name in
(* Find the matching prototype *)
@@ -372,7 +361,7 @@ let overloaded_call ~fundec overload block loc mk_call vf args =
Self.result ~current:true ~level:2
"Translating call to the specialized version %a."
(pp_prototype name) tparams;
- match_call ~loc ~fundec block mk_call new_callee tparams args
+ match_call ~builder new_callee tparams args
@@ -443,11 +432,9 @@ let format_length typ =
find_predicate_by_width typ "format_length" "wformat_length"
-let build_specialized_fun env vf format_fun tvparams =
+let build_specialized_fun ~builder env vf format_fun tvparams =
let open Format_types in
- let module Build =
- Cil_builder.Stateful (struct let loc = vf.vf_decl.vdecl end)
- in
+ let module Build = (val builder : Builder.S) in
(* Choose function name *)
let name = vf.vf_decl.vorig_name in
@@ -455,7 +442,8 @@ let build_specialized_fun env vf format_fun tvparams =
let new_name = name ^ "_va_" ^ (string_of_int vf.vf_specialization_count) in
(* Start building the function *)
- let funvar = Build.open_function ~vorig_name:name new_name in
+ let loc = vf.vf_decl.vdecl in
+ let funvar = Build.open_function ~loc ~vorig_name:name new_name in
(* Set function return type and attributes *)
let ret_typ, params, _, attrs = Cil.splitFunctionType vf.vf_original_type in
@@ -612,8 +600,8 @@ let build_specialized_fun env vf format_fun tvparams =
Build.assigns !dests !sources;
(* Build the default behaviour *)
- let glob = Build.finish_declaration ~register:false () in
- glob, Build.cil_varinfo funvar
+ Build.finish_declaration ();
+ Build.cil_varinfo funvar
(* --- Call translation --- *)
@@ -720,7 +708,7 @@ let infer_format_from_args vf format_fun args =
| PrintfLike -> Format_types.FFormat (List.map f_format format)
| ScanfLike -> Format_types.SFormat (List.map s_format format)
-let format_fun_call ~fundec env format_fun scope loc mk_call vf args =
+let format_fun_call ~builder env format_fun vf args =
(* Extract the format if possible *)
let format =
try
@@ -754,8 +742,7 @@ let format_fun_call ~fundec env format_fun scope loc mk_call vf args =
in
(* Create the new callee *)
- let glob, new_callee = build_specialized_fun env vf format_fun tvparams in
- new_globals := glob :: !new_globals;
+ let new_callee = build_specialized_fun ~builder env vf format_fun tvparams in
(* Store the translation *)
Replacements.add new_callee vf.vf_decl;
@@ -765,4 +752,4 @@ let format_fun_call ~fundec env format_fun scope loc mk_call vf args =
"Translating call to %s to a call to the specialized version %s."
vf.vf_decl.vorig_name new_callee.vname;
let tparams = Typ.params_types new_callee.vtype in
- match_call ~loc ~fundec scope mk_call new_callee tparams args
+ match_call ~builder new_callee tparams args
diff --git a/src/plugins/variadic/standard.mli b/src/plugins/variadic/standard.mli
index 27b7a6e1bc5a76719031829dd6276b05f4feedff..6b4eabea06d55b7a9ccbc3628fdffb8c33872f32 100644
--- a/src/plugins/variadic/standard.mli
+++ b/src/plugins/variadic/standard.mli
@@ -20,28 +20,24 @@
(* *)
(**************************************************************************)
-(* Ugly ref *)
-val new_globals : (Cil_types.global list) ref
-
-type call_builder = Cil_types.exp -> Cil_types.exp list -> Cil_types.instr
-
exception Translate_call_exn of Cil_types.varinfo
-val fallback_fun_call : callee:Cil_types.varinfo -> Cil_types.location ->
- call_builder -> Va_types.variadic_function -> Cil_types.exp list ->
- Cil_types.instr list
+val fallback_fun_call :
+ builder:Builder.t -> callee:Cil_types.varinfo ->
+ Va_types.variadic_function -> Cil_types.exp list -> unit
-val aggregator_call : fundec:Cil_types.fundec -> ghost:bool ->
- Va_types.aggregator -> Cil_types.block -> Cil_types.location ->
- call_builder -> Va_types.variadic_function -> Cil_types.exp list ->
- Cil_types.instr list
+val aggregator_call :
+ builder:Builder.t ->
+ Va_types.aggregator ->
+ Va_types.variadic_function -> Cil_types.exp list -> unit
-val overloaded_call : fundec:Cil_types.fundec -> Va_types.overload ->
- Cil_types.block -> Cil_types.location -> call_builder ->
- Va_types.variadic_function -> Cil_types.exp list ->
- Cil_types.instr list
+val overloaded_call :
+ builder:Builder.t ->
+ Va_types.overload ->
+ Va_types.variadic_function -> Cil_types.exp list -> unit
-val format_fun_call : fundec:Cil_types.fundec -> Environment.t ->
- Va_types.format_fun -> Cil_types.block -> Cil_types.location ->
- call_builder -> Va_types.variadic_function -> Cil_types.exp list ->
- Cil_types.instr list
+val format_fun_call :
+ builder:Builder.t ->
+ Environment.t ->
+ Va_types.format_fun ->
+ Va_types.variadic_function -> Cil_types.exp list -> unit
diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml
index b20d67e253d474a9d4e0256452843014b763c64e..726274ac3398d651807447cc0efa4ab5a2f6f851 100644
--- a/src/plugins/variadic/translate.ml
+++ b/src/plugins/variadic/translate.ml
@@ -77,7 +77,8 @@ let translate_variadics (file : file) =
let v = object (self)
inherit Cil.nopCilVisitor
- val curr_block = Stack.create ()
+ val curr_block = Stack.create () (* Opened blocks to store generated locals *)
+ val mutable pending_globals = [] (* List of globals to add before the current global once it's finished visiting *)
method! vblock b =
Stack.push b curr_block;
@@ -87,6 +88,31 @@ let translate_variadics (file : file) =
try Stack.top curr_block
with Stack.Empty -> Options.Self.fatal "No enclosing block here"
+ method private make_builder ~loc ~fundec ~ghost ~mk_call =
+ let module B =
+ struct
+ include Cil_builder.Stateful ()
+
+ let loc = loc
+
+ let finish_function () =
+ pending_globals <- finish_function () :: pending_globals
+
+ let finish_declaration () =
+ pending_globals <-
+ finish_declaration ~register:false () :: pending_globals
+
+ let start_translation () =
+ open_block ~loc ~into:fundec ~ghost ()
+
+ let translated_call callee args =
+ of_instr
+ (mk_call (cil_exp ~loc callee) (List.map (cil_exp ~loc) args))
+ end
+ in
+ (module B : Builder.S)
+
+
method! vtype _typ =
Cil.DoChildrenPost (Generic.translate_type)
@@ -109,9 +135,9 @@ let translate_variadics (file : file) =
Generic.add_vpar vi;
fundec.sformals <- Cil.getFormalsDecl vi;
end;
- Standard.new_globals := [];
+ pending_globals <- [];
Cil.DoChildrenPost (fun globs ->
- List.rev (globs @ !Standard.new_globals))
+ List.rev_append pending_globals globs)
| _ ->
Cil.DoChildren
@@ -160,35 +186,48 @@ let translate_variadics (file : file) =
let loc = Cil_datatype.Instr.loc i in
let block = self#enclosing_block () in
let ghost = (Option.get self#current_stmt).ghost in
- let make_new_args mk_call f args =
+ let translate_call mk_call translator args =
+ File.must_recompute_cfg fundec;
+ let builder = self#make_builder ~loc ~fundec ~ghost ~mk_call in
+ translator ~builder args;
+ let module Builder = (val builder : Builder.S) in
+ Builder.finish_instr_list ~scope:block ()
+ in
+ let mk_translator f =
let vf = Table.find classification f in
- try begin
- match vf.vf_class with
- | Overload o -> Standard.overloaded_call ~fundec o block loc mk_call vf args
- | Aggregator a -> Standard.aggregator_call ~fundec ~ghost a block loc mk_call vf args
- | FormatFun f -> Standard.format_fun_call ~fundec env f block loc mk_call vf args
- | Builtin ->
- Self.result ~level:2 ~current:true
- "Call to variadic builtin %s left untransformed." f.vname;
- raise Not_found
- | _ ->
- Generic.translate_call
- ~fundec ~ghost block loc mk_call (Cil.evar ~loc f) args
- end with Standard.Translate_call_exn callee ->
- Standard.fallback_fun_call ~callee loc mk_call vf args
+ let cover_failure f =
+ fun ~builder args ->
+ try
+ f ~builder args
+ with Standard.Translate_call_exn callee ->
+ Standard.fallback_fun_call ~callee ~builder vf args
+ in
+ match vf.vf_class with
+ | Overload o -> cover_failure (Standard.overloaded_call o vf)
+ | Aggregator a -> cover_failure (Standard.aggregator_call a vf)
+ | FormatFun f -> cover_failure (Standard.format_fun_call env f vf)
+ | Builtin ->
+ Self.result ~level:2 ~current:true
+ "Call to variadic builtin %s left untransformed." f.vname;
+ raise Not_found
+ | _ ->
+ Generic.translate_call (Cil.evar ~loc f)
in
begin match i with
+ (* Translate builtins *)
| Call(_, {enode = Lval(Var vi, _)}, _, _)
when Classify.is_va_builtin vi.vname ->
File.must_recompute_cfg fundec;
Cil.ChangeTo (Generic.translate_va_builtin fundec i)
+
+ (* Translate variadic calls *)
| Call(lv, {enode = Lval(Var vi, NoOffset)}, args, loc) ->
begin
try
let mk_call f args = Call (lv, f, args, loc) in
- let res = make_new_args mk_call vi args in
- File.must_recompute_cfg fundec;
- Cil.ChangeTo res
+ let translator = mk_translator vi in
+ let instr_list = translate_call mk_call translator args in
+ Cil.ChangeTo instr_list
with Not_found ->
Cil.DoChildren
end
@@ -199,20 +238,12 @@ let translate_variadics (file : file) =
in
if is_variadic then begin
let mk_call f args = Call (lv, f, args, loc) in
- let res =
- Generic.translate_call
- ~fundec
- ~ghost
- block
- loc
- mk_call
- callee
- args
- in
- File.must_recompute_cfg fundec;
- Cil.ChangeTo res
+ let translator = Generic.translate_call callee in
+ let instr_list = translate_call mk_call translator args in
+ Cil.ChangeTo instr_list
end else
Cil.DoChildren
+
| Local_init(v, ConsInit(c, args, kind), loc) ->
begin
try
@@ -240,9 +271,9 @@ let translate_variadics (file : file) =
| Plain_func -> args
| Constructor -> Cil.mkAddrOfVi v :: args
in
- let res = make_new_args mk_call c args in
- File.must_recompute_cfg fundec;
- Cil.ChangeTo res
+ let translator = mk_translator c in
+ let instr_list = translate_call mk_call translator args in
+ Cil.ChangeTo instr_list
with Not_found ->
Cil.DoChildren
end
diff --git a/tests/misc/cil_builder.i b/tests/misc/cil_builder.i
new file mode 100644
index 0000000000000000000000000000000000000000..3dde1fd899ccfcdb05f414528b4a0c5fc6ded365
--- /dev/null
+++ b/tests/misc/cil_builder.i
@@ -0,0 +1,8 @@
+/* run.config
+MODULE: @PTEST_NAME@
+ OPT:
+*/
+
+void main(void) {
+ // This will be filled by the OCaml Module
+}
diff --git a/tests/misc/cil_builder.ml b/tests/misc/cil_builder.ml
new file mode 100644
index 0000000000000000000000000000000000000000..571edd890e7d77048cac3fd1376645a59e2eab64
--- /dev/null
+++ b/tests/misc/cil_builder.ml
@@ -0,0 +1,21 @@
+module Build = Cil_builder.Pure
+
+let run () =
+ let kf, _ = Globals.entry_point () in
+ let stmt = Kernel_function.find_first_stmt kf in
+ let loc = Kernel_function.get_location kf in
+ let into = Kernel_function.get_definition kf in
+ stmt.skind <- Build.(
+ cil_stmtkind ~into ~loc @@ sequence @@
+ let+ i = local int "x" in [
+ i := (of_int 1);
+ if_ (i < of_int 3)
+ ~then_:[incr i]
+ ~else_:[i := zero]
+ ]
+ );
+ Kernel.result "%a" Printer.pp_file (Ast.get ())
+
+
+let () =
+ Db.Main.extend run
diff --git a/tests/misc/oracle/cil_builder.res.oracle b/tests/misc/oracle/cil_builder.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c4f1e7ee9c3cce168d6ce7be2a79e3925cc4174d
--- /dev/null
+++ b/tests/misc/oracle/cil_builder.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing cil_builder.i (no preprocessing)
+[kernel] /* Generated by Frama-C */
+ void main(void)
+ {
+ {
+ int x;
+ x = 1;
+ if (x < 3) x ++; else x = 0;
+ }
+ }