From 8dbfc4926113489f514b19d17510821a4059f349 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 21 Dec 2011 17:40:22 +0000
Subject: [PATCH] better modularisation
---
src/plugins/e-acsl/Makefile.in | 12 +-
src/plugins/e-acsl/TODO | 2 +-
src/plugins/e-acsl/quantif.ml | 233 +++++++++++++++++++++++++
src/plugins/e-acsl/quantif.mli | 41 +++++
src/plugins/e-acsl/typing.ml | 117 +++++++++++++
src/plugins/e-acsl/typing.mli | 38 +++++
src/plugins/e-acsl/visit.ml | 301 ++-------------------------------
7 files changed, 453 insertions(+), 291 deletions(-)
create mode 100644 src/plugins/e-acsl/quantif.ml
create mode 100644 src/plugins/e-acsl/quantif.mli
create mode 100644 src/plugins/e-acsl/typing.ml
create mode 100644 src/plugins/e-acsl/typing.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index b088a3edf52..d1de8fd647b 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -33,7 +33,17 @@ PLUGIN_DIR ?=.
PLUGIN_ENABLE:=@ENABLE_E_ACSL@
PLUGIN_DYNAMIC:=@DYNAMIC_E_ACSL@
PLUGIN_NAME:=E_ACSL
-PLUGIN_CMO:= local_config options read_header error misc mpz env visit main
+PLUGIN_CMO:= local_config \
+ options \
+ read_header \
+ error \
+ misc \
+ mpz \
+ env \
+ typing \
+ quantif \
+ visit \
+ main
PLUGIN_HAS_MLI:=yes
# Enable -warn-error, but do not distribute the plug-in with this option being
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 196b0a77559..2b21ec90db9 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -66,7 +66,7 @@
- test sizeof.i devraient être plus précis quand logic_typing plus précis
- structs
- unions
-- quantifications entières invalides
+- inclure exemple du E-ACSL Reference Manual
####################
# AVANT LA DISTRIB #
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
new file mode 100644
index 00000000000..b78a919472f
--- /dev/null
+++ b/src/plugins/e-acsl/quantif.ml
@@ -0,0 +1,233 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the E-ACSL plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2011 *)
+(* 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 Cil
+open Cil_datatype
+
+let named_predicate_to_exp_ref
+ : (Env.t -> predicate named -> exp * Env.t) ref
+ = Extlib.mk_fun "named_predicate_to_exp_ref"
+
+let term_to_exp_ref
+ : (Env.t -> logic_type -> term -> exp * Env.t) ref
+ = Extlib.mk_fun "term_to_exp_ref"
+
+let compute_quantif_guards quantif bounded_vars hyps =
+ let error msg pp x =
+ let msg1 = Pretty_utils.sfprintf msg pp x in
+ let msg2 =
+ Pretty_utils.sfprintf "@[ in quantification@ %a@]"
+ d_predicate_named quantif
+ in
+ Error.untypable (msg1 ^ msg2)
+ in
+ let rec aux acc vars p =
+ match p.content with
+ | Pand({ content = Prel((Rlt | Rle) as r1, t11, t12) },
+ { content = Prel((Rlt | Rle) as r2, t21, t22) }) ->
+ (match t12.term_node, t21.term_node with
+ | TLval(TVar x1, TNoOffset), TLval(TVar x2, TNoOffset) ->
+ let v, vars = match vars with
+ | [] -> error "@[too much constraint(s)%a@]" (fun _ () -> ()) ()
+ | v :: tl ->
+ match v.lv_type with
+ | Ctype ty when isIntegralType ty -> v, tl
+ | Linteger -> v, tl
+ | Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
+ error "@[non integer variable %a@]" d_logic_var v
+ in
+ if Logic_var.equal x1 x2 && Logic_var.equal x1 v then
+ (t11, r1, x1, r2, t22) :: acc, vars
+ else
+ error "@[invalid binder %a@]" d_term t21
+ | TLval _, _ -> error "@[invalid binder %a@]" d_term t21
+ | _, _ -> error "@[invalid binder %a@]" d_term t12)
+ | Pand(p1, p2) ->
+ let acc, vars = aux acc vars p1 in
+ aux acc vars p2
+ | _ -> error "@[invalid guard %a@]" d_predicate_named p
+ in
+ let acc, vars = aux [] bounded_vars hyps in
+ (match vars with
+ | [] -> ()
+ | _ :: _ ->
+ let msg =
+ Pretty_utils.sfprintf
+ "@[unguarded variable%s %tin quantification@ %a@]"
+ (if List.length vars = 1 then "" else "s")
+ (fun fmt ->
+ List.iter (fun v -> Format.fprintf fmt "@[%a @]" d_logic_var v) vars)
+ d_predicate_named quantif
+ in
+ Error.untypable msg);
+ List.rev acc
+
+module Label_ids =
+ State_builder.Counter(struct let name = "E_ACSL.Label_ids" end)
+
+let convert env loc p bounded_vars hyps goal =
+ let named_predicate_to_exp = !named_predicate_to_exp_ref in
+ let term_to_exp = !term_to_exp_ref in
+ (* universal quantification over integers (or a subtype of integer) *)
+ let guards = compute_quantif_guards p bounded_vars hyps in
+ let env = List.fold_left Env.Logic_binding.add env bounded_vars in
+ let var_res = ref Varinfo.dummy in
+ let res, env =
+ (* variable storing the result of the \forall *)
+ Env.new_var env None intType
+ (fun v _ ->
+ var_res := v;
+ let lv = var v in
+ [ mkStmtOneInstr ~valid_sid:true (Set(lv, one ~loc, loc)) ])
+ in
+ let end_loop_ref = ref dummyStmt in
+ let rec mk_for_loop env = function
+ | [] ->
+ (* innermost loop body: store the result in [res] and go out according
+ to evaluation of the goal *)
+ let test, env = named_predicate_to_exp (Env.push env) goal in
+ let then_block = mkBlock [ mkEmptyStmt ~loc () ] in
+ let else_block =
+ (* use a 'goto', not a simple 'break' in order to handle 'forall' with
+ multiple binders (leading to imbricated loops) *)
+ mkBlock
+ [ mkStmtOneInstr
+ ~valid_sid:true (Set(var !var_res, zero ~loc, loc));
+ mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
+ in
+ let blk, env =
+ Env.pop_and_get
+ env
+ (mkStmt ~valid_sid:true (If(test, then_block, else_block, loc)))
+ ~global_clear:false
+ Env.After
+ in
+ (* TODO: could be optimised if [pop_and_get] would return a list of
+ stmts *)
+ [ mkStmt ~valid_sid:true (Block blk) ], env
+ | (t1, rel1, logic_x, rel2, t2) :: tl ->
+ let body, env = mk_for_loop env tl in
+ let t_plus_one t =
+ Logic_const.term ~loc
+ (TBinOp(PlusA, t, Logic_const.tinteger ~loc ~ikind:IChar 1))
+ Linteger
+ in
+ let t1 = match rel1 with
+ | Rlt -> t_plus_one t1
+ | Rle -> t1
+ | Rgt | Rge | Req | Rneq -> assert false
+ in
+ let bop2 = match rel2 with
+ | Rlt -> Lt
+ | Rle -> Le
+ | Rgt | Rge | Req | Rneq -> assert false
+ in
+ (* we increment the loop counter one more time (at the end of the
+ loop). Thus to prevent overflow, check the type of [t2 + 1] instead
+ of [t2]. *)
+ let ty = Typing.principal_type_from_term t1 (t_plus_one t2) in
+ let ty = Typing.principal_type ty logic_x.lv_type in
+ (* loop counter corresponding to the quantified variable *)
+ let var_x = Env.Logic_binding.get env logic_x in
+ let lv_x = var var_x in
+ let x = new_exp ~loc (Lval lv_x) in
+ let env = match ty with
+ | Ctype ty when isIntegralType ty ->
+ var_x.vtype <- ty;
+ env
+ | Linteger ->
+ var_x.vtype <- Mpz.t;
+ Env.add_stmt env (Mpz.init x)
+ | Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ -> assert false
+ in
+ (* initialize the loop counter to [t1] *)
+ let e1, env = term_to_exp (Env.push env) ty t1 in
+ let init_blk, env =
+ Env.pop_and_get
+ env
+ (Mpz.affect lv_x x e1)
+ ~global_clear:false
+ Env.Middle
+ in
+ (* generate the guard [x bop t2] *)
+ let stmts_block b = [ mkStmt ~valid_sid:true (Block b) ] in
+ let tlv = Logic_const.tvar ~loc (cvar_to_lvar var_x) in
+ let guard_exp, env =
+ term_to_exp
+ (Env.push env)
+ (Ctype intType)
+ (Logic_const.term (TBinOp(bop2, tlv, t2)) ty)
+ in
+ let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
+ let guard_blk, env =
+ Env.pop_and_get
+ env
+ (mkStmt ~valid_sid:true
+ (If(guard_exp,
+ mkBlock [ mkEmptyStmt () ],
+ mkBlock [ break_stmt ],
+ guard_exp.eloc)))
+ ~global_clear:false
+ Env.Middle
+ in
+ let guard = stmts_block guard_blk in
+ (* increment the loop counter [x++] *)
+ let incr, env = term_to_exp (Env.push env) ty (t_plus_one tlv) in
+ let next_blk, env =
+ Env.pop_and_get
+ env
+ (Mpz.affect lv_x x incr)
+ ~global_clear:false
+ Env.Middle
+ in
+ (* generate the whole loop *)
+ let start = stmts_block init_blk in
+ let next = stmts_block next_blk in
+ start @
+ [ mkStmt ~valid_sid:true
+ (Loop ([],
+ mkBlock (guard @ body @ next),
+ loc,
+ None,
+ Some break_stmt)) ],
+ env
+ in
+ let stmts, env = mk_for_loop env guards in
+ let env =
+ Env.add_stmt env (mkStmt ~valid_sid:true (Block (mkBlock stmts)))
+ in
+ (* where to jump to go out of the loop *)
+ let end_loop = mkEmptyStmt ~loc () in
+ let label_name = "e_acsl_end_loop" ^ string_of_int (Label_ids.next ()) in
+ let label = Label(label_name, loc, false) in
+ end_loop.labels <- label :: end_loop.labels;
+ end_loop_ref := end_loop;
+ let env = Env.add_stmt env end_loop in
+ let env = List.fold_left Env.Logic_binding.remove env bounded_vars in
+ res, env
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)
diff --git a/src/plugins/e-acsl/quantif.mli b/src/plugins/e-acsl/quantif.mli
new file mode 100644
index 00000000000..0c0361abb43
--- /dev/null
+++ b/src/plugins/e-acsl/quantif.mli
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the E-ACSL plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2011 *)
+(* 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 convert:
+ Env.t ->
+ location ->
+ predicate named ->
+ logic_var list ->
+ predicate named ->
+ predicate named ->
+ exp * Env.t
+
+val named_predicate_to_exp_ref: (Env.t -> predicate named -> exp * Env.t) ref
+val term_to_exp_ref: (Env.t -> logic_type -> term -> exp * Env.t) ref
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
new file mode 100644
index 00000000000..7c0625fce18
--- /dev/null
+++ b/src/plugins/e-acsl/typing.ml
@@ -0,0 +1,117 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the E-ACSL plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2011 *)
+(* 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 Cil
+
+let compatible_type ty ty' =
+ (* compatible if the two type has the same "integrality" *)
+ isIntegralType ty = isIntegralType ty'
+
+(* convert [e] corresponding to a term of type [ty] in a way that it is
+ compatible with the given context. *)
+let context_sensitive ?loc env ctx is_mpz_string t_opt e =
+ let ty = typeOf e in
+ let mk_mpz env e =
+ Env.new_var env t_opt Mpz.t (fun lv v -> [ Mpz.init_set (var lv) v e ])
+ in
+ let do_int_ctx ty' =
+ let e, env = if is_mpz_string then mk_mpz env e else e, env in
+ if Mpz.is_t ty || is_mpz_string then
+ (* cast the mpz into a C integer *)
+ let name =
+ if isSignedInteger ty' then "__gmpz_get_si" else "__gmpz_get_ui"
+ in
+ Options.warning
+ ?source:(Extlib.opt_map fst loc)
+ ~once:true
+ "@[missing guard for ensuring that the given integer is \
+C-representable@]";
+ Env.new_var
+ env
+ None
+ ty'
+ (fun v _ -> [ Misc.mk_call ?loc ~result:(var v) name [ e ] ])
+ else
+ e, env
+ in
+ match ctx with
+ | Ctype ty' -> do_int_ctx ty'
+ | Linteger ->
+ if Mpz.is_t ty then
+ e, env
+ else begin
+ (* Convert the C integer into a mpz.
+ Remember: very long integer constant has been temporary converted into
+ strings *)
+ assert (Options.verify
+ (isIntegralType ty || is_mpz_string)
+ "how to convert %a to an integer?"
+ d_type ty);
+ mk_mpz env e
+ end
+ | ty' when Logic_const.is_boolean_type ty' -> do_int_ctx intType
+ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
+ (* not yet supported, thus cannot occur at this point *)
+ assert false
+
+let principal_type ty ty' = match ty, ty' with
+ | Ctype ty, Ctype ty' when isIntegralType ty ->
+ assert (isIntegralType ty');
+ Ctype (arithmeticConversion ty ty')
+ | Ctype ty, Linteger | Linteger, Ctype ty when isIntegralType ty -> Linteger
+ (* not possible to unify cases below (see caml bts #5432) *)
+ | Ctype ty1, Ctype ty2 when Mpz.is_t ty1 && isIntegralType ty2 -> Linteger
+ | Ctype ty2, Ctype ty1 when Mpz.is_t ty1 && isIntegralType ty2 -> Linteger
+ | Ctype tty, Ctype tty' ->
+ assert (compatible_type tty tty');
+ ty
+ | Ctype _, Linteger | Linteger, Ctype _ -> Linteger
+ | Linteger, Linteger -> Linteger
+ | (Ltype _ | Lvar _ | Lreal | Larrow _), _
+ | _, (Ltype _ | Lvar _ | Lreal | Larrow _) ->
+ (* not yet supported, thus cannot occur at this point *)
+ Options.error "What is this %a here?" d_logic_type ty';
+ assert false
+
+let principal_type_from_term t1 t2 =
+ let typ t =
+ let ty = t.term_type in
+ if Logic_const.is_boolean_type ty then Ctype intType
+ else match t.term_node, ty with
+ | TConst (CInt64(_, (ILongLong | IULongLong), _)), Linteger ->
+ (* constant potentially not representable in C *)
+ Linteger
+ | TConst (CInt64(_, k, _)), _ ->
+ (* C-representable constant *)
+ Ctype (TInt (k, []))
+ | _, _ ->
+ (* for direct C terms, should be able to infer the corresponding C type *)
+ ty
+ in
+ principal_type (typ t1) (typ t2)
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
new file mode 100644
index 00000000000..b115f54ef90
--- /dev/null
+++ b/src/plugins/e-acsl/typing.mli
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the E-ACSL plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2011 *)
+(* 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
+
+(** Typing rules. *)
+
+val principal_type: logic_type -> logic_type -> logic_type
+val principal_type_from_term: term -> term -> logic_type
+
+val context_sensitive:
+ ?loc:location -> Env.t -> logic_type -> bool -> term option -> exp ->
+ exp * Env.t
+
+(*
+Local Variables:
+compile-command: "make"
+End:
+*)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index ac7c267ad64..b1418f57e1f 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -24,98 +24,6 @@ open Cil_types
open Cil_datatype
open Cil
-(* ************************************************************************** *)
-(* Typing rules *)
-(* ************************************************************************** *)
-
-let compatible_type ty ty' =
- (* compatible if the two type has the same "integrality" *)
- isIntegralType ty = isIntegralType ty'
-
-(* convert [e] corresponding to a term of type [ty] in a way that it is
- compatible with the given context. *)
-let context_sensitive ?loc env ctx is_mpz_string t_opt e =
- let ty = typeOf e in
- let mk_mpz env e =
- Env.new_var env t_opt Mpz.t (fun lv v -> [ Mpz.init_set (var lv) v e ])
- in
- let do_int_ctx ty' =
- let e, env = if is_mpz_string then mk_mpz env e else e, env in
- if Mpz.is_t ty || is_mpz_string then
- (* cast the mpz into a C integer *)
- let name =
- if isSignedInteger ty' then "__gmpz_get_si" else "__gmpz_get_ui"
- in
- Options.warning
- ?source:(Extlib.opt_map fst loc)
- ~once:true
- "@[missing guard for ensuring that the given integer is \
-C-representable@]";
- Env.new_var
- env
- None
- ty'
- (fun v _ -> [ Misc.mk_call ?loc ~result:(var v) name [ e ] ])
- else
- e, env
- in
- match ctx with
- | Ctype ty' -> do_int_ctx ty'
- | Linteger ->
- if Mpz.is_t ty then
- e, env
- else begin
- (* Convert the C integer into a mpz.
- Remember: very long integer constant has been temporary converted into
- strings *)
- assert (Options.verify
- (isIntegralType ty || is_mpz_string)
- "how to convert %a to an integer?"
- d_type ty);
- mk_mpz env e
- end
- | ty' when Logic_const.is_boolean_type ty' -> do_int_ctx intType
- | Ltype _ | Lvar _ | Lreal | Larrow _ ->
- (* not yet supported, thus cannot occur at this point *)
- assert false
-
-let principal_type ty ty' = match ty, ty' with
- | Ctype ty, Ctype ty' when isIntegralType ty ->
- assert (isIntegralType ty');
- Ctype (arithmeticConversion ty ty')
- | Ctype ty, Linteger | Linteger, Ctype ty when isIntegralType ty -> Linteger
- (* both cases below should be unified, but it is not possible because of
- caml bts #5432 *)
- | Ctype ty1, Ctype ty2 when Mpz.is_t ty1 && isIntegralType ty2 -> Linteger
- | Ctype ty2, Ctype ty1 when Mpz.is_t ty1 && isIntegralType ty2 -> Linteger
- | Ctype tty, Ctype tty' ->
- assert (compatible_type tty tty');
- ty
- | Ctype _, Linteger | Linteger, Ctype _ -> Linteger
- | Linteger, Linteger -> Linteger
- | (Ltype _ | Lvar _ | Lreal | Larrow _), _
- | _, (Ltype _ | Lvar _ | Lreal | Larrow _) ->
- (* not yet supported, thus cannot occur at this point *)
- Options.error "What is this %a here?" d_logic_type ty';
- assert false
-
-let principal_type_from_term t1 t2 =
- let typ t =
- let ty = t.term_type in
- if Logic_const.is_boolean_type ty then Ctype intType
- else match t.term_node, ty with
- | TConst (CInt64(_, (ILongLong | IULongLong), _)), Linteger ->
- (* constant potentially not representable in C *)
- Linteger
- | TConst (CInt64(_, k, _)), _ ->
- (* C-representable constant *)
- Ctype (TInt (k, []))
- | _, _ ->
- (* for direct C terms, should be able to infer the corresponding C type *)
- ty
- in
- principal_type (typ t1) (typ t2)
-
(* ************************************************************************** *)
(* Transforming terms and predicates into C expressions (if any) *)
(* ************************************************************************** *)
@@ -144,60 +52,6 @@ let is_representable _n k _s = match k with
| ILongLong | IULongLong ->
false
-let compute_quantif_guards quantif bounded_vars hyps =
- let error msg pp x =
- let msg1 = Pretty_utils.sfprintf msg pp x in
- let msg2 =
- Pretty_utils.sfprintf "@[ in quantification@ %a@]"
- d_predicate_named quantif
- in
- Error.untypable (msg1 ^ msg2)
- in
- let rec aux acc vars p =
- match p.content with
- | Pand({ content = Prel((Rlt | Rle) as r1, t11, t12) },
- { content = Prel((Rlt | Rle) as r2, t21, t22) }) ->
- (match t12.term_node, t21.term_node with
- | TLval(TVar x1, TNoOffset), TLval(TVar x2, TNoOffset) ->
- let v, vars = match vars with
- | [] -> error "@[too much constraint(s)%a@]" (fun _ () -> ()) ()
- | v :: tl ->
- match v.lv_type with
- | Ctype ty when isIntegralType ty -> v, tl
- | Linteger -> v, tl
- | Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
- error "@[non integer variable %a@]" d_logic_var v
- in
- if Logic_var.equal x1 x2 && Logic_var.equal x1 v then
- (t11, r1, x1, r2, t22) :: acc, vars
- else
- error "@[invalid binder %a@]" d_term t21
- | TLval _, _ -> error "@[invalid binder %a@]" d_term t21
- | _, _ -> error "@[invalid binder %a@]" d_term t12)
- | Pand(p1, p2) ->
- let acc, vars = aux acc vars p1 in
- aux acc vars p2
- | _ -> error "@[invalid guard %a@]" d_predicate_named p
- in
- let acc, vars = aux [] bounded_vars hyps in
- (match vars with
- | [] -> ()
- | _ :: _ ->
- let msg =
- Pretty_utils.sfprintf
- "@[unguarded variable%s %tin quantification@ %a@]"
- (if List.length vars = 1 then "" else "s")
- (fun fmt ->
- List.iter (fun v -> Format.fprintf fmt "@[%a @]" d_logic_var v) vars)
- d_predicate_named quantif
- in
- Error.untypable msg);
- List.rev acc
-
-
-module Label_ids =
- State_builder.Counter(struct let name = "E_ACSL.Label_ids" end)
-
let constant_to_exp ?(loc=Location.unknown) = function
| CInt64(n, k, s) ->
if is_representable n k s then kinteger64_repr ?loc k n s, false
@@ -301,7 +155,7 @@ and context_insensitive_term_to_exp env t =
e, env, false
| TBinOp(Div | Mod as bop, t1, t2) ->
(* arithmetic binary operator potentially convertible into C *)
- let ctx = principal_type_from_term t1 t2 in
+ let ctx = Typing.principal_type_from_term t1 t2 in
let e1, env = term_to_exp env ctx t1 in
let e2, env = term_to_exp env ctx t2 in
(* guarding divisions and modulos *)
@@ -438,22 +292,23 @@ and context_insensitive_term_to_exp env t =
constructs. *)
and term_to_exp env ctx t =
let e, env, is_mpz_string = context_insensitive_term_to_exp env t in
- context_sensitive ~loc:t.term_loc env ctx is_mpz_string (Some t) e
+ Typing.context_sensitive ~loc:t.term_loc env ctx is_mpz_string (Some t) e
(* generate the C code equivalent to [t1 bop t2]. *)
and comparison_to_exp ?(loc=Location.unknown) ?e1 env bop t1 t2 t_opt =
let ctx = match e1 with
- | None -> principal_type_from_term t1 t2
+ | None -> Typing.principal_type_from_term t1 t2
| Some(_, ctx) ->
(* Options.feedback "principality oriented by %a" d_logic_type ctx;*)
- principal_type_from_term { t1 with term_type = ctx } t2
+ Typing.principal_type_from_term { t1 with term_type = ctx } t2
in
(* Options.feedback "principal type of %a and %a is %a"
d_term t1 d_term t2 d_logic_type ctx;*)
let e1, env = match e1 with
| None -> term_to_exp env ctx t1
| Some(e1, ctx1) when Cil_datatype.Logic_type.equal ctx ctx1 -> e1, env
- | Some(e1, _) -> context_sensitive ~loc:e1.eloc env ctx false (Some t1) e1
+ | Some(e1, _) ->
+ Typing.context_sensitive ~loc:e1.eloc env ctx false (Some t1) e1
in
let e2, env = term_to_exp env ctx t2 in
match ctx with
@@ -483,7 +338,7 @@ let rec named_predicate_to_exp env p =
let e, env =
comparison_to_exp ~loc env (relation_to_binop rel) t1 t2 None
in
- context_sensitive ~loc env (Ctype intType) false None e
+ Typing.context_sensitive ~loc env (Ctype intType) false None e
| Pand(p1, p2) ->
(* p1 && p2 <==> if p1 then p2 else false *)
let e1, env1 = named_predicate_to_exp env p1 in
@@ -532,143 +387,7 @@ let rec named_predicate_to_exp env p =
| Pif _ -> Error.not_yet "_ ? _ : _"
| Plet _ -> Error.not_yet "let _ = _ in _"
| Pforall(bounded_vars, { content = Pimplies(hyps, goal) }) ->
- (* universal quantification over integers (or a subtype of integer) *)
- let guards = compute_quantif_guards p bounded_vars hyps in
- let env = List.fold_left Env.Logic_binding.add env bounded_vars in
- let var_res = ref Varinfo.dummy in
- let res, env =
- (* variable storing the result of the \forall *)
- Env.new_var env None intType
- (fun v _ ->
- var_res := v;
- let lv = var v in
- [ mkStmtOneInstr ~valid_sid:true (Set(lv, one ~loc, loc)) ])
- in
- let end_loop_ref = ref dummyStmt in
- let rec mk_for_loop env = function
- | [] ->
- (* innermost loop body: store the result in [res] and go out according
- to evaluation of the goal *)
- let test, env = named_predicate_to_exp (Env.push env) goal in
- let then_block = mkBlock [ mkEmptyStmt ~loc () ] in
- let else_block =
- (* use a 'goto', not a simple 'break' in order to handle 'forall' with
- multiple binders (leading to imbricated loops) *)
- mkBlock
- [ mkStmtOneInstr
- ~valid_sid:true (Set(var !var_res, zero ~loc, loc));
- mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
- in
- let blk, env =
- Env.pop_and_get
- env
- (mkStmt ~valid_sid:true (If(test, then_block, else_block, loc)))
- ~global_clear:false
- Env.After
- in
- (* TODO: could be optimised if [pop_and_get] would return a list of
- stmts *)
- [ mkStmt ~valid_sid:true (Block blk) ], env
- | (t1, rel1, logic_x, rel2, t2) :: tl ->
- let body, env = mk_for_loop env tl in
- let t_plus_one t =
- Logic_const.term ~loc
- (TBinOp(PlusA, t, Logic_const.tinteger ~loc ~ikind:IChar 1))
- Linteger
- in
- let t1 = match rel1 with
- | Rlt -> t_plus_one t1
- | Rle -> t1
- | Rgt | Rge | Req | Rneq -> assert false
- in
- let bop2 = match rel2 with
- | Rlt -> Lt
- | Rle -> Le
- | Rgt | Rge | Req | Rneq -> assert false
- in
- (* we increment the loop counter one more time (at the end of the
- loop). Thus to prevent overflow, check the type of [t2 + 1] instead
- of [t2]. *)
- let ty = principal_type_from_term t1 (t_plus_one t2) in
- let ty = principal_type ty logic_x.lv_type in
- (* loop counter corresponding to the quantified variable *)
- let var_x = Env.Logic_binding.get env logic_x in
- let lv_x = var var_x in
- let x = new_exp ~loc (Lval lv_x) in
- let env = match ty with
- | Ctype ty when isIntegralType ty ->
- var_x.vtype <- ty;
- env
- | Linteger ->
- var_x.vtype <- Mpz.t;
- Env.add_stmt env (Mpz.init x)
- | Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ -> assert false
- in
- (* initialize the loop counter to [t1] *)
- let e1, env = term_to_exp (Env.push env) ty t1 in
- let init_blk, env =
- Env.pop_and_get
- env
- (Mpz.affect lv_x x e1)
- ~global_clear:false
- Env.Middle
- in
- (* generate the guard [x bop t2] *)
- let stmts_block b = [ mkStmt ~valid_sid:true (Block b) ] in
- let tlv = Logic_const.tvar ~loc (cvar_to_lvar var_x) in
- let guard_exp, env =
- term_to_exp
- (Env.push env)
- (Ctype intType)
- (Logic_const.term (TBinOp(bop2, tlv, t2)) ty)
- in
- let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
- let guard_blk, env =
- Env.pop_and_get
- env
- (mkStmt ~valid_sid:true
- (If(guard_exp,
- mkBlock [ mkEmptyStmt () ],
- mkBlock [ break_stmt ],
- guard_exp.eloc)))
- ~global_clear:false
- Env.Middle
- in
- let guard = stmts_block guard_blk in
- (* increment the loop counter [x++] *)
- let incr, env = term_to_exp (Env.push env) ty (t_plus_one tlv) in
- let next_blk, env =
- Env.pop_and_get
- env
- (Mpz.affect lv_x x incr)
- ~global_clear:false
- Env.Middle
- in
- (* generate the whole loop *)
- let start = stmts_block init_blk in
- let next = stmts_block next_blk in
- start @
- [ mkStmt ~valid_sid:true
- (Loop ([],
- mkBlock (guard @ body @ next),
- loc,
- None,
- Some break_stmt)) ],
- env
- in
- let stmts, env = mk_for_loop env guards in
- let env =
- Env.add_stmt env (mkStmt ~valid_sid:true (Block (mkBlock stmts)))
- in
- (* where to jump to go out of the loop *)
- let end_loop = mkEmptyStmt ~loc () in
- let label_name = "e_acsl_end_loop" ^ string_of_int (Label_ids.next ()) in
- let label = Label(label_name, loc, false) in
- end_loop.labels <- label :: end_loop.labels;
- end_loop_ref := end_loop;
- let env = Env.add_stmt env end_loop in
- let env = List.fold_left Env.Logic_binding.remove env bounded_vars in
- res, env
+ Quantif.convert env loc p bounded_vars hyps goal
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
(* | Pexists(bounded_vars, { content = Pand(hyps, _goal) }) ->
let guards = compute_quantif_guards p bounded_vars hyps in
@@ -688,6 +407,10 @@ let rec named_predicate_to_exp env p =
| Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
| Pinitialized _ -> Error.not_yet "\\initialized"
+let () =
+ Quantif.term_to_exp_ref := term_to_exp;
+ Quantif.named_predicate_to_exp_ref := named_predicate_to_exp
+
(* ************************************************************************** *)
(* [convert_*] converts a given ACSL annotation into the corresponding C
statement (if any) for runtime assertion checking *)
--
GitLab