diff --git a/Makefile b/Makefile
index 7f7d6c9d99545f4713c0c6040965cdfd3daed406..5b1cb6057283e4c4e9203c1df0dcab604e48bc4f 100644
--- a/Makefile
+++ b/Makefile
@@ -302,6 +302,7 @@ DISTRIB_FILES:=\
$(wildcard src/kernel_internals/typing/*.ml*) \
$(wildcard src/kernel_services/ast_data/*.ml*) \
$(wildcard src/kernel_services/ast_queries/*.ml*) \
+ $(wildcard src/kernel_services/ast_building/*.ml*) \
$(wildcard src/kernel_services/ast_printing/*.ml*) \
$(wildcard src/kernel_services/cmdline_parameters/*.ml*) \
$(wildcard src/kernel_services/analysis/*.ml*) \
@@ -627,7 +628,8 @@ KERNEL_CMO=\
src/kernel_services/ast_transformations/filter.cmo \
src/kernel_services/ast_transformations/inline.cmo \
src/kernel_internals/runtime/special_hooks.cmo \
- src/kernel_internals/runtime/messages.cmo
+ src/kernel_internals/runtime/messages.cmo \
+ src/kernel_services/ast_building/cil_builder.cmo \
CMO += $(KERNEL_CMO)
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index a201e0f32e7a5d6c5491bb2f1e97396c84fe0add..afdc2161a96bc21aafe417e4a274eb10f7069b4a 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -493,6 +493,8 @@ src/kernel_services/analysis/undefined_sequence.ml: CEA_LGPL
src/kernel_services/analysis/undefined_sequence.mli: CEA_LGPL
src/kernel_services/analysis/wto_statement.ml: CEA_LGPL
src/kernel_services/analysis/wto_statement.mli: CEA_LGPL
+src/kernel_services/ast_building/cil_builder.ml: CEA_LGPL
+src/kernel_services/ast_building/cil_builder.mli: CEA_LGPL
src/kernel_services/ast_data/README.md: .ignore
src/kernel_services/ast_data/alarms.ml: CEA_LGPL
src/kernel_services/ast_data/alarms.mli: CEA_LGPL
diff --git a/share/Makefile.common b/share/Makefile.common
index affc77563611993266375cc54d2dfdfb7d31ba4e..a8db78b9f90ed31b98f2aaa537f1948fb6768a0e 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
@@ -43,6 +43,7 @@ FRAMAC_SRC_DIRS= plugins/pdg_types plugins/value_types \
kernel_services/ast_data \
kernel_services/ast_queries \
kernel_services/ast_printing \
+ kernel_services/ast_building \
kernel_services/cmdline_parameters \
kernel_services/plugin_entry_points \
kernel_services/abstract_interp \
diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml
new file mode 100644
index 0000000000000000000000000000000000000000..83db7e89fda810eba0c93f569741232ce0a85416
--- /dev/null
+++ b/src/kernel_services/ast_building/cil_builder.ml
@@ -0,0 +1,631 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* --- C & Logic expressions builder --- *)
+
+module Exp =
+struct
+ (*
+ This modules exportes polymorphic variant to simulate subtyping.
+ It uses regular variant internally though, instead of using only the
+ polymorphic variant, as
+ 1. it simplifies greatly the .mli since most of the types don't have
+ to be exposed ; it also greatly simplifies mistyping errors for the user
+ 2. recursive polymorphic variant do not allow inclusion of one into another
+ 3. it is much easier to type the program with regular variants
+ *)
+
+ type const' =
+ | Int of Integer.t
+ | CilConstant of Cil_types.constant
+ and var' =
+ Cil_types.varinfo
+ and lval' =
+ | CilLval of Cil_types.lval
+ | Var of var'
+ | Result
+ | Mem of exp'
+ | Field of lval' * Cil_types.fieldinfo
+ | FieldNamed of lval' * string
+ and exp' =
+ | CilExp of Cil_types.exp
+ | CilExpCopy of Cil_types.exp
+ | CilTerm of Cil_types.term
+ | Lval of lval'
+ | Const of const'
+ | Range of exp' option * exp' option
+ | Unop of Cil_types.unop * exp'
+ | Binop of Cil_types.binop * exp' * exp'
+
+ type const = [ `const of const' ]
+ type var = [ `var of var' ]
+ type lval = [ var | `lval of lval' ]
+ type exp = [ const | lval | `exp of exp' ]
+
+ (* Depolymorphize *)
+
+ let harden_const c =
+ match (c :> const) with
+ | `const const -> const
+
+ let harden_var v =
+ match (v :> var) with
+ | `var var -> var
+
+ let harden_lval lv =
+ match (lv :> lval) with
+ | #var as var -> Var (harden_var var)
+ | `lval lval -> lval
+
+ let harden_lval_opt = function
+ | `none -> None
+ | #lval as lval -> Some (harden_lval lval)
+
+ let harden_exp e =
+ match (e :> exp) with
+ | #const as const -> Const (harden_const const)
+ | #lval as lval -> Lval (harden_lval lval)
+ | `exp exp -> exp
+
+ let harden_exp_opt = function
+ | `none -> None
+ | #exp as exp -> Some (harden_exp exp)
+
+ let harden_exp_list l =
+ List.map harden_exp l
+
+ (* Build *)
+
+ let constant c = `const (CilConstant c)
+ let integer i = `const (Int i)
+ let int i = `const (Int (Integer.of_int i))
+ let zero = int 0
+ let one = int 1
+ let var v = `var v
+ let lval lv = `lval (CilLval lv)
+ let exp e = `exp (CilExp e)
+ let exp_copy e = `exp (CilExpCopy e)
+ 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
+ let bwnot e = unop Cil_types.BNot e
+ let binop op e1 e2 = `exp (Binop (op, harden_exp e1, harden_exp e2))
+ let add e1 e2 = binop Cil_types.PlusA e1 e2
+ let sub e1 e2 = binop Cil_types.MinusA e1 e2
+ let mul e1 e2 = binop Cil_types.Mult e1 e2
+ let div e1 e2 = binop Cil_types.Div e1 e2
+ let modulo e1 e2 = binop Cil_types.Mod e1 e2
+ let shiftl e1 e2 = binop Cil_types.Shiftlt e1 e2
+ let shiftr e1 e2 = binop Cil_types.Shiftrt e1 e2
+ let lt e1 e2 = binop Cil_types.Lt e1 e2
+ let gt e1 e2 = binop Cil_types.Gt e1 e2
+ let le e1 e2 = binop Cil_types.Le e1 e2
+ let ge e1 e2 = binop Cil_types.Ge e1 e2
+ let eq e1 e2 = binop Cil_types.Eq e1 e2
+ let ne e1 e2 = binop Cil_types.Ne e1 e2
+ let bwand e1 e2 = binop Cil_types.BAnd e1 e2
+ let bwor e1 e2 = binop Cil_types.BOr e1 e2
+ let bwxor e1 e2 = binop Cil_types.BXor e1 e2
+ let logand e1 e2 = binop Cil_types.LAnd e1 e2
+ let logor e1 e2 = binop Cil_types.LOr e1 e2
+ let mem e = `lval (Mem (harden_exp e))
+ let field lv fi = `lval (Field (harden_lval lv, fi))
+ let fieldnamed lv s = `lval (FieldNamed (harden_lval lv, s))
+ let result = `lval Result
+ let term t = `exp (CilTerm t)
+ let none = `none
+ let range e1 e2 = `exp (Range (harden_exp_opt e1, harden_exp_opt e2))
+
+ exception EmptyList
+
+ let reduce f l =
+ match (l :> exp list) with
+ | [] -> raise EmptyList
+ | h :: t -> List.fold_left f h t
+
+ let logand_list l = reduce logand l
+ let logor_list l = reduce logor l
+
+ let (+), (-), ( * ), (/), (%) = add, sub, mul, div, modulo
+ let (<<), (>>) = shiftl, shiftr
+ let (<), (>), (<=), (>=), (==), (!=) = lt, gt, le, ge, eq, ne
+
+ (* Convert *)
+
+ exception LogicInC
+ exception CInLogic
+ exception Typing_error of string
+
+ let get_fieldinfo typ fieldname =
+ match Cil.unrollType typ with
+ | Cil_types.TComp (compinfo,_,_) ->
+ begin try
+ Cil.getCompField compinfo fieldname
+ with Not_found ->
+ let cname = compinfo.Cil_types.cname in
+ raise (Typing_error ("no field " ^ fieldname ^ " in " ^ cname))
+ end
+ | _ ->
+ raise (Typing_error ("trying to get a field of a non-composite type"))
+
+ let get_fieldinfo_from_ltype ltyp fieldname =
+ match Logic_utils.unroll_type ltyp with
+ | Cil_types.Ctype typ ->
+ get_fieldinfo typ fieldname
+ | _ ->
+ raise (Typing_error ("trying to get a field of a logic type"))
+
+ let rec build_constant = function
+ | CilConstant const -> const
+ | Int i -> Cil_types.(CInt64 (i, IInt, None))
+
+ and build_lval ~loc = function
+ | CilLval lval -> lval
+ | Var v -> Cil_types.(Var v, NoOffset)
+ | Result -> raise LogicInC
+ | Mem e ->
+ Cil.mkMem ~addr:(build_exp ~loc e) ~off:Cil_types.NoOffset
+ | Field (lv,f) ->
+ let host, offset = build_lval ~loc lv in
+ let offset' = Cil.addOffset Cil_types.(Field (f, NoOffset)) in
+ host, offset' offset
+ | FieldNamed (lv,s) ->
+ let (host, offset) as lval = build_lval ~loc lv in
+ let ty = Cil.typeOfLval lval in
+ let f = get_fieldinfo ty s in
+ let offset' = Cil_types.(Field (f, NoOffset)) in
+ host, Cil.addOffset offset' offset
+
+ and build_exp ~loc = function
+ | CilTerm _ | Range _ -> raise LogicInC
+ | 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))
+ | Unop (op,e) ->
+ let e' = build_exp ~loc e in
+ let t = Cil.typeOf e' in
+ let t' = Cil.integralPromotion t in
+ Cil.(new_exp ~loc (Cil_types.UnOp (op, mkCastT e' t t', t')))
+ | Binop (op,e1,e2) ->
+ let e1' = build_exp ~loc e1
+ and e2' = build_exp ~loc e2 in
+ Cil.mkBinOp ~loc op e1' e2'
+
+ let rec build_term_lval ~loc ~restyp = function
+ | CilLval _ -> raise CInLogic
+ | Var v -> Cil_types.(TVar (Cil.cvar_to_lvar v), TNoOffset)
+ | Mem e -> Cil_types.(TMem (build_term ~loc ~restyp e), TNoOffset)
+ | Result -> Cil_types.(TResult restyp, TNoOffset)
+ | Field (lv,f) ->
+ let host, offset = build_term_lval ~loc ~restyp lv in
+ let offset' = Cil_types.(TField (f, TNoOffset)) in
+ host, Logic_const.addTermOffset offset' offset
+ | FieldNamed (lv,s) ->
+ let (host, offset) as tlval = build_term_lval ~loc ~restyp lv in
+ let ty = Cil.typeOfTermLval tlval in
+ let f = get_fieldinfo_from_ltype ty s in
+ let offset' = Cil_types.(TField (f, TNoOffset)) in
+ host, Logic_const.addTermOffset offset' offset
+
+ and build_term ~loc ~restyp = function
+ | Const (CilConstant _) | CilExp _ | CilExpCopy _ -> raise CInLogic
+ | CilTerm term -> term
+ | Const (Int i) ->
+ Logic_const.tint ~loc i
+ | Lval lval ->
+ let tlval = build_term_lval ~loc ~restyp lval in
+ Logic_const.term ~loc Cil_types.(TLval tlval) (Cil.typeOfTermLval tlval)
+ | Unop (op,e) ->
+ let t = build_term e ~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 ty = t1.Cil_types.term_type in
+ (* TODO: type conversion *)
+ Logic_const.term ~loc Cil_types.(TBinOp (op,t1,t2)) ty
+ | Range (t1,t2) ->
+ let t1' = Extlib.opt_map (build_term ~loc ~restyp) t1
+ and t2' = Extlib.opt_map (build_term ~loc ~restyp) t2 in
+ Logic_const.trange ~loc (t1',t2')
+
+ (* Export *)
+
+ 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_lval_opt ~loc lv =
+ Extlib.opt_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 = Extlib.opt_map (build_exp ~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)
+end
+
+
+(* --- Pure builder --- *)
+
+module Pure =
+struct
+ include Exp
+
+ type instr' =
+ | CilInstr of Cil_types.instr
+ | Skip
+ | Assign of lval' * exp'
+ | Call of lval' option * exp' * exp' list
+
+ type stmt' =
+ | CilStmt of Cil_types.stmt
+ | CilStmtkind of Cil_types.stmtkind
+ | Instr of instr'
+ | Sequence of stmt' list
+
+ 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 =
+ match (i :> instr) with
+ | `instr instr -> instr
+
+ let harden_stmt s =
+ match (s :> stmt) with
+ | #instr as instr -> Instr (harden_instr instr)
+ | `stmt stmt -> stmt
+
+ (* Build *)
+
+ let instr i = `instr (CilInstr i)
+ let skip = `instr Skip
+ let assign dest src = `instr (Assign (harden_lval dest, harden_exp src))
+ let incr dest = `instr (Assign (harden_lval dest, harden_exp (add dest one)))
+ let call res callee args =
+ `instr (Call (harden_lval_opt res, harden_exp callee, harden_exp_list args))
+ let stmtkind sk = `stmt (CilStmtkind sk)
+ let stmt s = `stmt (CilStmt s)
+ let stmts l = `stmt (Sequence (List.map (fun s -> CilStmt s) l))
+ let block l = `stmt (Sequence (List.map harden_stmt l))
+
+ (* Convert *)
+
+ let build_instr ~loc = function
+ | CilInstr i -> i
+ | Skip ->
+ Cil_types.Skip (loc)
+ | Assign (dest,src) ->
+ Cil_types.Set (build_lval ~loc dest, build_exp ~loc src, loc)
+ | Call (dest,callee,args) ->
+ let dest' = Extlib.opt_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 = 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 l)
+
+ and build_stmt ~loc = function
+ | CilStmt s -> s
+ | stmt -> Cil.mkStmt (build_stmtkind ~loc stmt)
+
+ and build_block ~loc l =
+ let bstmts = List.map (build_stmt ~loc) (flatten_sequences l) in
+ Cil.mkBlock bstmts
+
+ (* Export *)
+
+ let cil_instr ~loc i = build_instr ~loc (harden_instr i)
+ let cil_stmtkind ~loc s = build_stmtkind ~loc (harden_stmt s)
+ let cil_stmt ~loc s = build_stmt ~loc (harden_stmt s)
+end
+
+
+(* --- Stateful builder --- *)
+
+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) =
+struct
+ include Exp
+
+ type block =
+ {
+ block_type: block_type;
+ mutable stmts: Cil_types.stmt list; (* In reverse order *)
+ mutable locals: Cil_types.varinfo list; (* In reverse order *)
+ mutable pending_labels: Cil_types.label list;
+ }
+ and block_type =
+ | Block
+ | IfThen of {ifthen_exp: Cil_types.exp}
+ | IfThenElse of {ifthenelse_exp: Cil_types.exp; then_block: Cil_types.block}
+ | Switch of {switch_exp: Cil_types.exp}
+ | Function of {fundec: Cil_types.fundec}
+
+
+ let loc = Location.loc
+
+ (* State management *)
+
+ let stack : block list ref = ref []
+ let owner: Cil_types.fundec option ref = ref None
+
+ let pretty_stack fmt =
+ let pretty_block fmt b =
+ match b.block_type with
+ | Block -> Format.pp_print_string fmt "block"
+ | IfThen _ -> Format.pp_print_string fmt "if-then"
+ | IfThenElse _ -> Format.pp_print_string fmt "if-then-else"
+ | Switch _ -> Format.pp_print_string fmt "switch"
+ | Function _ -> Format.pp_print_string fmt "function"
+ in
+ Pretty_utils.pp_list ~pre:"[@[" ~sep:";@," ~last:"@]]"
+ pretty_block fmt !stack
+
+ let check_empty () =
+ if !stack <> [] then
+ raise (WrongContext "some contextes have not been closed")
+
+ let check_not_empty () =
+ if !stack = [] then
+ raise (WrongContext "only a finish_* function can close all contextes")
+
+ let top () =
+ match !stack with
+ | [] -> raise (WrongContext "not in an opened context")
+ | state :: _ -> state
+
+ let push state =
+ stack := state :: !stack;
+ Kernel.debug ~dkey "push onto %t" pretty_stack
+
+ let pop () =
+ Kernel.debug ~dkey "pop from %t" pretty_stack;
+ match !stack with
+ | [] -> raise (WrongContext "not in an opened context")
+ | hd :: tail ->
+ stack := tail;
+ hd
+
+ let finish () =
+ match !stack with
+ | [] -> raise (WrongContext "not in an opened context")
+ | [b] -> b
+ | _ :: _ :: _ -> raise (WrongContext "all contextes have not been closed")
+
+ let reset_owner () =
+ owner := None
+
+ let set_owner o =
+ owner := Some o
+
+ let get_owner () =
+ match !owner with
+ | None -> raise (WrongContext "not in an opened function")
+ | Some fundec -> fundec
+
+ (* Block management *)
+
+ let append_stmt b s =
+ if b.pending_labels <> [] then begin
+ s.Cil_types.labels <- List.rev b.pending_labels @ s.Cil_types.labels;
+ b.pending_labels <- [];
+ end;
+ b.stmts <- s :: b.stmts
+
+ (* Conversion to Cil *)
+
+ let build_block b =
+ if b.pending_labels <> [] then begin
+ append_stmt b (Cil.mkEmptyStmt ~loc ())
+ end;
+ let block = Cil.mkBlock (List.rev b.stmts) in
+ block.Cil_types.blocals <- List.rev b.locals;
+ block
+
+ let build_stmtkind b =
+ let block = build_block b in
+ match b.block_type with
+ | 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)
+ | Switch { switch_exp } ->
+ let open Cil_types in
+ (* Case are only allowed in the current block by the case function *)
+ let contains_case stmt =
+ 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)
+ | Function _ ->
+ raise (WrongContext "not convertible to stmtkind")
+
+ (* Statements *)
+
+ let stmt s =
+ let b = top () in
+ append_stmt b s
+
+ let stmts l =
+ let b = top () in
+ List.iter (append_stmt b) l
+
+ let stmtkind sk =
+ stmt (Cil.mkStmt sk)
+
+ let new_block block_type = {
+ block_type;
+ stmts = [];
+ locals = [];
+ pending_labels = [];
+ }
+
+ let open_function name =
+ check_empty ();
+ let fundec = Cil.emptyFunction name in
+ set_owner fundec;
+ push (new_block (Function {fundec}));
+ `var fundec.Cil_types.svar
+
+ let open_block () =
+ push (new_block Block)
+
+ let open_switch exp =
+ let switch_exp = cil_exp ~loc exp in
+ push (new_block (Switch {switch_exp}))
+
+ let open_if exp =
+ let ifthen_exp = cil_exp ~loc exp in
+ push (new_block (IfThen {ifthen_exp}))
+
+ let open_else () =
+ let b = pop () in
+ let ifthenelse_exp = match b.block_type with
+ | IfThen {ifthen_exp} -> ifthen_exp
+ | _ -> raise (WrongContext "not in an opened if-then-else context")
+ in
+ let then_block = build_block b in
+ push (new_block (IfThenElse {ifthenelse_exp; then_block}))
+
+ let close () =
+ let above = pop () in
+ check_not_empty ();
+ stmtkind (build_stmtkind above) (* add the block to the parent *)
+
+ let finish_block () =
+ let b = finish () in
+ match build_stmtkind b with
+ | Cil_types.Block b -> b
+ | _ -> raise (WrongContext "not in an opened simple block context")
+
+ let finish_stmt () =
+ let b = finish () in
+ Cil.mkStmt (build_stmtkind b)
+
+ let finish_function ?(register=true) () =
+ let b = finish () in
+ match b.block_type with
+ | Function {fundec} ->
+ let open Cil_types in
+ fundec.sbody <- build_block b;
+ fundec.svar.vdefined <- true;
+ if register then begin
+ let funspec = Cil.empty_funspec () in
+ Globals.Functions.replace_by_definition funspec fundec loc;
+ let keepSwitch = Kernel.KeepSwitch.get () in
+ Cfg.prepareCFG ~keepSwitch fundec;
+ Cfg.cfgFun fundec;
+ end;
+ reset_owner ();
+ GFun (fundec,loc)
+ | _ -> raise (WrongContext "not in a opened function context")
+
+ let case exp =
+ let b = top () in
+ match b.block_type with
+ | Switch _context ->
+ let label = Cil_types.Case (cil_exp ~loc exp, loc) in
+ b.pending_labels <- label :: b.pending_labels
+ | _ -> raise (WrongContext "no in a opened switch context")
+
+ let break () =
+ stmtkind (Cil_types.Break loc)
+
+ let return exp =
+ stmtkind (Cil_types.Return (cil_exp_opt ~loc exp, loc))
+
+ (* Instructions *)
+
+ let instr i =
+ stmtkind (Cil_types.Instr i)
+
+ let assign lval exp =
+ let lval' = cil_lval ~loc lval
+ and exp' = cil_exp ~loc exp in
+ instr (Cil_types.Set (lval', exp', loc))
+
+ let incr lval =
+ assign lval (add lval (int 1))
+
+ let call dest callee args =
+ let dest' = cil_lval_opt ~loc dest
+ and callee' = cil_exp ~loc callee
+ and args' = cil_exp_list ~loc args in
+ instr (Cil_types.Call (dest', callee', args', loc))
+
+ (* Variables *)
+
+ let return_type typ =
+ let fundec = get_owner () in
+ Cil.setReturnType fundec typ
+
+ let local typ name =
+ let fundec = get_owner () in
+ let v = Cil.makeLocalVar fundec ~insert:false name typ in
+ `var v
+
+ let local_copy ?(suffix="_tmp") (`var vi) =
+ let fundec = get_owner () and b = top () in
+ let v = Cil.copyVarinfo vi (vi.Cil_types.vname ^ suffix) in
+ Cil.refresh_local_name fundec v;
+ fundec.Cil_types.slocals <- fundec.Cil_types.slocals @ [v];
+ b.locals <- v :: b.locals;
+ `var v
+
+ let parameter ?(attributes=[]) typ name =
+ let fundec = get_owner () in
+ let v = Cil.makeFormalVar fundec name typ in
+ v.Cil_types.vattr <- attributes;
+ `var v
+end
diff --git a/src/kernel_services/ast_building/cil_builder.mli b/src/kernel_services/ast_building/cil_builder.mli
new file mode 100644
index 0000000000000000000000000000000000000000..17b07cf2e44a2827b9c3f3ba2c133801a2f27016
--- /dev/null
+++ b/src/kernel_services/ast_building/cil_builder.mli
@@ -0,0 +1,199 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(*
+- Permet l'utilisation des lval là où il faut des expression (sous typage)
+- Construit de la même manière le C et la logique
+- Pas nécessaire de renseigner la location partout
+- Interface unifiée vers les smart constructors
+*)
+
+
+(* --- C & Logic expressions builder --- *)
+
+module Exp :
+sig
+ type const'
+ type var'
+ type lval'
+ type exp'
+
+ type const = [ `const of const' ]
+ type var = [ `var of var' ]
+ type lval = [ var | `lval of lval' ]
+ type exp = [ const | lval | `exp of exp' ]
+
+ (* Build Constants *)
+
+ val constant : Cil_types.constant -> [> const]
+ val int : int -> [> const]
+ val integer : Integer.t -> [> const]
+ val zero : [> const]
+ val one : [> const]
+
+ (* Build LValues *)
+
+ val var : Cil_types.varinfo -> [> var]
+ val lval : Cil_types.lval -> [> lval]
+
+ (* Build Expressions *)
+
+ val exp : Cil_types.exp -> [> exp]
+ val exp_copy : Cil_types.exp -> [> exp]
+ val unop : Cil_types.unop -> [< exp] -> [> exp]
+ val neg : [< exp] -> [> exp]
+ val lognot : [< exp] -> [> exp]
+ val bwnot : [< exp] -> [> exp]
+ val binop : Cil_types.binop -> [< exp] -> [< exp] -> [> exp]
+ val add : [< exp] -> [< exp] -> [> exp]
+ val sub : [< exp] -> [< exp] -> [> exp]
+ val mul : [< exp] -> [< exp] -> [> exp]
+ val div : [< exp] -> [< exp] -> [> exp]
+ val modulo : [< exp] -> [< exp] -> [> exp]
+ val shiftl : [< exp] -> [< exp] -> [> exp]
+ val shiftr : [< exp] -> [< exp] -> [> exp]
+ val lt : [< exp] -> [< exp] -> [> exp]
+ val gt : [< exp] -> [< exp] -> [> exp]
+ val le : [< exp] -> [< exp] -> [> exp]
+ val ge : [< exp] -> [< exp] -> [> exp]
+ val eq : [< exp] -> [< exp] -> [> exp]
+ val ne : [< exp] -> [< exp] -> [> exp]
+ val logor : [< exp] -> [< exp] -> [> exp]
+ val logand : [< exp] -> [< exp] -> [> exp]
+ val bwand : [< exp] -> [< exp] -> [> exp]
+ val bwor : [< exp] -> [< exp] -> [> exp]
+ val bwxor : [< exp] -> [< exp] -> [> exp]
+ val mem : [< exp] -> [> lval]
+ val field : [< lval] -> Cil_types.fieldinfo -> [> lval]
+ val fieldnamed : [< lval] -> string -> [> lval]
+ val result : [> lval]
+ val term : Cil_types.term -> [> exp]
+ val none : [> `none]
+ val range : [< exp | `none] -> [< exp | `none] -> [> exp]
+
+ exception EmptyList
+
+ val logor_list : [< exp] list -> exp
+ val logand_list : [< exp] list -> exp
+
+ (* Redefined operators *)
+
+ val (+) : [< exp] -> [< exp] -> [> exp]
+ val (-) : [< exp] -> [< exp] -> [> exp]
+ val ( * ) : [< exp] -> [< exp] -> [> exp]
+ val (/) : [< exp] -> [< exp] -> [> exp]
+ val (%) : [< exp] -> [< exp] -> [> exp]
+ val (<<) : [< exp] -> [< exp] -> [> exp]
+ val (>>) : [< exp] -> [< exp] -> [> exp]
+ val (<) : [< exp] -> [< exp] -> [> exp]
+ val (>) : [< exp] -> [< exp] -> [> exp]
+ val (<=) : [< exp] -> [< exp] -> [> exp]
+ val (>=) : [< exp] -> [< exp] -> [> exp]
+ val (==) : [< exp] -> [< exp] -> [> exp]
+ val (!=) : [< exp] -> [< exp] -> [> exp]
+
+ (* Export CIL objects from built expressions *)
+
+ exception LogicInC
+ exception CInLogic
+ exception Typing_error of string
+
+ val cil_constant : [< const] -> Cil_types.constant
+ val cil_varinfo : [< var] -> Cil_types.varinfo
+ val cil_lval : loc:Cil_types.location -> [< lval] -> Cil_types.lval
+ val cil_exp : loc:Cil_types.location -> [< exp] -> Cil_types.exp
+ val cil_term_lval : loc:Cil_types.location -> restyp:Cil_types.typ ->
+ [< lval] -> Cil_types.term_lval
+ val cil_term : loc:Cil_types.location -> restyp:Cil_types.typ ->
+ [< exp] -> Cil_types.term
+end
+
+
+(* --- Pure builder --- *)
+
+module Pure :
+sig
+ include module type of Exp
+
+ type instr'
+ type stmt'
+
+ type instr = [ `instr of instr' ]
+ type stmt = [ instr | `stmt of stmt' ]
+
+ val instr : Cil_types.instr -> [> instr]
+ val skip : [> instr]
+ val assign : [< lval] -> [< exp] -> [> instr]
+ val incr : [< lval] -> [> instr]
+ val call : [< lval | `none] -> [< exp] -> [< exp] list -> [> instr]
+ val stmtkind : Cil_types.stmtkind -> [> stmt]
+ val stmt : Cil_types.stmt -> [> stmt]
+ val stmts : Cil_types.stmt list -> [> stmt]
+ val block : [< 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
+end
+
+
+(* --- Stateful builder --- *)
+
+exception WrongContext of string
+
+module type T =
+sig
+ val loc : Cil_types.location
+end
+
+module Stateful (Location : T) :
+sig
+ include module type of Exp
+
+ (* Statements *)
+ val instr : Cil_types.instr -> unit
+ val stmtkind : Cil_types.stmtkind -> unit
+ val stmt : Cil_types.stmt -> unit
+ val stmts : Cil_types.stmt list -> unit
+ val open_function : string -> [> var]
+ val open_block : unit -> unit
+ val open_switch : [< exp] -> unit
+ val open_if : [< exp] -> unit
+ val open_else : unit -> unit
+ val close : unit -> unit
+ val finish_block : unit -> Cil_types.block
+ val finish_stmt : unit -> Cil_types.stmt
+ val finish_function : ?register:bool -> unit -> Cil_types.global
+ val case : [< exp] -> unit
+ val break : unit -> unit
+ val return : [< exp | `none] -> unit
+ val assign : [< lval] -> [< exp] -> unit
+ val incr : [< lval] -> unit
+ val call : [< lval | `none] -> [< exp] -> [< exp] list -> unit
+
+ (* Variables *)
+ val return_type : Cil_types.typ -> unit
+ val local : Cil_types.typ -> string -> [> var]
+ val local_copy : ?suffix:string -> [< var] -> [> var]
+ val parameter : ?attributes:Cil_types.attributes ->
+ Cil_types.typ -> string -> [> var]
+end