diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index aed90a086c6ad3694d8b651b1b7c6dcb094c1d74..f7b3af2154a7d982397e655030d199bf8b7251a9 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -68,6 +68,10 @@ SRC_ANALYSES:= \
SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
# code generator
+CODE_GENERATOR_CMI:= \
+ contract_types
+CODE_GENERATOR_CMI:=$(addprefix src/code_generator/, $(CODE_GENERATOR_CMI))
+
SRC_CODE_GENERATOR:= \
smart_exp \
smart_stmt \
@@ -82,6 +86,7 @@ SRC_CODE_GENERATOR:= \
logic_functions \
logic_array \
translate \
+ contract \
temporal \
memory_observer \
literal_observer \
@@ -112,7 +117,8 @@ PLUGIN_CMO:= src/local_config \
$(SRC_ANALYSES) \
$(SRC_CODE_GENERATOR) \
src/main
-
+PLUGIN_CMI:= \
+ $(CODE_GENERATOR_CMI)
PLUGIN_HAS_MLI:=yes
PLUGIN_DISTRIBUTED:=yes
PLUGIN_DEPENDENCIES:= RteGen
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index de8c767ec7536bab5ed0794cd0055c093ec1a9b0..ac18901b5347f1d2d5263d35907e13d279a6cb00 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -82,6 +82,9 @@ src/analyses/typing.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/typing.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/at_with_lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/at_with_lscope.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/contract.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/contract.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/contract_types.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/env.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/env.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/global_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
new file mode 100644
index 0000000000000000000000000000000000000000..7a8291e0b66e658b7660e7feb38e681c89c084fb
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -0,0 +1,753 @@
+(**************************************************************************)
+(* *)
+(* 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
+open Contract_types
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let must_translate_ppt_ref : (Property.t -> bool) ref =
+ Extlib.mk_fun "must_translate_ppt_ref"
+
+let must_translate_ppt_opt_ref : (Property.t option -> bool) ref =
+ Extlib.mk_fun "must_translate_ppt_opt_ref"
+
+(**************************************************************************)
+(********************** Contract ********************************)
+(**************************************************************************)
+
+type t = contract
+
+(** Module to ease the access to the C API for contracts *)
+module Rtl_call: sig
+ val init:
+ loc:location -> result_name:string -> Env.t -> kernel_function -> int ->
+ varinfo * exp * Env.t
+ (** Call the C function [__e_acsl_contract_init] *)
+
+ val cleanup:
+ loc:location -> Env.t -> kernel_function -> exp -> Env.t
+ (** Call the C function [__e_acsl_contract_cleanup] *)
+
+ val set_assumes:
+ loc:location -> Env.t -> kernel_function -> exp -> int -> predicate ->
+ Env.t
+ (** Call the C function [__e_acsl_contract_set_behavior_assumes] *)
+
+ val get_assumes:
+ loc:location -> result:varinfo -> Env.t -> kernel_function -> exp -> int ->
+ Env.t
+ (** Call the C function [__e_acsl_contract_get_behavior_assumes] *)
+
+ val partial_count_behaviors:
+ loc:location -> result:varinfo -> Env.t -> kernel_function -> exp ->
+ int list -> Env.t
+ (** Call the C function [__e_acsl_contract_partial_count_behaviors] *)
+
+ val partial_count_all_behaviors:
+ loc:location -> result:varinfo -> Env.t -> kernel_function -> exp -> Env.t
+ (** Call the C function [__e_acsl_contract_partial_count_all_behaviors] *)
+
+end = struct
+ let init_function_name = "contract_init"
+
+ let init_kf_lazy =
+ lazy
+ (Globals.Functions.find_by_name
+ (Functions.RTL.mk_api_name init_function_name))
+
+ let ctyp_lazy =
+ lazy
+ (Globals.Types.find_type
+ Logic_typing.Typedef (Functions.RTL.mk_api_name "contract_t"))
+
+ let init ~loc ~result_name env kf count =
+ (* Tell Eva to use init as a builtin *)
+ let init_kf = Lazy.force init_kf_lazy in
+ Dep_eva.use_builtin init_kf "Frama_C_malloc";
+ (* Add a call to init in the environment *)
+ let ty = TPtr(Lazy.force ctyp_lazy, []) in
+ Env.new_var
+ ~loc
+ ~name:result_name
+ ~scope:Varname.Function
+ env
+ kf
+ None
+ ty
+ (fun vi _e ->
+ let result = Cil.var vi in
+ let count_e = Cil.integer ~loc count in
+ [ Smart_stmt.rtl_call
+ ~loc
+ ~result
+ init_function_name
+ [count_e] ])
+
+ let cleanup ~loc env kf contract =
+ Env.add_stmt
+ env
+ kf
+ (Smart_stmt.rtl_call
+ ~loc
+ "contract_clean"
+ [contract])
+
+ let set_assumes ~loc env kf contract idx assumes =
+ let idx_e = Cil.integer ~loc idx in
+ let assumes_e, env =
+ Translate.generalized_untyped_predicate_to_exp kf env assumes
+ in
+ Env.add_stmt
+ env
+ kf
+ (Smart_stmt.rtl_call
+ ~loc
+ "contract_set_behavior_assumes"
+ [contract; idx_e; assumes_e])
+
+ let get_assumes ~loc ~result env kf contract idx =
+ let idx_e = Cil.integer ~loc idx in
+ let result = Cil.var result in
+ Env.add_stmt
+ env
+ kf
+ (Smart_stmt.rtl_call
+ ~loc
+ ~result
+ "contract_get_behavior_assumes"
+ [contract; idx_e])
+
+ let partial_count_behaviors ~loc ~result env kf contract idxes =
+ let idxes, count =
+ List.fold_right
+ (fun idx (idxes, count) ->
+ Cil.integer ~loc idx :: idxes, count + 1)
+ idxes
+ ([], 0)
+ in
+ let result = Cil.var result in
+ Env.add_stmt
+ env
+ kf
+ (Smart_stmt.rtl_call
+ ~loc
+ ~result
+ "contract_partial_count_behaviors"
+ (contract :: Cil.integer ~loc count :: idxes))
+
+ let partial_count_all_behaviors ~loc ~result env kf contract =
+ let result = Cil.var result in
+ Env.add_stmt
+ env
+ kf
+ (Smart_stmt.rtl_call
+ ~loc
+ ~result
+ "contract_partial_count_all_behaviors"
+ [ contract ])
+end
+
+(** Convert the given assumes clauses list to a single [predicate] *)
+let assumes_predicate assumes =
+ List.fold_left
+ (fun acc p ->
+ let pred = p.ip_content.tp_statement in
+ let loc = pred.pred_loc in
+ Logic_const.pand ~loc
+ (acc,
+ Logic_const.unamed ~loc pred.pred_content))
+ Logic_const.ptrue
+ assumes
+
+(** Create a [predicate] from the requires [identified_predicate] *)
+let requires_predicate requires =
+ let pred = requires.ip_content.tp_statement in
+ let loc = pred.pred_loc in
+ let p = Logic_const.unamed ~loc pred.pred_content
+ in
+ p
+
+(** Create a [predicate] from the ensures [identified_predicate] *)
+let ensures_predicate ensures =
+ let pred = ensures.ip_content.tp_statement in
+ let loc = pred.pred_loc in
+ let p = Logic_const.unamed ~loc pred.pred_content
+ in
+ p
+
+let create ~loc spec =
+ (* Create a hashtable to associate a behavior name with an index *)
+ let name_to_idx_tbl = Hashtbl.create 7 in
+ let named_behaviors_count =
+ List.fold_left
+ (fun idx b ->
+ if Cil.is_default_behavior b then
+ idx
+ else begin
+ Hashtbl.add name_to_idx_tbl b.b_name idx;
+ idx + 1
+ end
+ )
+ 0
+ spec.spec_behavior
+ in
+ let var = None in
+ (* Create the contract *)
+ { location = loc;
+ named_behaviors_count;
+ name_to_idx_tbl;
+ var;
+ all_assumes_translated = true;
+ spec }
+
+(** Initialize the C API for the given contract *)
+let init kf env contract =
+ if contract.named_behaviors_count > 0 then
+ let loc = contract.location in
+ let contract_vi, contract_e, env =
+ Rtl_call.init
+ ~loc
+ ~result_name:"contract"
+ env
+ kf
+ contract.named_behaviors_count
+ in
+ contract.var <- Some (contract_vi, contract_e);
+ env
+ else env
+
+(** Cleanup the C API for the given contract *)
+let cleanup kf env contract =
+ match contract.var with
+ | None -> env
+ | Some (_, e) ->
+ let loc = contract.location in
+ Rtl_call.cleanup ~loc env kf e
+
+(** Retrieve the behavior index from its name for the given contract *)
+let get_bhvr_idx contract bhvr_name =
+ (* by construction, the behavior name is in the hashtable *)
+ try Hashtbl.find contract.name_to_idx_tbl bhvr_name
+ with _ -> assert false
+
+(** Retrieve the C variable with the contract structure for the given contract.
+ Assumes that there is such a variable. *)
+let get_contract_var contract =
+ match contract.var with
+ | Some (contract_vi, contract_e) -> contract_vi, contract_e
+ | None ->
+ Options.fatal
+ "Unexpected call to get_contract_var with a contract without named \
+ behaviors"
+
+(** Setup the assumes values for the C API *)
+let setup_assumes kf env contract =
+ match contract.var with
+ | None -> env
+ | Some (_, contract_e) ->
+ let do_fold env b =
+ let do_it env =
+ try
+ if Cil.is_default_behavior b then
+ env
+ else
+ let assumes = assumes_predicate b.b_assumes in
+ let loc = assumes.pred_loc in
+ Cil.CurrentLoc.set loc;
+ let idx = get_bhvr_idx contract b.b_name in
+ Rtl_call.set_assumes ~loc env kf contract_e idx assumes
+ with exn ->
+ (* Unable to translate the assumes clause. Save that fact and re-raise
+ the exception *)
+ contract.all_assumes_translated <- false;
+ raise exn
+ in
+ Env.handle_error do_it env
+ in
+ List.fold_left do_fold env contract.spec.spec_behavior
+
+(** Returns a closure that will (1) creates a local C variable when first
+ called and (2) returns said variable on subsequent calls. *)
+let mk_get_or_create_var kf typ var_name =
+ let var_ref = ref None in
+ let f ~loc env =
+ match !var_ref with
+ | None ->
+ let vi, e, env =
+ Env.new_var
+ ~loc
+ ~scope:Varname.Block
+ ~name:var_name
+ env
+ kf
+ None
+ typ
+ (fun _ _ -> [])
+ in
+ var_ref := Some (vi, e);
+ vi, e, env
+ | Some (vi, e) -> vi, e, env
+ in
+ f
+
+(** Drop-in replacement for [List.fold_left] with the folding function wrapped
+ in a [handle_error] call *)
+let fold_left_handle_error f env l =
+ (* Reverse input args of f *)
+ let f2 x env = f env x in
+ (* Call fold_left on the list with handle_error at each element *)
+ List.fold_left
+ (fun env x ->
+ Env.handle_error (f2 x) env)
+ env
+ l
+
+(** Drop-in replacement for [List.fold_left] when the accumulator is more than
+ the [env], with the folding function wrapped in a [handle_error] call.
+
+ The accumulator for the fold should be set up with a pair where the first
+ element is the environment and the second element the rest of the
+ accumulator. *)
+let fold_left_handle_error_with_args f (env, acc) l =
+ let f2 x (env, args) = f (env, args) x in
+ List.fold_left
+ (fun (env, args) x ->
+ Env.handle_error_with_args (f2 x) (env, args))
+ (env, acc)
+ l
+
+(** Insert requires check for the given contract in the environment *)
+let check_requires kf kinstr env contract =
+ let get_or_create_assumes_var =
+ mk_get_or_create_var kf Cil.intType "assumes_value"
+ in
+ let do_behavior env b =
+ if Cil.is_default_behavior b then
+ fold_left_handle_error
+ (fun env requires ->
+ if !must_translate_ppt_ref
+ (Property.ip_of_requires kf kinstr b requires) then
+ (* If translating the default behavior, directly translate the
+ predicate *)
+ let requires = requires_predicate requires in
+ let loc = requires.pred_loc in
+ Cil.CurrentLoc.set loc;
+ Translate.translate_predicate kf env requires
+ else
+ env)
+ env
+ b.b_requires
+ else
+ (* Compute the assumes predicate for pretty-printing *)
+ let assumes = assumes_predicate b.b_assumes in
+ (* Push a new env and check the requires of the behavior *)
+ let env = Env.push env in
+ let env, stmts =
+ fold_left_handle_error_with_args
+ (fun (env, stmts) requires ->
+ if !must_translate_ppt_ref
+ (Property.ip_of_requires kf kinstr b requires) then
+ let requires = requires_predicate requires in
+ let loc = requires.pred_loc in
+ Cil.CurrentLoc.set loc;
+ (* Prepend the name of the behavior *)
+ let requires =
+ { requires with pred_name = b.b_name :: requires.pred_name }
+ in
+ (* Create runtime check *)
+ let requires_e, env =
+ Translate.generalized_untyped_predicate_to_exp kf env requires
+ in
+ let stmt =
+ Smart_stmt.runtime_check
+ Smart_stmt.Precondition
+ kf
+ requires_e
+ requires
+ in
+ env, stmt :: stmts
+ else
+ env, stmts)
+ (env, [])
+ b.b_requires
+ in
+ let requires = Smart_stmt.block_from_stmts stmts in
+ (* Pop the env to build the requires check *)
+ let requires_blk, env =
+ Env.pop_and_get
+ env
+ requires
+ ~global_clear:false
+ Env.Middle
+ in
+ match stmts with
+ | [] ->
+ (* If no requires check have been generated, then return immediately *)
+ env
+ | _ :: _ ->
+ (* Generate a predicate that will retrieve and test the
+ already computed assumes value for the behavior *)
+ let loc = assumes.pred_loc in
+ Cil.CurrentLoc.set loc;
+ let assumes_vi, assumes_e, env =
+ get_or_create_assumes_var ~loc env
+ in
+ let _, contract_e = get_contract_var contract in
+ let idx = get_bhvr_idx contract b.b_name in
+ let env =
+ Rtl_call.get_assumes
+ ~loc
+ ~result:assumes_vi
+ env
+ kf
+ contract_e
+ idx
+ in
+ let stmt = Smart_stmt.if_stmt ~loc ~cond:assumes_e requires_blk in
+ Env.add_stmt env kf stmt
+ in
+ List.fold_left
+ do_behavior
+ env
+ contract.spec.spec_behavior
+
+type translate_ppt =
+ | Complete
+ | Disjoint
+ | Both
+
+(** For each set of behavior names in [clauses], [check_active_behaviors] counts
+ the number of active behaviors and creates assertions for the
+ [ppt_to_translate]. *)
+let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf kinstr env contract clauses =
+ let must_translate = !must_translate_ppt_ref in
+ let loc = contract.location in
+ Cil.CurrentLoc.set loc;
+ let do_clause env bhvrs =
+ let bhvrs_list = Datatype.String.Set.elements bhvrs in
+ let active = [] in (* TODO: 'for' behaviors, e-acsl#109 *)
+ let must_translate_complete =
+ match ppt_to_translate with
+ | Both | Complete ->
+ must_translate (Property.ip_of_complete kf kinstr ~active bhvrs_list)
+ | Disjoint -> false
+ in
+ let must_translate_disjoint =
+ match ppt_to_translate with
+ | Both | Disjoint ->
+ must_translate (Property.ip_of_disjoint kf kinstr ~active bhvrs_list)
+ | Complete -> false
+ in
+
+ if must_translate_complete || must_translate_disjoint then
+ (* Retrieve the number of active behaviors *)
+ let active_bhvrs_e, complete_msg, disjoint_msg, env =
+ let _, contract_e = get_contract_var contract in
+ let vi, e, env = get_or_create_var ~loc env in
+ let clause_card = Datatype.String.Set.cardinal bhvrs in
+ let env, complete_msg, disjoint_msg =
+ if Datatype.Int.equal clause_card contract.named_behaviors_count then
+ let env =
+ Rtl_call.partial_count_all_behaviors
+ ~loc
+ ~result:vi
+ env
+ kf
+ contract_e
+ in
+ let complete_msg = "all behaviors complete" in
+ let disjoint_msg = "all behaviors disjoint" in
+ env, complete_msg, disjoint_msg
+ else
+ let args, bhvrs_names =
+ Datatype.String.Set.fold
+ (fun bhvr_name (args, bhvrs_names) ->
+ let args = get_bhvr_idx contract bhvr_name :: args in
+ let bhvrs_names = bhvr_name :: bhvrs_names in
+ args, bhvrs_names)
+ bhvrs
+ ([], [])
+ in
+ let env =
+ Rtl_call.partial_count_behaviors
+ ~loc
+ ~result:vi
+ env
+ kf
+ contract_e
+ args
+ in
+ let bhvrs_names = String.concat ", " bhvrs_names in
+ let complete_msg =
+ Format.sprintf "complete behaviors %s" bhvrs_names
+ in
+ let disjoint_msg =
+ Format.sprintf "disjoint behaviors %s" bhvrs_names
+ in
+ env, complete_msg, disjoint_msg
+ in
+ e, complete_msg, disjoint_msg, env
+ in
+
+ (* Create assertions for complete and disjoint behaviors checks *)
+ let create_assert_stmt bop msg =
+ Smart_stmt.runtime_check_with_msg
+ ~loc
+ msg
+ (Env.annotation_kind env)
+ kf
+ (Cil.mkBinOp ~loc bop active_bhvrs_e (Cil.one ~loc))
+ in
+ let assert_complete_stmt = create_assert_stmt Ge complete_msg in
+ let assert_disjoint_stmt = create_assert_stmt Le disjoint_msg in
+
+ if must_translate_complete && must_translate_disjoint then
+ (* Build an enclosing [if] if both complete and disjoint must be checked
+ for the given clause *)
+ Env.add_stmt
+ env
+ kf
+ (Smart_stmt.if_stmt
+ ~loc
+ ~cond:(Cil.mkBinOp ~loc Ne active_bhvrs_e (Cil.one ~loc))
+ (Cil.mkBlock [ assert_complete_stmt; assert_disjoint_stmt ]))
+ (* Otherwise just get the corresponding assertion *)
+ else if must_translate_complete then
+ Env.add_stmt env kf assert_complete_stmt
+ else if must_translate_disjoint then
+ Env.add_stmt env kf assert_disjoint_stmt
+ else
+ (* By construction, at least either [must_translate_complete] or
+ [must_translate_disjoint] is true *)
+ assert false
+ else
+ (* Nothing to translate *)
+ env
+ in
+ fold_left_handle_error do_clause env clauses
+
+(** Insert complete and disjoint behaviors check for the given contract in the
+ environement *)
+let check_complete_and_disjoint kf kinstr env contract =
+ (* Only translate the complete and disjoint clauses if all the assumes clauses
+ could be translated *)
+ if contract.all_assumes_translated then
+ (* Partition the complete and disjoint clauses of the contract into 3 lists:
+ - The complete and disjoint list
+ - The complete list
+ - The disjoint list
+
+ The behaviors of a clause are stored in a Set so that they are
+ automatically sorted, the duplicates are removed, and they can be compared
+ for equality.
+ *)
+ let completes =
+ List.map
+ Datatype.String.Set.of_list
+ contract.spec.spec_complete_behaviors
+ in
+ let completes_and_disjoints, completes, disjoints =
+ List.fold_left
+ (fun (completes_and_disjoints, completes, disjoints) clause ->
+ let clause = Datatype.String.Set.of_list clause in
+ if List.mem clause completes then
+ let completes_and_disjoints = clause :: completes_and_disjoints in
+ let completes =
+ List.filter
+ (fun c -> not (Datatype.String.Set.equal clause c))
+ completes
+ in
+ completes_and_disjoints, completes, disjoints
+ else
+ let disjoints = clause :: disjoints in
+ completes_and_disjoints, completes, disjoints
+ )
+ ([], completes, [])
+ contract.spec.spec_disjoint_behaviors
+ in
+ (* Create a common variable to hold the number of active behavior for the
+ current check *)
+ let get_or_create_var = mk_get_or_create_var kf Cil.intType "active_bhvrs" in
+ (* Check the complete and disjoint clauses *)
+ let check_bhvrs env ppt_to_translate bhvrs =
+ check_active_behaviors
+ ~ppt_to_translate
+ ~get_or_create_var
+ kf
+ kinstr
+ env
+ contract
+ bhvrs
+ in
+ let env = check_bhvrs env Both completes_and_disjoints in
+ let env = check_bhvrs env Complete completes in
+ let env = check_bhvrs env Disjoint disjoints in
+ env
+ else begin
+ Cil.CurrentLoc.set contract.location;
+ Options.warning
+ ~current:true
+ "@[Some assumes clauses couldn't be translated.@ Ignoring complete and \
+ disjoint behaviors annotations.@]";
+ env
+ end
+
+(** Insert ensures check for the given contract in the environement *)
+let check_post_conds kf kinstr env contract =
+ let get_or_create_assumes_var =
+ mk_get_or_create_var kf Cil.intType "assumes_value"
+ in
+ let do_behavior env b =
+ let env =
+ Env.handle_error
+ (fun env ->
+ let active = [] in (* TODO: 'for' behaviors, e-acsl#109 *)
+ let ppt = Property.ip_assigns_of_behavior kf kinstr ~active b in
+ if b.b_assigns <> WritesAny && !must_translate_ppt_opt_ref ppt
+ then Env.not_yet env "assigns clause in behavior";
+ (* ignore b.b_extended since we never translate them *)
+ env)
+ env
+ in
+ if Cil.is_default_behavior b then
+ fold_left_handle_error
+ (fun env ((termination, post_cond) as tp) ->
+ if !must_translate_ppt_ref
+ (Property.ip_of_ensures kf kinstr b tp) then
+ let post_cond = ensures_predicate post_cond in
+ let loc = post_cond.pred_loc in
+ Cil.CurrentLoc.set loc;
+ match termination with
+ | Normal ->
+ (* If translating the default behavior, directly translate the
+ predicate *)
+ Translate.translate_predicate kf env post_cond
+ | Exits | Breaks | Continues | Returns ->
+ Error.process_error
+ (Error.not_yet "abnormal termination case in behavior");
+ env
+ else
+ env)
+ env
+ b.b_post_cond
+ else
+ (* Compute the assumes predicate for pretty printing *)
+ let assumes = assumes_predicate b.b_assumes in
+ (* Push a new env and check the ensures of the behavior *)
+ let env = Env.push env in
+ let env, stmts =
+ fold_left_handle_error_with_args
+ (fun (env, stmts) ((termination, post_cond) as tp) ->
+ if !must_translate_ppt_ref
+ (Property.ip_of_ensures kf kinstr b tp) then
+ let post_cond = ensures_predicate post_cond in
+ let loc = post_cond.pred_loc in
+ Cil.CurrentLoc.set loc;
+ match termination with
+ | Normal ->
+ (* Prepend the name of the behavior *)
+ let post_cond =
+ { post_cond with pred_name = b.b_name :: post_cond.pred_name }
+ in
+ (* Create runtime check *)
+ let post_cond_e, env =
+ Translate.generalized_untyped_predicate_to_exp kf env post_cond
+ in
+ let stmt =
+ Smart_stmt.runtime_check
+ Smart_stmt.Postcondition
+ kf
+ post_cond_e
+ post_cond
+ in
+ env, stmt :: stmts
+ | Exits | Breaks | Continues | Returns ->
+ Error.process_error (Error.not_yet "abnormal termination case in behavior");
+ env, stmts
+ else
+ env, stmts)
+ (env, [])
+ b.b_post_cond
+ in
+ let post_cond = Smart_stmt.block_from_stmts stmts in
+ (* Pop the env to build the post_cond check *)
+ let post_cond_blk, env =
+ Env.pop_and_get
+ env
+ post_cond
+ ~global_clear:false
+ Env.Middle
+ in
+ match stmts with
+ | [] ->
+ (* If no post_cond check have been generated, then return immediately *)
+ env
+ | _ :: _ ->
+ (* Generate a predicate that retrieves and tests the already
+ computed assumes value for the behavior *)
+ let loc = assumes.pred_loc in
+ let assumes_vi, assumes_e, env =
+ get_or_create_assumes_var ~loc env
+ in
+ let _, contract_e = get_contract_var contract in
+ let idx = get_bhvr_idx contract b.b_name in
+ let env =
+ Rtl_call.get_assumes
+ ~loc
+ ~result:assumes_vi
+ env
+ kf
+ contract_e
+ idx
+ in
+ let stmt = Smart_stmt.if_stmt ~loc ~cond:assumes_e post_cond_blk in
+ Env.add_stmt env kf stmt
+ in
+ List.fold_left
+ do_behavior
+ env
+ contract.spec.spec_behavior
+
+let translate_preconditions kf kinstr env contract =
+ let env = Env.set_annotation_kind env Smart_stmt.Precondition in
+ let env = Env.push_contract env contract in
+ let env = init kf env contract in
+ let env = setup_assumes kf env contract in
+ let do_it env =
+ let env = check_requires kf kinstr env contract in
+ let env = check_complete_and_disjoint kf kinstr env contract in
+ env
+ in
+ Env.handle_error do_it env
+
+let translate_postconditions kf kinstr env =
+ let env = Env.set_annotation_kind env Smart_stmt.Postcondition in
+ let contract, env = Env.pop_and_get_contract env in
+ let do_it env =
+ let env = check_post_conds kf kinstr env contract in
+ env
+ in
+ let env = Env.handle_error do_it env in
+ cleanup kf env contract
diff --git a/src/plugins/e-acsl/src/code_generator/contract.mli b/src/plugins/e-acsl/src/code_generator/contract.mli
new file mode 100644
index 0000000000000000000000000000000000000000..0b7732602334736cc9d258c4867bd6b57e028f66
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/contract.mli
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(* *)
+(* 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
+open Contract_types
+
+(** Translate a given ACSL contract (function or statement) into the
+ corresponding C statement for runtime assertion checking. *)
+
+type t = contract
+
+val create: loc:location -> spec -> t
+(** Create a contract from a [spec] object (either function spec or statement
+ spec) *)
+
+val translate_preconditions: kernel_function -> kinstr -> Env.t -> t -> Env.t
+(** Translate the preconditions of the given contract into the environement *)
+
+val translate_postconditions: kernel_function -> kinstr -> Env.t -> Env.t
+(** Translate the postconditions of the given contract into the environment *)
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val must_translate_ppt_ref: (Property.t -> bool) ref
+
+val must_translate_ppt_opt_ref: (Property.t option -> bool) ref
diff --git a/src/plugins/e-acsl/src/code_generator/contract_types.mli b/src/plugins/e-acsl/src/code_generator/contract_types.mli
new file mode 100644
index 0000000000000000000000000000000000000000..adef414cc84636870d1c2d5167cf48384e6958e5
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/contract_types.mli
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(* *)
+(* 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
+
+(** Represent a function or statement contract. *)
+type contract = {
+ location: location;
+ (** Location of the function or statement attached to the contract. *)
+
+ named_behaviors_count: int;
+ (** Number of named behaviors in the contract
+ (excluding the default behavior) *)
+
+ name_to_idx_tbl: (string, int) Hashtbl.t;
+ (** Hashtable associating the name of a behavior with its index in the C API
+ structure used to store behaviors information at runtime. *)
+
+ mutable var: (varinfo * exp) option;
+ (** Elements to access the C API structure used to store contracts
+ information at runtime. *)
+
+ mutable all_assumes_translated: bool;
+ (** True if all the assumes clauses of the contract could be translated, false
+ otherwise.
+
+ If even one assume clause can't be translated, then the complete and
+ disjoint clauses can't be computed. *)
+
+ spec: spec
+ (** Specification for the contract *)
+}
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 5466f4cc98c85758ad4fc64e6091625ffc7e6097..595dc566e1e836413c056e3c2c462ff3fedcf11a 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -23,6 +23,7 @@
module E_acsl_label = Label
open Cil_types
open Cil_datatype
+open Contract_types
type localized_scope =
| LGlobal
@@ -62,6 +63,8 @@ type t = {
should be added. *)
global_mp_tbl: mp_tbl;
env_stack: local_env list;
+ contract_stack: contract list;
+ (* Stack of contracts for active functions and statements *)
var_mapping: Varinfo.t Stack.t Logic_var.Map.t;
(* records of C bindings for logic vars *)
loop_invariants: predicate list list;
@@ -92,6 +95,7 @@ let empty =
new_global_vars = [];
global_mp_tbl = empty_mp_tbl;
env_stack = [];
+ contract_stack = [];
var_mapping = Logic_var.Map.empty;
loop_invariants = [];
cpt = 0 }
@@ -508,6 +512,23 @@ let untypable env s =
Context.save env;
Error.untypable s
+let push_contract env contract =
+ { env with contract_stack = contract :: env.contract_stack }
+
+let top_contract env =
+ match env.contract_stack with
+ | [] -> Options.fatal "Contract list is empty in env. That is unexpected"
+ | hd :: tl -> hd, tl
+
+let pop_and_get_contract env =
+ let hd, tl = top_contract env in
+ hd, { env with contract_stack = tl }
+
+let pop_contract env =
+ let _, env = pop_and_get_contract env in
+ env
+
+
(* debugging purpose *)
let pretty fmt env =
let local_env, _ = top env in
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 065d3babd2b2ec1c93d9d6661ba6eb7408b264ff..3a5aebf2f5d4f1a0ea67af77099032535365f8e7 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Contract_types
(** Environments.
@@ -192,6 +193,19 @@ val not_yet: t -> string -> 'a
val untypable: t -> string -> 'a
(** Save the current context and raise [Error.Typing_error] exception. *)
+(* ************************************************************************** *)
+(** {2 Contracts} *)
+(* ************************************************************************** *)
+
+val push_contract: t -> contract -> t
+(** Push a contract to the environment's stack *)
+val top_contract: t -> contract * contract list
+(** Return the top contract of the environment's stack *)
+val pop_and_get_contract: t -> contract * t
+(** Pop and return the top contract of the environment's stack *)
+val pop_contract: t -> t
+(** Pop the top contract of the environment's stack *)
+
val pretty: Format.formatter -> t -> unit
(*