From b4636e5711c357c62e46eb45d5e5ee26980055d5 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 19 Nov 2020 15:22:08 +0100
Subject: [PATCH] [eacsl] Update ocaml calls to the RTL
- Add prefix parameter to `Smart_stmt.rtl_call`
- Remove `Smart_stmt.lib_call` and replace it with calls to `Smart_stmt.rtl_call`
- Add `Smart_stmt.call` to call an arbitrary function from the AST
- Use `Smart_stmt.call` when generating calls to `malloc` and `free
---
.../src/code_generator/at_with_lscope.ml | 4 +--
src/plugins/e-acsl/src/code_generator/gmp.ml | 7 ++--
.../src/code_generator/memory_translate.ml | 3 +-
.../e-acsl/src/code_generator/rational.ml | 14 ++++++--
.../e-acsl/src/code_generator/smart_stmt.ml | 35 ++++++++++++-------
.../e-acsl/src/code_generator/smart_stmt.mli | 15 +++++---
.../e-acsl/src/code_generator/temporal.ml | 34 +++++++++++-------
.../e-acsl/src/code_generator/translate.ml | 35 +++++++++++++------
src/plugins/e-acsl/src/libraries/functions.ml | 10 +++---
.../e-acsl/src/libraries/functions.mli | 6 ++++
10 files changed, 110 insertions(+), 53 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
index 671ea306b1f..ea38062b647 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
@@ -260,7 +260,7 @@ 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 =
- Smart_stmt.lib_call ~loc
+ Smart_stmt.call ~loc
~result:(Cil.var vi)
"malloc"
[ e_size ]
@@ -273,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 = Smart_stmt.lib_call ~loc "free" [e] in
+ let free_stmt = Smart_stmt.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].
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index 8a2b5385f1c..cfc50474029 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -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
- Smart_stmt.lib_call ~loc (prefix ^ funname) [ e ]
+ Smart_stmt.rtl_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
@@ -90,7 +90,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 ty e in
- Smart_stmt.lib_call ~loc (fname ^ suf) (ev :: args)
+ Smart_stmt.rtl_call ~loc ~prefix:"" (fname ^ suf) (ev :: args)
end else
Smart_stmt.assigns ~loc:e.eloc ~result:lv e
@@ -111,7 +111,8 @@ let init_set ~loc lv ev e =
| Lval elv ->
assert (Gmp_types.Z.is_t (Cil.typeOf ev));
let call =
- Smart_stmt.lib_call ~loc
+ Smart_stmt.rtl_call ~loc
+ ~prefix:""
"__gmpz_import"
[ ev;
Cil.one ~loc;
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 38166949656..524df6755b2 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -159,8 +159,9 @@ let gmp_to_sizet ~loc kf env size p =
sizet
(fun vi _ ->
[ Smart_stmt.runtime_check Smart_stmt.RTE kf guard p;
- Smart_stmt.lib_call ~loc
+ Smart_stmt.rtl_call ~loc
~result:(Cil.var vi)
+ ~prefix:""
"__gmpz_get_ui"
[ size ] ])
in
diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index 2f4417b0191..0af7f3b0697 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -148,8 +148,9 @@ let add_cast ~loc ?name e env kf ty =
None
Cil.doubleType
(fun v _ ->
- [ Smart_stmt.lib_call ~loc
+ [ Smart_stmt.rtl_call ~loc
~result:(Cil.var v)
+ ~prefix:""
"__gmpq_get_d"
[ e ] ])
in
@@ -197,7 +198,11 @@ let cmp ~loc bop e1 e2 env kf t_opt =
~name
Cil.intType
(fun v _ ->
- [ Smart_stmt.lib_call ~loc ~result:(Cil.var v) fname [ e1; e2 ] ])
+ [ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var v)
+ ~prefix:""
+ fname
+ [ e1; e2 ] ])
in
Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
@@ -226,7 +231,10 @@ let binop ~loc bop e1 e2 env kf t_opt =
[e2] *)
let e1, env = create ~loc e1 env kf None in
let e2, env = create ~loc e2 env kf None in
- let mk_stmts _ e = [ Smart_stmt.lib_call ~loc name [ e; e1; e2 ] ] in
+ let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
+ ~prefix:""
+ name
+ [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
let _, e, env = new_var_and_init ~loc ~name env kf t_opt mk_stmts in
e, env
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
index 98418854690..2c3497df873 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
@@ -30,7 +30,7 @@ let stmt sk = Cil.mkStmt ~valid_sid:true sk
let instr i = stmt (Instr i)
let block_stmt blk = stmt (Block blk)
let block_from_stmts stmts = block_stmt (Cil.mkBlock stmts)
-let call ~loc ?result e args = instr (Call(result, e, args, loc))
+let call_instr ~loc ?result e args = instr (Call(result, e, args, loc))
let assigns ~loc ~result e = instr (Set(result, e, loc))
@@ -68,13 +68,7 @@ let block stmt b = match b.bstmts with
(* E-ACSL specific code *)
(* ********************************************************************** *)
-let lib_call ~loc ?result fname args =
- let vi =
- try Rtl.Symbols.find_vi fname
- with Rtl.Symbols.Unregistered _ as exn ->
- try Builtins.find fname
- with Not_found -> raise exn
- in
+let do_call ~loc ?result vi args =
let f = Cil.evar ~loc vi in
vi.vreferenced <- true;
let make_args ~variadic args param_ty =
@@ -95,7 +89,7 @@ let lib_call ~loc ?result fname args =
Options.fatal
"Mismatch between the number of expressions given and the number \
of arguments in the signature when calling function '%s'"
- fname
+ vi.vname
in
List.rev (make_rev_args [] args param_ty)
in
@@ -104,10 +98,27 @@ let lib_call ~loc ?result fname args =
| TFun(_, None, _, _) -> []
| _ -> assert false
in
- call ~loc ?result f args
+ call_instr ~loc ?result f args
+
+let call ~loc ?result fname args =
+ let kf =
+ try Globals.Functions.find_by_name fname
+ with Not_found ->
+ Options.fatal "Unable to find function '%s'" fname
+ in
+ let vi = Globals.Functions.get_vi kf in
+ do_call ~loc ?result vi args
-let rtl_call ~loc ?result fname args =
- lib_call ~loc ?result (Functions.RTL.mk_api_name fname) args
+let rtl_call ~loc ?result ?(prefix=Functions.RTL.api_prefix) fname args =
+ let fname = prefix ^ fname in
+ let vi =
+ try Rtl.Symbols.find_vi fname
+ with Rtl.Symbols.Unregistered _ as exn ->
+ try Builtins.find fname
+ with Not_found ->
+ raise exn
+ in
+ do_call ~loc ?result vi args
(* ************************************************************************** *)
(** {2 Handling the E-ACSL's C-libraries, part II} *)
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
index 3aebb9f4cc2..abd797824e9 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
@@ -56,15 +56,22 @@ val break: loc:location -> stmt
(* E-ACSL specific code: build calls to its RTL API *)
(* ********************************************************************** *)
-val lib_call: loc:location -> ?result:lval -> string -> exp list -> stmt
+val call: loc:location -> ?result:lval -> string -> exp list -> stmt
+(** Construct a call to a function with the given name.
+ @raise Not_found if the given string does not represent a function in the
+ AST, for instance if the function does not exist. *)
+
+val rtl_call:
+ loc:location -> ?result:lval -> ?prefix:string -> string -> exp list -> stmt
(** Construct a call to a library function with the given name.
+
+ [prefix] defaults to the E-ACSL RTL API prefix and can be explicitely
+ provided to call functions without this prefix.
+
@raise Rtl.Symbols.Unregistered if the given string does not represent
such a function or if library functions were never registered (only possible
when using E-ACSL through its API). *)
-val rtl_call: loc:location -> ?result:lval -> string -> exp list -> stmt
-(** Special version of [lib_call] for E-ACSL's RTL functions. *)
-
val store_stmt: ?str_size:exp -> varinfo -> stmt
(** Construct a call to [__e_acsl_store_block] that observes the allocation of
the given varinfo. See [share/e-acsl/e_acsl.h] for details about this
diff --git a/src/plugins/e-acsl/src/code_generator/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
index d0f6ced85f1..f56c6d4837f 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.ml
+++ b/src/plugins/e-acsl/src/code_generator/temporal.ml
@@ -75,13 +75,13 @@ module Mk: sig
end = struct
let store_reference ~loc flow lhs rhs =
+ let prefix = RTL.temporal_prefix in
let fname = match flow with
| Direct -> "store_nblock"
| Indirect -> "store_nreferent"
| Copy -> Options.fatal "Copy flow type in store_reference"
in
- let fname = RTL.mk_temporal_name fname in
- Smart_stmt.lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs ]
+ Smart_stmt.rtl_call ~loc ~prefix fname [ Cil.mkAddrOf ~loc lhs; rhs ]
let save_param ~loc flow lhs pos =
let infix = match flow with
@@ -89,17 +89,19 @@ end = struct
| Indirect -> "nreferent"
| Copy -> "copy"
in
+ let prefix = RTL.temporal_prefix in
let fname = "save_" ^ infix ^ "_parameter" in
- let fname = RTL.mk_temporal_name fname in
- Smart_stmt.lib_call ~loc fname [ lhs ; Cil.integer ~loc pos ]
+ Smart_stmt.rtl_call ~loc ~prefix fname [ lhs ; Cil.integer ~loc pos ]
let pull_param ~loc vi pos =
+ let prefix = RTL.temporal_prefix in
+ let fname = "pull_parameter" in
let exp = Cil.mkAddrOfVi vi in
- let fname = RTL.mk_temporal_name "pull_parameter" in
let sz = Cil.kinteger ~loc IULong (Cil.bytesSizeOf vi.vtype) in
- Smart_stmt.lib_call ~loc fname [ exp ; Cil.integer ~loc pos ; sz ]
+ Smart_stmt.rtl_call ~loc ~prefix fname [ exp ; Cil.integer ~loc pos ; sz ]
let handle_return_referent ~save ~loc lhs =
+ let prefix = RTL.temporal_prefix in
let fname = match save with
| true -> "save_return"
| false -> "pull_return"
@@ -108,15 +110,17 @@ end = struct
(match (Cil.typeOf lhs) with
| TPtr _ -> ()
| _ -> Error.not_yet "Struct in return");
- Smart_stmt.lib_call ~loc (RTL.mk_temporal_name fname) [ lhs ]
+ Smart_stmt.rtl_call ~loc ~prefix fname [ lhs ]
let reset_return_referent ~loc =
- Smart_stmt.lib_call ~loc (RTL.mk_temporal_name "reset_return") []
+ let prefix = RTL.temporal_prefix in
+ Smart_stmt.rtl_call ~loc ~prefix "reset_return" []
let temporal_memcpy_struct ~loc lhs rhs =
- let fname = RTL.mk_temporal_name "memcpy" in
+ let prefix = RTL.temporal_prefix in
+ let fname = "memcpy" in
let size = Cil.sizeOf ~loc (Cil.typeOfLval lhs) in
- Smart_stmt.lib_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs; size ]
+ Smart_stmt.rtl_call ~loc ~prefix fname [ Cil.mkAddrOf ~loc lhs; rhs; size ]
end
(* }}} *)
@@ -301,12 +305,13 @@ end = struct
associated with memcpy/memset call *)
let call_memxxx current_stmt loc args fexp env kf =
if Libc.is_memcpy fexp || Libc.is_memset fexp then
+ let prefix = RTL.temporal_prefix in
let name = match fexp.enode with
| Lval(Var vi, _) -> vi.vname
| _ -> Options.fatal "[Temporal.call_memxxx] not a left-value"
in
let stmt =
- Smart_stmt.lib_call ~loc (RTL.mk_temporal_name name) args
+ Smart_stmt.rtl_call ~loc ~prefix name args
in
Env.add_stmt ~before:current_stmt ~post:false env kf stmt
else
@@ -320,8 +325,11 @@ end = struct
it makes sense to make this somewhat-debug-level-call. In production mode
the implementation of the function should be empty and compiler should
be able to optimize that code out. *)
- let name = (RTL.mk_temporal_name "reset_parameters") in
- let stmt = Smart_stmt.lib_call ~loc name [] in
+ let stmt =
+ let prefix = RTL.temporal_prefix in
+ let name = "reset_parameters" in
+ Smart_stmt.rtl_call ~loc ~prefix name []
+ in
let env = Env.add_stmt ~before:current_stmt ~post:false env kf stmt in
let stmt = Mk.reset_return_referent ~loc in
let env = Env.add_stmt ~before:current_stmt ~post:false env kf stmt in
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 2570aa9bbfb..8d7be521858 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -135,7 +135,11 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e =
None
new_ty
(fun v _ ->
- [ Smart_stmt.lib_call ~loc ~result:(Cil.var v) fname [ e ] ])
+ [ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var v)
+ ~prefix:""
+ fname
+ [ e ] ])
in
e, env
else if Gmp_types.Q.is_t ty || strnum = Str_R then
@@ -297,7 +301,7 @@ and context_insensitive_term_to_exp kf env t =
kf
~name:vname
(Some t)
- (fun _ ev -> [ Smart_stmt.lib_call ~loc name [ ev; e ] ])
+ (fun _ ev -> [ Smart_stmt.rtl_call ~loc ~prefix:"" name [ ev; e ] ])
in
e, env, C_number, ""
else if Gmp_types.Q.is_t ty then
@@ -326,7 +330,10 @@ and context_insensitive_term_to_exp kf env t =
let e2, env = term_to_exp kf env t2 in
if Gmp_types.Z.is_t ty then
let name = name_of_mpz_arith_bop bop in
- let mk_stmts _ e = [ Smart_stmt.lib_call ~loc name [ e; e1; e2 ] ] in
+ let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
+ ~prefix:""
+ name
+ [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
let _, e, env =
Env.new_var_and_mpz_init ~loc ~name env kf (Some t) mk_stmts
@@ -371,7 +378,7 @@ and context_insensitive_term_to_exp kf env t =
p
in
Env.add_assert kf cond p;
- let instr = Smart_stmt.lib_call ~loc name [ e; e1; e2 ] in
+ let instr = Smart_stmt.rtl_call ~loc ~prefix:"" name [ e; e1; e2 ] in
[ cond; instr ]
in
let name = Misc.name_of_binop bop in
@@ -429,7 +436,7 @@ and context_insensitive_term_to_exp kf env t =
(fun vi _e ->
let result = Cil.var vi in
let fname = "__gmpz_fits_ulong_p" in
- [ Smart_stmt.lib_call ~loc ~result fname [ e2 ] ])
+ [ Smart_stmt.rtl_call ~loc ~result ~prefix:"" fname [ e2 ] ])
in
e, env
in
@@ -459,7 +466,7 @@ and context_insensitive_term_to_exp kf env t =
in
let result = Cil.var vi in
let name = "__gmpz_get_ui" in
- let instr = Smart_stmt.lib_call ~loc ~result name [ e2 ] in
+ let instr = Smart_stmt.rtl_call ~loc ~result ~prefix:"" name [ e2 ] in
[ coerce_guard_cond; instr ]
in
let name = e2_name ^ bop_name ^ "_coerced" in
@@ -478,7 +485,10 @@ and context_insensitive_term_to_exp kf env t =
(* Create the shift instruction *)
let mk_shift_instr result_e =
let name = name_of_mpz_arith_bop bop in
- Smart_stmt.lib_call ~loc name [ result_e; e1; e2_as_bitcnt_e ]
+ Smart_stmt.rtl_call ~loc
+ ~prefix:""
+ name
+ [ result_e; e1; e2_as_bitcnt_e ]
in
(* Put t in an option to use with comparison_to_exp and
@@ -569,7 +579,7 @@ and context_insensitive_term_to_exp kf env t =
if Gmp_types.Z.is_t ty then
let mk_stmts _v e =
let name = name_of_mpz_arith_bop bop in
- let instr = Smart_stmt.lib_call ~loc name [ e; e1; e2 ] in
+ let instr = Smart_stmt.rtl_call ~loc ~prefix:"" name [ e; e1; e2 ] in
[ instr ]
in
let name = Misc.name_of_binop bop in
@@ -648,7 +658,11 @@ and context_insensitive_term_to_exp kf env t =
(Some t)
(Misc.cty (Extlib.the li.l_type))
(fun vi _ ->
- [ Smart_stmt.lib_call ~loc ~result:(Cil.var vi) fname args ])
+ [ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var vi)
+ ~prefix:""
+ fname
+ args ])
else
(* build the arguments and compute the integer_ty of the parameters *)
let params_ty, args, env =
@@ -797,8 +811,9 @@ and comparison_to_exp
~name
Cil.intType
(fun v _ ->
- [ Smart_stmt.lib_call ~loc
+ [ Smart_stmt.rtl_call ~loc
~result:(Cil.var v)
+ ~prefix:""
"__gmpz_cmp"
[ e1; e2 ] ])
in
diff --git a/src/plugins/e-acsl/src/libraries/functions.ml b/src/plugins/e-acsl/src/libraries/functions.ml
index 37cf8f8319f..4a82689a964 100644
--- a/src/plugins/e-acsl/src/libraries/functions.ml
+++ b/src/plugins/e-acsl/src/libraries/functions.ml
@@ -63,14 +63,14 @@ let has_fundef exp = match exp.enode with
module RTL = struct
(* prefix of all functions/variables from the public E-ACSL API *)
- let e_acsl_api_prefix = "__e_acsl_"
+ let api_prefix = "__e_acsl_"
(* prefix of temporal analysis functions of the public E-ACSL API *)
- let e_acsl_temporal_prefix = e_acsl_api_prefix ^ "temporal_"
+ let temporal_prefix = api_prefix ^ "temporal_"
(* prefix of all builtin functions/variables from the public E-ACSL API,
Builtin functions replace original calls in programs. *)
- let e_acsl_builtin_prefix = e_acsl_api_prefix ^ "builtin_"
+ let e_acsl_builtin_prefix = api_prefix ^ "builtin_"
(* prefix of functions/variables generated by E-ACSL *)
let e_acsl_gen_prefix = "__gen_e_acsl_"
@@ -78,9 +78,9 @@ module RTL = struct
(* prefix of literal strings generated by E-ACSL *)
let e_acsl_lit_string_prefix = e_acsl_gen_prefix ^ "literal_string"
- let mk_api_name fname = e_acsl_api_prefix ^ fname
+ let mk_api_name fname = api_prefix ^ fname
- let mk_temporal_name fname = e_acsl_temporal_prefix ^ fname
+ let mk_temporal_name fname = temporal_prefix ^ fname
let mk_gen_name name = e_acsl_gen_prefix ^ name
diff --git a/src/plugins/e-acsl/src/libraries/functions.mli b/src/plugins/e-acsl/src/libraries/functions.mli
index 4963870c285..f2d66cb65e8 100644
--- a/src/plugins/e-acsl/src/libraries/functions.mli
+++ b/src/plugins/e-acsl/src/libraries/functions.mli
@@ -38,6 +38,12 @@ val instrument: kernel_function -> bool
(* ************************************************************************** *)
module RTL: sig
+ val api_prefix: string
+ (** Prefix used for the public API of E-ACSL runtime library. *)
+
+ val temporal_prefix:string
+ (** Prefix used for the public API of E-ACSL runtime library dealing with
+ temporal analysis. *)
val mk_api_name: string -> string
(** Prefix a name (of a variable or a function) with a string that identifies
--
GitLab