From 52b0e43a6fcc51559398b3372af48149751fb313 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 10 Jun 2020 17:07:14 +0200
Subject: [PATCH] [eacsl] Add a module supporting the translation of logic
arrays to expressions
---
src/plugins/e-acsl/Makefile.in | 1 +
src/plugins/e-acsl/headers/header_spec.txt | 2 +
.../e-acsl/src/code_generator/logic_array.ml | 294 ++++++++++++++++++
.../e-acsl/src/code_generator/logic_array.mli | 42 +++
4 files changed, 339 insertions(+)
create mode 100644 src/plugins/e-acsl/src/code_generator/logic_array.ml
create mode 100644 src/plugins/e-acsl/src/code_generator/logic_array.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index e7380d160ca..936fc6f57fa 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -74,6 +74,7 @@ SRC_CODE_GENERATOR:= \
at_with_lscope \
mmodel_translate \
logic_functions \
+ logic_array \
translate \
temporal \
memory_observer \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 1d8b97641ff..ece261d80bc 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -66,6 +66,8 @@ src/code_generator/label.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/label.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/literal_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/literal_observer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/logic_array.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/logic_array.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/logic_functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/logic_functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/loops.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
new file mode 100644
index 00000000000..af522479dc6
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -0,0 +1,294 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(* Forward references *)
+let translate_rte_ref:
+ (?filter:(code_annotation -> bool) -> kernel_function -> Env.t -> exp ->
+ Env.t) ref =
+ let func ?filter _kf _env _e =
+ let _ = filter in
+ Extlib.mk_labeled_fun "translate_rte_ref"
+ in
+ ref func
+
+(** @return the content of the array type if [ty] is an array, or None
+ otherwise. *)
+let rec get_array_typ_opt ty =
+ if Gmp_types.is_t ty then
+ (* GMP pointer types are declared as arrays of one element. They are treated
+ as a special case here to ensure that they are not considered as arrays.
+ *)
+ None
+ else
+ match ty with
+ | TNamed (r, _) -> get_array_typ_opt r.ttype
+ | TArray (t, eo, bsot, a) -> Some (t, eo, bsot, a)
+ | _ -> None
+
+let is_array ty =
+ match get_array_typ_opt ty with
+ | Some _ -> true
+ | None -> false
+
+(** Retrieve the length of the [array] expression in a new variable [name] and
+ return it as an expression.
+ If the length is present in the type then the function directly assigns the
+ length to the variable, otherwise it is computed with the formula
+ [length = (\block_length(array) - \offset(array)) / sizeof(elem_typ)]. *)
+let length_exp ~loc kf env ~name array =
+ let elem_typ, array_len =
+ match get_array_typ_opt (Cil.typeOf array) with
+ | None -> Options.fatal "Trying to retrieve the length of a non-array"
+ | Some (t, len, _, _) -> t, len
+ in
+ try
+ let len = Cil.lenOfArray64 array_len in
+ (Cil.kinteger64 ~loc len), env
+ with Cil.LenOfArray ->
+ (* check RTE on the array before accessing its block length and offset *)
+ let env = !translate_rte_ref kf env array in
+ (* helper function *)
+ let rtl env name =
+ Env.rtl_call_to_new_var
+ ~loc
+ env
+ kf
+ None
+ Cil.theMachine.typeOfSizeOf
+ name
+ [ array ]
+ in
+ (* block_length(array) *)
+ let block_length_exp, env = rtl env "block_length" in
+ (* offset(array) *)
+ let offset_exp, env = rtl env "offset" in
+ (* sizeof(elem_typ) *)
+ let sizeof_exp = Cil.new_exp ~loc (SizeOf elem_typ) in
+ (* Create var and compute length *)
+ let _, len_exp, env =
+ Env.new_var
+ ~loc
+ env
+ kf
+ None
+ ~name
+ Cil.theMachine.typeOfSizeOf
+ (fun v _ -> [
+ Constructor.mk_assigns
+ ~loc
+ ~result:(Cil.var v)
+ (Cil.mkBinOp
+ ~loc
+ Div
+ (Cil.mkBinOp ~loc MinusA block_length_exp offset_exp)
+ sizeof_exp)
+ ])
+ in
+ len_exp, env
+
+let comparison_to_exp ~loc kf env ~name bop array1 array2 =
+ (match bop with
+ | Eq | Ne -> () (* Ok *)
+ | _ ->
+ Options.fatal ~current:true "Something else than comparison of equality\
+ between two arrays.");
+
+ (* The generated code can be the same for [Ne] and [Eq] if we just adjust the
+ values for the result.
+ [res_value()] returns the initial value for
+ the result and [res_flip_value()] returns the flipped value of the result.
+ If the arrays have been coerced in ACSL to a different array size, then we
+ add a check to see if the coerced size is lesser or equal to then actual
+ length of the array.
+ The generated code returned by this function is equivalent to:
+ int result = res_value();
+ size_t len1 = length(array1);
+ size_t len2 = length(array2);
+ if (len1 == len2) {
+ // Here we add check that the coerced length doesn't exceed the
+ // actual length of the arrays.
+ // Then we compare the content of the arrays, using the coerced
+ // length.
+ for (int i = 0 ; i < len1 ; ++i) {
+ if (array1[i] != array2[i]) {
+ result = res_value(flip);
+ break;
+ }
+ }
+ } else {
+ result = res_value(flip);
+ }
+ result
+ *)
+ let res_value ?(flip=false) () =
+ match flip, bop with
+ | false, Eq | true, Ne -> Cil.one ~loc
+ | true, Eq | false, Ne -> Cil.zero ~loc
+ | _ -> assert false
+ in
+
+ (* Helper function: call [Env.pop_and_get] with [global_clear] and [where]
+ pre-set *)
+ let pop_and_get_env env stmt =
+ Env.pop_and_get
+ env
+ stmt
+ ~global_clear:false
+ Env.Middle
+ in
+
+ (* Create var that will hold the result of the comparison between the
+ two arrays *)
+ let comparison_vi, comparison_exp, env =
+ Env.new_var
+ ~loc
+ env
+ kf
+ None
+ ~name
+ Cil.intType
+ (fun v _ -> [ Constructor.mk_assigns ~loc ~result:(Cil.var v) (res_value ()) ])
+ in
+
+ (* Retrieve the length of the arrays *)
+ let len1_exp, env = length_exp ~loc kf env ~name:"length1" array1 in
+ let len2_exp, env = length_exp ~loc kf env ~name:"length2" array2 in
+
+ (* Push a new env to declare the variable that will hold the iterator of the
+ loop *)
+ let env = Env.push env in
+ let iter, iter_e, env =
+ Env.new_var
+ ~loc
+ env
+ kf
+ None
+ ~name:"iter"
+ Cil.theMachine.typeOfSizeOf
+ (fun _ _ -> [])
+ in
+
+ (* Push a new env to do the innermost comparison between two elements of the
+ arrays. This env will enable us to also check RTEs *)
+ let env = Env.push env in
+ (* Create the access to the arrays *)
+ let array1_iter_e = Constructor.mk_subscript ~loc array1 iter_e in
+ let array2_iter_e = Constructor.mk_subscript ~loc array2 iter_e in
+ (* Check RTE on the arrays, filtering out bounding checks since the accesses
+ are built already in bounds *)
+ let filter a =
+ let index_bound =
+ Alarms.get_name (Index_out_of_bound (iter_e, Some len1_exp))
+ in
+ match a.annot_content with
+ | AAssert (_, _, { pred_name = hd :: _ })
+ when Datatype.String.equal hd index_bound -> false
+ | _ -> true
+ in
+ let env = !translate_rte_ref ~filter kf env array1_iter_e in
+ let env = !translate_rte_ref ~filter kf env array2_iter_e in
+ (* Create the condition *)
+ let cond = Cil.mkBinOp ~loc Ne array1_iter_e array2_iter_e in
+ (* Create the statement representing the body of the for loop *)
+ let body =
+ Constructor.mk_if
+ ~loc
+ ~cond
+ (Cil.mkBlock [
+ Constructor.mk_assigns ~loc ~result:(Cil.var comparison_vi) (res_value ~flip:true ());
+ Constructor.mk_break ~loc
+ ])
+ in
+ (* Pop the env to build the body of the for loop *)
+ let body_blk, env = pop_and_get_env env body in
+
+ (* Create the statement representing the full for loop *)
+ let for_loop =
+ (Constructor.mk_block_stmt
+ (Cil.mkBlock
+ (Cil.mkForIncr
+ ~iter
+ ~first:(Cil.zero ~loc)
+ ~stopat:len1_exp
+ ~incr:(Cil.one ~loc)
+ ~body:[ Constructor.mk_block_stmt body_blk ]
+ )
+ )
+ )
+ in
+
+ (* Create the list of statements that will be in the `then` block of the
+ top-level if *)
+ let then_stmts = [ for_loop ] in
+
+ (* Add the check for the length before the for loop *)
+ let prepend_coercion_check ~name env stmts array len =
+ let array_orig = Option.get (Constructor.extract_uncoerced_lval array) in
+ if array_orig == array then
+ stmts, env
+ else
+ let len_orig, env =
+ length_exp ~loc kf env ~name:(name ^ "_orig") array_orig
+ in
+ let e = Cil.mkBinOp ~loc Le len len_orig in
+ let p =
+ Logic_const.prel
+ ~loc
+ (Rle, Logic_utils.expr_to_term len, Logic_utils.expr_to_term len_orig)
+ in
+ let p = { p with pred_name = "array_coercion" :: p.pred_name } in
+ let stmt =
+ Constructor.mk_runtime_check Constructor.RTE kf e p
+ in
+ stmt :: stmts, env
+ in
+ let then_stmts, env =
+ prepend_coercion_check ~name:"length2" env then_stmts array2 len2_exp
+ in
+ let then_stmts, env =
+ prepend_coercion_check ~name:"length1" env then_stmts array1 len1_exp
+ in
+
+ (* Pop the env to build the full then block *)
+ let then_blk, env =
+ pop_and_get_env env (Constructor.mk_block_stmt (Cil.mkBlock then_stmts))
+ in
+
+ (* Create the statement representing the whole generated code *)
+ let stmt =
+ Constructor.mk_if
+ ~loc
+ ~cond:(Cil.mkBinOp ~loc Eq len1_exp len2_exp)
+ then_blk
+ ~else_blk:(Cil.mkBlock
+ [ Constructor.mk_assigns
+ ~loc
+ ~result:(Cil.var comparison_vi)
+ (res_value ~flip:true ()) ])
+ in
+ (* Build the statement in the current env *)
+ let env = Env.add_stmt env kf stmt in
+
+ (* Return the result expression with the result of the comparison *)
+ comparison_exp, env
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.mli b/src/plugins/e-acsl/src/code_generator/logic_array.mli
new file mode 100644
index 00000000000..e6ca3976f85
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.mli
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+val is_array: typ -> bool
+(** @return true iff the type is an array *)
+
+val comparison_to_exp: loc:location -> kernel_function -> Env.t ->
+ name:string -> binop -> exp -> exp -> exp * Env.t
+(** [comparison_to_exp ~loc kf env ~name bop e1 e2] generate the C code
+ equivalent to [e1 bop e2].
+ Requires that [bop] is either [Ne] or [Eq] and that [e1] and [e2] are
+ arrays. *)
+
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val translate_rte_ref:
+ (?filter:(code_annotation -> bool) -> kernel_function -> Env.t -> exp ->
+ Env.t) ref
--
GitLab