Commit e9d9ee90 authored by Julien Signoles's avatar Julien Signoles
Browse files

[archi] file for smart constructors

parent e652c431
......@@ -65,6 +65,7 @@ SRC_PROJECT_INITIALIZER:=\
# code generator
SRC_CODE_GENERATOR:= \
constructor \
gmp \
label \
env \
......
......@@ -260,7 +260,10 @@ let to_exp ~loc kf env pot label =
let e_size, _ = term_to_exp kf env t_size in
let e_size = Cil.constFold false e_size in
let malloc_stmt =
Misc.mk_call ~loc ~result:(Cil.var vi) "malloc" [e_size]
Constructor.mk_lib_call ~loc
~result:(Cil.var vi)
"malloc"
[e_size]
in
malloc_stmt
| Typing.(C_integer _ | C_float _ | Gmpz) ->
......@@ -270,7 +273,7 @@ let to_exp ~loc kf env pot label =
| Typing.(Rational | Real | Nan) ->
Error.not_yet "quantification over non-integer type"
in
let free_stmt = Misc.mk_call ~loc "free" [e] in
let free_stmt = Constructor.mk_lib_call ~loc "free" [e] in
(* The list of stmts returned by the current closure are inserted
LOCALLY to the block where the new var is FIRST used, whatever scope
is indicated to [Env.new_var].
......
(**************************************************************************)
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2012-2018 *)
(* 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). *)
(* *)
(**************************************************************************)
open Cil_types
(* ********************************************************************** *)
(* Expressions *)
(* ********************************************************************** *)
let mk_deref ~loc lv = Cil.new_exp ~loc (Lval(Mem(lv), NoOffset))
(* ********************************************************************** *)
(* Statements *)
(* ********************************************************************** *)
let mk_stmt sk = Cil.mkStmt ~valid_sid:true sk
let mk_instr i = mk_stmt (Instr i)
let mk_call ~loc ?result e args = mk_instr (Call(result, e, args, loc))
type annotation_kind =
| Assertion
| Precondition
| Postcondition
| Invariant
| RTE
let kind_to_string loc k =
Cil.mkString
~loc
(match k with
| Assertion -> "Assertion"
| Precondition -> "Precondition"
| Postcondition -> "Postcondition"
| Invariant -> "Invariant"
| RTE -> "RTE")
let mk_block stmt b = match b.bstmts with
| [] ->
(match stmt.skind with
| Instr(Skip _) -> stmt
| _ -> assert false)
| [ s ] -> s
| _ :: _ -> mk_stmt (Block b)
(* ********************************************************************** *)
(* E-ACSL specific code *)
(* ********************************************************************** *)
let mk_lib_call ~loc ?result fname args =
let vi = Misc.get_lib_fun_vi fname in
let f = Cil.evar ~loc vi in
vi.vreferenced <- true;
let make_args args ty_params =
List.map2
(fun (_, ty, _) arg ->
let e =
match ty, Cil.unrollType (Cil.typeOf arg), arg.enode with
| TPtr _, TArray _, Lval lv -> Cil.new_exp ~loc (StartOf lv)
| TPtr _, TArray _, _ -> assert false
| _, _, _ -> arg
in
Cil.mkCast ~force:false ~newt:ty ~e)
ty_params
args
in
let args = match vi.vtype with
| TFun(_, Some params, _, _) -> make_args args params
| TFun(_, None, _, _) -> []
| _ -> assert false
in
mk_call ~loc ?result f args
let mk_rtl_call ~loc ?result fname args =
mk_lib_call ~loc ?result (Functions.RTL.mk_api_name fname) args
(* ************************************************************************** *)
(** {2 Handling the E-ACSL's C-libraries, part II} *)
(* ************************************************************************** *)
let mk_full_init_stmt ?(addr=true) vi =
let loc = vi.vdecl in
let mk = mk_rtl_call ~loc "full_init" in
match addr, Cil.unrollType vi.vtype with
| _, TArray(_,Some _, _, _) | false, _ -> mk [ Cil.evar ~loc vi ]
| _ -> mk [ Cil.mkAddrOfVi vi ]
let mk_initialize ~loc (host, offset as lv) = match host, offset with
| Var _, NoOffset ->
mk_rtl_call ~loc "full_init" [ Cil.mkAddrOf ~loc lv ]
| _ ->
let typ = Cil.typeOfLval lv in
mk_rtl_call ~loc
"initialize"
[ Cil.mkAddrOf ~loc lv; Cil.new_exp loc (SizeOf typ) ]
let mk_named_store_stmt name ?str_size vi =
let ty = Cil.unrollType vi.vtype in
let loc = vi.vdecl in
let store = mk_rtl_call ~loc name in
match ty, str_size with
| TArray(_, Some _,_,_), None ->
store [ Cil.evar ~loc vi ; Cil.sizeOf ~loc ty ]
| TPtr(TInt(IChar, _), _), Some size -> store [ Cil.evar ~loc vi ; size ]
| _, None -> store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
| _, Some _ -> assert false
let mk_store_stmt ?str_size vi =
mk_named_store_stmt "store_block" ?str_size vi
let mk_duplicate_store_stmt ?str_size vi =
mk_named_store_stmt "store_block_duplicate" ?str_size vi
let mk_delete_stmt vi =
let loc = vi.vdecl in
let mk = mk_rtl_call ~loc "delete_block" in
match Cil.unrollType vi.vtype with
| TArray(_, Some _, _, _) -> mk [ Cil.evar ~loc vi ]
| _ -> mk [ Cil.mkAddrOfVi vi ]
let mk_mark_readonly vi =
let loc = vi.vdecl in
mk_rtl_call ~loc "mark_readonly" [ Cil.evar ~loc vi ]
let mk_runtime_check ?(reverse=false) kind kf e p =
let loc = p.pred_loc in
let msg =
Kernel.Unicode.without_unicode
(Format.asprintf "%a@?" Printer.pp_predicate) p
in
let line = (fst loc).Filepath.pos_lnum in
let e =
if reverse then e else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
in
mk_rtl_call ~loc
"assert"
[ e;
kind_to_string loc kind;
Cil.mkString ~loc (Functions.RTL.get_original_name kf);
Cil.mkString ~loc msg;
Cil.integer loc line ]
(*
Local Variables:
compile-command: "make -C ../.."
End:
*)
(**************************************************************************)
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2012-2018 *)
(* 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). *)
(* *)
(**************************************************************************)
(** Smart constructors for building C code. *)
open Cil_types
open Cil_datatype
val mk_deref: loc:Location.t -> exp -> exp
(** Make a dereference of an expression *)
val mk_block: stmt -> block -> stmt
(* ********************************************************************** *)
(* E-ACSL specific code *)
(* ********************************************************************** *)
val mk_lib_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
(** Call of a library function.
@raise Unregistered_library_function if the given string does not represent
such a function or if these functions were never registered (only possible
when using E-ACSL through its API). *)
val mk_rtl_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
(** Special version of [mk_lib_call] for E-ACSL's RTL functions. *)
val mk_store_stmt: ?str_size:exp -> varinfo -> stmt
val mk_duplicate_store_stmt: ?str_size:exp -> varinfo -> stmt
val mk_delete_stmt: varinfo -> stmt
val mk_full_init_stmt: ?addr:bool -> varinfo -> stmt
val mk_initialize: loc:location -> lval -> stmt
val mk_mark_readonly: varinfo -> stmt
type annotation_kind =
| Assertion
| Precondition
| Postcondition
| Invariant
| RTE
val mk_runtime_check:
?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate ->
stmt
(** Generate a runtime check of the given expression. *)
(*
Local Variables:
compile-command: "make -C ../.."
End:
*)
......@@ -56,7 +56,7 @@ type local_env = {
type t = {
lscope: Lscope.t;
lscope_reset: bool;
annotation_kind: Misc.annotation_kind;
annotation_kind: Constructor.annotation_kind;
new_global_vars: (varinfo * localized_scope) list;
(* generated variables. The scope indicates the level where the variable
should be added. *)
......@@ -88,7 +88,7 @@ let empty_local_env =
let empty =
{ lscope = Lscope.empty;
lscope_reset = true;
annotation_kind = Misc.Assertion;
annotation_kind = Constructor.Assertion;
new_global_vars = [];
global_mp_tbl = empty_mp_tbl;
env_stack = [];
......
......@@ -139,8 +139,8 @@ end
(** {2 Current annotation kind} *)
(* ************************************************************************** *)
val annotation_kind: t -> Misc.annotation_kind
val set_annotation_kind: t -> Misc.annotation_kind -> t
val annotation_kind: t -> Constructor.annotation_kind
val set_annotation_kind: t -> Constructor.annotation_kind -> t
(* ************************************************************************** *)
(** {2 Loop invariants} *)
......
......@@ -112,8 +112,8 @@ let mk_init_function env =
Varinfo.Hashtbl.fold_sorted
(fun vi _ stmts ->
(* a global is both allocated and initialized *)
Misc.mk_store_stmt vi
:: Misc.mk_initialize ~loc:Location.unknown (Cil.var vi)
Constructor.mk_store_stmt vi
:: Constructor.mk_initialize ~loc:Location.unknown (Cil.var vi)
:: stmts)
tbl
stmts
......@@ -126,9 +126,9 @@ let mk_init_function env =
let e = Cil.new_exp ~loc:loc (Const (CStr s)) in
let str_size = Cil.new_exp loc (SizeOfStr s) in
Cil.mkStmtOneInstr ~valid_sid:true (Set(Cil.var vi, e, loc))
:: Misc.mk_store_stmt ~str_size vi
:: Misc.mk_full_init_stmt ~addr:false vi
:: Misc.mk_mark_readonly vi
:: Constructor.mk_store_stmt ~str_size vi
:: Constructor.mk_full_init_stmt ~addr:false vi
:: Constructor.mk_mark_readonly vi
:: stmts)
stmts
in
......@@ -172,8 +172,7 @@ let mk_init_function env =
let mk_delete_stmts stmts =
Varinfo.Hashtbl.fold_sorted
(fun vi _l acc ->
Misc.mk_delete_stmt vi :: acc)
(fun vi _l acc -> Constructor.mk_delete_stmt vi :: acc)
tbl
stmts
......
......@@ -33,7 +33,7 @@ let apply_on_var ~loc funname e =
else if Gmp_types.Q.is_t ty then "__gmpq_"
else assert false
in
Misc.mk_call ~loc (prefix ^ funname) [ e ]
Constructor.mk_lib_call ~loc (prefix ^ funname) [ e ]
let init ~loc e = apply_on_var "init" ~loc e
let clear ~loc e = apply_on_var "clear" ~loc e
......@@ -72,7 +72,7 @@ let generic_affect ~loc fname lv ev e =
let ty = Cil.typeOf ev in
if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then begin
let suf, args = get_set_suffix_and_arg e in
Misc.mk_call ~loc (fname ^ suf) (ev :: args)
Constructor.mk_lib_call ~loc (fname ^ suf) (ev :: args)
end else
Cil.mkStmtOneInstr ~valid_sid:true (Set(lv, e, e.eloc))
......@@ -92,8 +92,8 @@ let init_set ~loc lv ev e =
(match e.enode with
| Lval elv ->
assert (Gmp_types.Z.is_t (Cil.typeOf ev));
let call = Misc.mk_call
~loc
let call =
Constructor.mk_lib_call ~loc
"__gmpz_import"
[ ev;
Cil.one ~loc;
......
......@@ -84,7 +84,7 @@ let replace_literal_string_in_exp ~is_global_init env kf e =
if is_global_init then e, env else Literal_observer.exp_in_depth env kf e
let inject_in_local_init loc env kf vi = function
| ConsInit (fvi, sz :: _, _) as init
| ConsInit (fvi, _sz :: _, _) as init
when Functions.Libc.is_vla_alloc_name fvi.vname ->
(* handle variable-length array allocation via [__fc_vla_alloc]. Here each
instance of [__fc_vla_alloc] is rewritten to [alloca] (that is used to
......@@ -97,8 +97,7 @@ let inject_in_local_init loc env kf vi = function
fvi.vname <- Functions.Libc.actual_alloca;
(* Since we need to pass [vi] by value, cannot use [Misc.mk_store_stmt]
here. Do it manually. *)
let sname = Functions.RTL.mk_api_name "store_block" in
let store = Misc.mk_call ~loc sname [ Cil.evar vi ; sz ] in
let store = Constructor.mk_store_stmt vi in
let env = Env.add_stmt ~post:true env kf store in
init, env
......@@ -173,15 +172,14 @@ let add_initializer loc ?vi lv ?(post=false) stmt env kf =
let new_stmt =
(* bitfields are not yet supported ==> no initializer.
a [not_yet] will be raised in [Translate]. *)
if Cil.isBitfield lv
then Cil.mkEmptyStmt ()
else Misc.mk_initialize ~loc lv
if Cil.isBitfield lv then Cil.mkEmptyStmt ()
else Constructor.mk_initialize ~loc lv
in
let env = Env.add_stmt ~post ~before env kf new_stmt in
let env = match vi with
| None -> env
| Some vi ->
let new_stmt = Misc.mk_store_stmt vi in
let new_stmt = Constructor.mk_store_stmt vi in
Env.add_stmt ~post ~before env kf new_stmt
in
env
......@@ -291,17 +289,17 @@ let add_new_block_in_stmt env kf stmt =
if is_main kf && Mmodel_analysis.use_model () then begin
let stmts = b.bstmts in
let l = List.rev stmts in
let mclean = (Functions.RTL.mk_api_name "memory_clean") in
match l with
| [] -> assert false (* at least the 'return' stmt *)
| ret :: l ->
let loc = Stmt.loc stmt in
let delete_stmts =
Global_observer.mk_delete_stmts [ Misc.mk_call ~loc mclean []; ret ]
Global_observer.mk_delete_stmts
[ Constructor.mk_rtl_call ~loc "memory_clean" []; ret ]
in
b.bstmts <- List.rev l @ delete_stmts
end;
let new_stmt = Misc.mk_block stmt b in
let new_stmt = Constructor.mk_block stmt b in
if not (Cil_datatype.Stmt.equal stmt new_stmt) then begin
(* move the labels of the return to the new block in order to
evaluate the postcondition when jumping to them. *)
......@@ -331,7 +329,7 @@ let add_new_block_in_stmt env kf stmt =
let post_block, env =
Env.pop_and_get
env
(Misc.mk_block new_stmt pre_block)
(Constructor.mk_block new_stmt pre_block)
~global_clear:false
Env.Before
in
......@@ -340,7 +338,7 @@ let add_new_block_in_stmt env kf stmt =
then Cil.transient_block post_block
else post_block
in
let res = Misc.mk_block new_stmt post_block in
let res = Constructor.mk_block new_stmt post_block in
if not (Cil_datatype.Stmt.equal new_stmt res) then
E_acsl_label.move kf new_stmt res;
res, env
......@@ -512,10 +510,9 @@ and inject_in_block (env: Env.t) kf blk =
if Functions.instrument kf then
List.fold_left
(fun acc vi ->
if Mmodel_analysis.must_model_vi ~kf vi then
Misc.mk_delete_stmt vi :: acc
else
acc)
if Mmodel_analysis.must_model_vi ~kf vi
then Constructor.mk_delete_stmt vi :: acc
else acc)
stmts
blk.blocals
else
......@@ -548,7 +545,7 @@ and inject_in_block (env: Env.t) kf blk =
List.fold_left
(fun acc vi ->
if Mmodel_analysis.must_model_vi vi && not vi.vdefined
then Misc.mk_store_stmt vi :: acc
then Constructor.mk_store_stmt vi :: acc
else acc)
blk.bstmts
blk.blocals;
......@@ -735,8 +732,7 @@ let inject_mmodel_initializer main =
in
let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
let args = args @ [ ptr_size ] in
let name = Functions.RTL.mk_api_name "memory_init" in
let init = Misc.mk_call loc name args in
let init = Constructor.mk_rtl_call loc "memory_init" args in
main.sbody.bstmts <- init :: main.sbody.bstmts
in
Extlib.may handle_main main
......
......@@ -81,10 +81,10 @@ let preserve_invariant env kf stmt = match stmt.skind with
let blk, env =
Env.pop_and_get env last ~global_clear:false Env.Before
in
Misc.mk_block last blk :: stmts, env, invariants != []
Constructor.mk_block last blk :: stmts, env, invariants != []
| s :: tl -> handle_invariants (s :: stmts, env, false) tl
in
let env = Env.set_annotation_kind env Misc.Invariant in
let env = Env.set_annotation_kind env Constructor.Invariant in
let stmts, env, has_loop = handle_invariants ([], env, false) stmts in
let new_blk = { blk with bstmts = List.rev stmts } in
{ stmt with skind = Loop([], new_blk, loc, cont, break) },
......@@ -274,7 +274,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
| Some p ->
let e, env = !named_predicate_ref kf (Env.push env) p in
let stmt, env =
Misc.mk_e_acsl_guard ~reverse:true Misc.RTE kf e p, env
Constructor.mk_runtime_check ~reverse:true Constructor.RTE kf e p, env
in
let b, env = Env.pop_and_get env stmt ~global_clear:false Env.After in
let guard_for_small_type = Cil.mkStmt ~valid_sid:true (Block b) in
......
......@@ -39,7 +39,7 @@ let store ?before env kf vars =
tracking_stmt
?before
List.fold_right (* small list *)
Misc.mk_store_stmt
Constructor.mk_store_stmt
env
kf
vars
......@@ -48,7 +48,7 @@ let duplicate_store ?before env kf vars =
tracking_stmt
?before
Varinfo.Set.fold
Misc.mk_duplicate_store_stmt
Constructor.mk_duplicate_store_stmt
env
kf
vars
......@@ -57,7 +57,7 @@ let delete_from_list ?before env kf vars =
tracking_stmt
?before
List.fold_right (* small list *)
Misc.mk_delete_stmt
Constructor.mk_delete_stmt
env
kf
vars
......@@ -66,7 +66,7 @@ let delete_from_set ?before env kf vars =
tracking_stmt
?before
Varinfo.Set.fold
Misc.mk_delete_stmt
Constructor.mk_delete_stmt
env
kf
vars
......
......@@ -126,7 +126,7 @@ let call ~loc kf name ctx env t =
ctx
(fun v _ ->
let name = Functions.RTL.mk_api_name name in
[ Misc.mk_call ~loc ~result:(Cil.var v) name [ e ] ])
[ Constructor.mk_lib_call ~loc ~result:(Cil.var v) name [ e ] ])
in
res, env
......@@ -159,8 +159,11 @@ let gmp_to_sizet ~loc kf env size p =
None
sizet
(fun vi _ ->
[ Misc.mk_e_acsl_guard ~reverse:true Misc.RTE kf guard p;
Misc.mk_call ~loc ~result:(Cil.var vi) "__gmpz_get_ui" [ size ] ])
[ Constructor.mk_runtime_check ~reverse:true Constructor.RTE kf guard p;
Constructor.mk_lib_call ~loc
~result:(Cil.var vi)
"__gmpz_get_ui"
[ size ] ])
in
e, env
......@@ -242,7 +245,7 @@ let call_memory_block ~loc kf name ctx env ptr r p =
| "initialized" -> [ ptr; size ]
| _ -> Error.not_yet ("builtin " ^ name)
in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
[ Constructor.mk_lib_call ~loc ~result:(Cil.var v) fname args ])
in
e, env
......@@ -346,8 +349,10 @@ let call_with_size ~loc kf name ctx env t p =
(fun v _ ->
let ty = Misc.cty t.term_type in
let sizeof = Misc.mk_ptr_sizeof ty loc in
let fname = Functions.RTL.mk_api_name name in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e; sizeof ] ])
[ Constructor.mk_rtl_call ~loc
~result:(Cil.var v)
name
[ e; sizeof ] ])
in
res, env
in
......@@ -384,9 +389,8 @@ let call_valid ~loc kf name ctx env t p =
(fun v _ ->
let ty = Misc.cty t.term_type in
let sizeof = Misc.mk_ptr_sizeof ty loc in
let fname = Functions.RTL.mk_api_name name in
let args = [ e; sizeof; base; base_addr ] in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
[ Constructor.mk_rtl_call ~loc ~result:(Cil.var v) name args ])
in
res, env
in
......
......@@ -154,7 +154,10 @@ let add_cast ~loc ?name e env kf ty =
None
Cil.doubleType
(fun v _ ->
[ Misc.mk_call ~loc ~result:(Cil.var v) "__gmpq_get_d" [ e ] ])
[ Constructor.mk_lib_call ~loc
~result:(Cil.var v)
"__gmpq_get_d"
[ e ] ])
in
e, env