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

[e-acsl] update headers

[e-acsl] universal quantifiers over integers. Not yet finished: work only in some cases
[e-acsl] logic variables (required by univ quantif)
parent f73cc8dd
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat à l'Énergie Atomique) *)
(* 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 *)
......
##########################################################################
# #
# This file is part of Frama-C. #
# This file is part of the E-ACSL plug-in of Frama-C. #
# #
# Copyright (C) 2007-2010 #
# CEA (Commissariat l'nergie Atomique) #
# 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 #
......@@ -89,6 +90,17 @@ uninstall::
$(PRINT_RM) E-ACSL share files
$(RM) -r $(FRAMAC_SHARE)/e-acsl
##########
# Header #
##########
headers::
@echo "Applying Headers..."
headache -c license/headache_config.txt -h license/CEA_LGPL \
*.ml *.mli \
Makefile.in configure.ac \
share/e-acsl/*.h
################
# Generic part #
################
......
à traiter avant la 1ère release:
- quantifications sans exentension de syntaxe
################
# NEXT RELEASE #
################
- quantifications sur les entiers
- mixed assumes and ensures in contracts
- pas d'arrêt brutal en cas de feature non implémentée
- utiliser Options.use_asserts
########
# CODE #
########
- mixed assumes and ensures
- Env.new_var*: ajouter la varinfo en sortie de la fonction ?
- function contracts for functions only declared
==> le noyau génère un "assigns \nothing" pour ces fonctions...
ce assign n'est de toute façon pas gérer
- multi ensures or multi requirements, their conjunctions and undefinedness
- utiliser Options.use_asserts
[JS 2011/12/06] c'est quoi çà ? :-(
- gestion des initialiseurs des globals: requiert un main
- mkcall ne devrait pas générer de nouvelles variables pour une même fonction
- garde pour les casts quand overflows potentiels
(même pas de warnings aujourd'hui)
- minimiser le nombre de variables générées
- constante entière longue: utiliser la représentation sous forme de string et
rechercher la base appropriée.
- arithmetic overflows
......@@ -38,11 +43,17 @@
- utiliser Rte (get_rte_annotations dans Oxygen)
- [Yannick] Logic functions
- type system for generating C int/float when possible
(generalisation of current Visit.principal_type)
(generalisation of current Visit.principal_type,
nouvelle unité de compilation Typing)
- vérifier le code de la division et du modulo
(div et modulo mathématiques différents des div et modulo de l'ANSI C99)
- customization des noms de variable générés
(par ex pour indiquer le nom de la variable d'origine, ou son rôle)
##############
# KNOWN BUGS #
##############
- \at incorrect si StmtLabel faisant référence au stmt courant (voir test at.i)
- incorrect d'utiliser un \old dans le post-state si pre-state == post-state
......@@ -56,18 +67,11 @@
- test sizeof.i devraient être plus précis quand logic_typing plus précis
- structs
- unions
- quantifications entières invalides
####################
# AVANT LA DISTRIB #
####################
- documentation
- e-acsl implementation manual
en lien avec bts #743:
- user manual
- make distrib
- headers (copyright 2011)
- license
- install répertoire share
VOIR CPAN
##########################################################################
# #
# This file is part of Frama-C. #
# This file is part of the E-ACSL plug-in of Frama-C. #
# #
# Copyright (C) 2007-2010 #
# CEA (Commissariat l'nergie Atomique) #
# 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 #
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat l'nergie Atomique) *)
(* 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 *)
......@@ -43,10 +44,10 @@ type local_env = { block_info: block_info; mpz_tbl: mpz_tbl }
type t =
{ visitor: Visitor.frama_c_visitor;
new_global_vars: varinfo list; (* generated variables at function
level *)
new_global_vars: varinfo list; (* generated variables at function level *)
global_mpz_tbl: mpz_tbl;
env_stack: local_env list;
var_mapping: Varinfo.t Logic_var.Map.t; (* bind logic var to C var *)
cpt: int; (* counter used when generating variables *) }
let empty_block =
......@@ -66,6 +67,7 @@ let dummy =
new_global_vars = [];
global_mpz_tbl = empty_mpz_tbl;
env_stack = [];
var_mapping = Logic_var.Map.empty;
cpt = 0 }
let empty v =
......@@ -73,6 +75,7 @@ let empty v =
new_global_vars = [];
global_mpz_tbl = empty_mpz_tbl;
env_stack = [];
var_mapping = Logic_var.Map.empty;
cpt = 0 }
let top env = match env.env_stack with [] -> assert false | hd :: tl -> hd, tl
......@@ -164,6 +167,32 @@ let new_var ?(global=false) env t ty mk_stmts =
let new_var_and_mpz_init ?global env t mk_stmts =
new_var ?global env t Mpz.t (fun v e -> Mpz.init e :: mk_stmts v e)
module Logic_binding = struct
let add env logic_v =
let v_ref = ref Varinfo.dummy in
let mk v _ = v_ref := v; [] in
let ty =
(* TODO: yet incorrect. Waiting for the type system... *)
match logic_v.lv_type with
| Ctype ty -> ty
| Linteger -> Mpz.t
| Ltype _ | Lvar _ | Lreal | Larrow _ -> assert false
in
let _, env = new_var env None ty mk in
{ env with var_mapping = Logic_var.Map.add logic_v !v_ref env.var_mapping }
let get env logic_v =
try Logic_var.Map.find logic_v env.var_mapping
with Not_found -> assert false
let remove env v =
let map = env.var_mapping in
assert (Logic_var.Map.mem v map);
{ env with var_mapping = Logic_var.Map.remove v map }
end
let current_kf env =
let v = env.visitor in
match v#current_kf with
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat à l'Énergie Atomique) *)
(* 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 *)
......@@ -52,6 +53,12 @@ val new_var_and_mpz_init:
(** Same as [new_var], but dedicated to mpz_t variables initialized by
{!Mpz.init}. *)
module Logic_binding: sig
val add: t -> logic_var -> t
val get: t -> logic_var -> varinfo
val remove: t -> logic_var -> t
end
val add_assert: t -> stmt -> predicate named -> unit
(** [add_assert kf s p] extends the global environment with an assertion [p]
associated to the statement [s] in function [kf]. *)
......@@ -70,14 +77,14 @@ val push: t -> t
type where = Before | Middle | After
val pop_and_get: t -> stmt -> global_clear:bool -> where -> block * t
(* Pop the last local context and get back the corresponding new block
(** Pop the last local context and get back the corresponding new block
containing the given [stmt] at the given place ([Before] is before the
code corresponding to annotations, [After] is after this code and [Middle] is
between the stmt corresponding to annotations and the ones for freeing the
memory. *)
val pop: t -> t
(* Pop the last local context (ignore the corresponding new block if any *)
(** Pop the last local context (ignore the corresponding new block if any *)
val get_generated_variables: t -> varinfo list
(** All the new variables local to the visited function. *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat à l'Énergie Atomique) *)
(* 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 *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat l'nergie Atomique) *)
(* 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 *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat l'nergie Atomique) *)
(* 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 *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat à l'Énergie Atomique) *)
(* 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 *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat l'nergie Atomique) *)
(* 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 *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat l'nergie Atomique) *)
(* 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 *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat l'nergie Atomique) *)
(* 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 *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat à l'Énergie Atomique) *)
(* 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 *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat l'nergie Atomique) *)
(* 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 *)
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat à l'Énergie Atomique) *)
(* 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 *)
......
/**************************************************************************/
/* */
/* 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). */
/* */
/**************************************************************************/
// TODO: remplacer par un e_acsl.h.in
// faire gnrer par le makefile un e_acsl.h
// avec des #include "FRAMAC_SHARE/libc/stdio.h", etc
......
/**************************************************************************/
/* */
/* 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). */
/* */
/**************************************************************************/
/*****************/
/* GMP functions */
......
/**************************************************************************/
/* */
/* 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). */
/* */
/**************************************************************************/
/*************/
/* GMP types */
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* This file is part of the E-ACSL plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2010 *)
(* CEA (Commissariat l'nergie Atomique) *)
(* 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 *)
......@@ -138,6 +139,72 @@ 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 guarded quantification %a"
d_predicate_named quantif
in
Misc.type_error (msg1 ^ msg2)
in
let vars =
let h = Logic_var.Hashtbl.create 7 in
List.iter
(fun v ->
(* only allow quantification over integers *)
(match v.lv_type with
| Ctype ty when isIntegralType ty -> ()
| Linteger -> ()
| Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
error "non integer variable %a" d_logic_var v);
Logic_var.Hashtbl.add h v ())
bounded_vars;
h
in
let used_vars = Logic_var.Hashtbl.create 7 in
let get_guards p =
let rec aux acc 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) ->
if Logic_var.equal x1 x2 then
if Logic_var.Hashtbl.mem vars x1 then begin
Logic_var.Hashtbl.replace used_vars x1 ();
(t11, r1, x1, r2, t22) :: acc
end else
error "unbound variable %a" d_logic_var x1
else
error "invalid guard %a" d_term t21
| TLval _, _ -> error "invalid guard %a" d_term t21
| _, _ -> error "invalid guard %a" d_term t12)
| Pand(p1, p2) -> aux (aux acc p2) p1
| _ -> error "invalid guard %a" d_predicate_named p
in
aux [] p
in
let guards = get_guards hyps in
(* check that all quantifiers are guarded *)
Logic_var.Hashtbl.iter
(fun v () -> Logic_var.Hashtbl.remove vars v)
used_vars;
let len = Logic_var.Hashtbl.length vars in
if len > 0 then begin
let msg =
Pretty_utils.sfprintf
"unguarded variable%s %tin quantification %a"
(if len = 1 then "" else "s")
(fun fmt ->
Logic_var.Hashtbl.iter
(fun v () -> Format.fprintf fmt "%a " d_logic_var v)
vars)
d_predicate_named quantif
in
Misc.type_error msg
end;
guards
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
......@@ -147,7 +214,8 @@ let constant_to_exp ?(loc=Location.unknown) = function
let rec thost_to_host env = function
| TVar { lv_origin = Some v } -> Var v, env
| TVar { lv_origin = None } -> Misc.not_yet "logic variable"
| TVar ({ lv_origin = None } as logic_v) ->
Var (Env.Logic_binding.get env logic_v), env
| TResult _typ ->
let vis = Env.get_visitor env in
let kf = Extlib.the vis#current_kf in
......@@ -441,11 +509,11 @@ let rec named_predicate_to_exp env p =
(fun v _ ->
let lv = var v in
let then_block, _ =
let s = mkStmt ~valid_sid:true (Instr (Set(lv, e2, loc))) in
let s = mkStmtOneInstr ~valid_sid:true (Set(lv, e2, loc)) in
Env.pop_and_get env2 s ~global_clear:false Env.Middle
in
let else_block =
mkBlock [ mkStmt ~valid_sid:true (Instr (Set(lv, zero loc, loc))) ]
mkBlock [ mkStmtOneInstr ~valid_sid:true (Set(lv, zero loc, loc)) ]
in
[ mkStmt ~valid_sid:true (If(e1, then_block, else_block, loc)) ])
| Por(p1, p2) ->
......@@ -476,8 +544,125 @@ let rec named_predicate_to_exp env p =
new_exp ~loc (UnOp(LNot, e, TInt(IInt, []))), env
| Pif _ -> Misc.not_yet "_ ? _ : _"
| Plet _ -> Misc.not_yet "let _ = _ in _"
| Pforall _ -> Misc.not_yet "\\forall"
| Pexists _ -> Misc.not_yet "\\exists"
| 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 =
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.