Commit ad8d968c authored by Fonenantsoa Maurica 's avatar Fonenantsoa Maurica Committed by Julien Signoles
Browse files

Extend Interval, Typing and Translate:

  - Interval:
    - Not_an_integer -> Is_a_real|Not_a_number.
    - infer -> infer_with_real
      because Not_a_number has priority over Is_a_real
    - Ival.bottom when Is_a_real
      because the interval is for integers
  - Typing:
    - integer_ty -> number_ty=Cty|Gmpz|Libr|Nan
    - Other -> 'Other (Oreal|Onan)'
  - Translate:
    Encode real constants into strings:
      - **NO** conversion to float-point type
      - strnum_ty=StrZ|StrR|Not_a_strnum
        for tracking the type of the string
Add Libr:
  - Gmpz -> Gmp=Gmpz+Gmpq
  - Libr=ref to Gmpq
Add Gmpq builtins:
  - Custom mini-gmp -> libgmp
    because mini-gmp has no support for Q
  - Add arithmetic over Q in e_acsl_gmp_api.h
Misc:
  - dec_to_frac: decimal expansion to fractional representation
    because decimal expansion is interpreted as double by Gmpq
Tests:
  - BTS 1307 has an assertion wrongly evaluated, fixed
  - Add tests/gmp/reals.c
THE MOST IMPORTANT TODO:
  - Completely hide the library for numbers (currently Gmp)
    inside Libr: Typing, Env and Translate should only know
    Libr and never directly call Gmp.
    This is crucial for extending E-ACSL in the future
    (eg: Gmp has no support for elementary functions), and
    also for using it as part of an abstract compiler
    (eg: with Fldlib)
    For the time being, in Translate,
    we have something as ugly as:
      let init_set =
        if Libr.is_t ty then Libr.init_set
        else Gmp.init_set
parent 3a1240c2
......@@ -64,13 +64,14 @@ PLUGIN_CMO:= local_config \
builtins \
functions \
misc \
gmpz \
gmp \
literal_strings \
mmodel_analysis \
exit_points \
label \
lscope \
env \
libr \
keep_status \
dup_functions \
interval \
......@@ -213,34 +214,10 @@ $(EACSL_DLMALLOC_LIB): $(EACSL_DLMALLOC_SRC)
echo 'RANLIB $@'
ranlib $@
############
# GMP #
############
EACSL_GMP_REL_DIR:=contrib/libgmp
EACSL_GMP_DIR := $(EACSL_PLUGIN_DIR)/$(EACSL_GMP_REL_DIR)
EACSL_GMP_LIBNAME = libeacsl-gmp.a
EACSL_GMP_LIB = $(EACSL_LIBDIR)/$(EACSL_GMP_LIBNAME)
EACSL_GMP_OBJ = mini-gmp.o
EACSL_GMP_SRC = $(EACSL_GMP_DIR)/mini-gmp.c
EACSL_GMP_FLAGS = \
-Dmalloc=__e_acsl_private_malloc \
-Drealloc=__e_acsl_private_realloc \
-Dfree=__e_acsl_private_free
$(EACSL_GMP_LIB): $(EACSL_GMP_SRC)
$(MKDIR) $(EACSL_LIBDIR)
echo 'CC $< '
$(CC) $< $(EACSL_GMP_FLAGS) -c -O2 -g3 -o$(EACSL_GMP_OBJ)
echo 'AR $@'
$(AR) crus $(EACSL_GMP_LIB) $(EACSL_GMP_OBJ)
echo 'RANLIB $@'
ranlib $(EACSL_GMP_LIB)
all:: $(EACSL_DLMALLOC_LIB) $(EACSL_GMP_LIB)
all:: $(EACSL_DLMALLOC_LIB)
clean::
$(RM) $(EACSL_DLMALLOC_LIB) $(EACSL_GMP_LIB)
$(RM) $(EACSL_DLMALLOC_LIB)
############
# Cleaning #
......@@ -261,8 +238,6 @@ e-acsl-distclean:: clean
EXPORT = e-acsl-$(EACSL_VERSION)
EACSL_CONTRIB_FILES = \
$(EACSL_GMP_REL_DIR)/mini-gmp.c \
$(EACSL_GMP_REL_DIR)/mini-gmp.h \
$(EACSL_DLMALLOC_REL_DIR)/dlmalloc.c
EACSL_MANUAL_FILES = doc/manuals/*.pdf
......@@ -276,7 +251,7 @@ EACSL_DOC_FILES = \
EACSL_TEST_FILES = \
tests/test_config.in tests/print.ml
# Test files without header management
# Test files without header management
EACSL_DISTRIB_TESTS = \
$(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
$(dir)/*.[ich] \
......@@ -401,7 +376,7 @@ EACSL_CEA_LGPL_BARE= *.ml *.mli Makefile.in configure.ac \
EACSL_CEA_LGPL=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_CEA_LGPL_BARE)) \
$(EACSL_CEA_SHARE)
# valid values: open-source, close-source
# valid values: open-source, close-source
EACSL_HEADERS?=open-source
headers::
@echo "Applying $(EACSL_HEADERS) headers..."
......@@ -414,9 +389,6 @@ headers::
headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \
-h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/MODIFIED_DLMALLOC \
$(EACSL_PLUGIN_DIR)/contrib/libdlmalloc/dlmalloc.c
headache -c $(EACSL_PLUGIN_DIR)/license/headache_config.txt \
-h $(EACSL_PLUGIN_DIR)/headers/$(EACSL_HEADERS)/MODIFIED_LIB_GMP \
$(EACSL_PLUGIN_DIR)/contrib/libgmp/mini-gmp.[ch]
endif
......
......@@ -229,55 +229,56 @@ let to_exp ~loc kf env pot label =
| Misc.PoT_pred _ ->
Cil.intType
| Misc.PoT_term t ->
begin match Typing.get_integer_ty t with
| Typing.C_type _ | Typing.Other ->
begin match Typing.get_number_ty t with
| Typing.C_type _ | Typing.Nan ->
Typing.get_typ t
| Typing.Gmp ->
| Typing.Libr ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
end
in
let ty_ptr = TPtr(ty, []) in
let vi_at, e_at, env =
Env.new_var
~loc
~name:"at"
~scope:Env.Function
env
None
ty_ptr
(fun vi e ->
(* Handle [malloc] and [free] stmts *)
let lty_sizeof = Ctype Cil.(theMachine.typeOfSizeOf) in
let t_sizeof = Logic_const.term ~loc (TSizeOf ty) lty_sizeof in
let t_size = size_from_sizes_and_shifts ~loc sizes_and_shifts in
let t_size =
Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
in
Typing.type_term ~use_gmp_opt:false t_size;
let malloc_stmt = match Typing.get_integer_ty t_size with
| Typing.C_type IInt ->
let e_size, _ = term_to_exp kf env t_size in
let e_size = Cil.constFold false e_size in
let malloc_stmt =
Misc.mk_call ~loc ~result:(Cil.var vi) "malloc" [e_size]
in
malloc_stmt
| Typing.C_type _ | Typing.Gmp ->
Error.not_yet
"\\at on purely logic variables that needs to allocate \
too much memory (bigger than int_max bytes)"
| Typing.Other ->
Options.fatal
"quantification over non-integer type is not part of E-ACSL"
in
let free_stmt = Misc.mk_call ~loc "free" [e] in
(* The list of stmts returned by the current closure are inserted
LOCALLY to the block where the new var is FIRST used, whatever scope
is indicated to [Env.new_var]. Thus we need to add [malloc] and
[free] through dedicated functions. *)
Malloc.add kf malloc_stmt;
Free.add kf free_stmt;
[])
let vi_at, e_at, env = Env.new_var
~loc
~name:"at"
~scope:Env.Function
env
None
ty_ptr
(fun vi e ->
(* Handle [malloc] and [free] stmts *)
let lty_sizeof = Ctype Cil.(theMachine.typeOfSizeOf) in
let t_sizeof = Logic_const.term ~loc (TSizeOf ty) lty_sizeof in
let t_size = size_from_sizes_and_shifts ~loc sizes_and_shifts in
let t_size =
Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
in
Typing.type_term ~use_gmp_opt:false t_size;
let malloc_stmt = match Typing.get_number_ty t_size with
| Typing.C_type IInt ->
let e_size, _ = term_to_exp kf env t_size in
let e_size = Cil.constFold false e_size in
let malloc_stmt =
Misc.mk_call ~loc ~result:(Cil.var vi) "malloc" [e_size]
in
malloc_stmt
| Typing.C_type _ | Typing.Gmpz ->
Error.not_yet
"\\at on purely logic variables that needs to allocate \
too much memory (bigger than int_max bytes)"
| Typing.Libr | Typing.Nan ->
Options.fatal
"quantification over non-integer type is not part of E-ACSL"
in
let free_stmt = Misc.mk_call ~loc "free" [e] in
(* The list of stmts returned by the current closure are inserted
LOCALLY to the block where the new var is FIRST used, whatever scope
is indicated to [Env.new_var].
Thus we need to add [malloc] and [free] through dedicated functions. *)
Malloc.add kf malloc_stmt;
Free.add kf free_stmt;
[])
in
(* Index *)
let t_index = index_from_sizes_and_shifts ~loc sizes_and_shifts in
......@@ -301,8 +302,8 @@ let to_exp ~loc kf env pot label =
variable declarations. *)
[ Cil.mkStmt ~valid_sid:true (Block block) ], env
| Misc.PoT_term t ->
begin match Typing.get_integer_ty t with
| Typing.C_type _ | Typing.Other ->
begin match Typing.get_number_ty t with
| Typing.C_type _ | Typing.Nan ->
let env = Env.push env in
let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
let e, env = term_to_exp kf env t in
......@@ -316,7 +317,9 @@ let to_exp ~loc kf env pot label =
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
[ Cil.mkStmt ~valid_sid:true (Block block) ], env
| Typing.Gmp ->
| Typing.Libr ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
end
in
......
# Copyright 1999 Free Software Foundation, Inc.
#
# This file is part of the GNU MP Library.
#
# The GNU MP Library is free software; you can redistribute it and/or modify
# it under the terms of either:
#
# * the GNU Lesser General Public License as published by the Free
# Software Foundation; either version 3 of the License, or (at your
# option) any later version.
#
# or
#
# * the GNU General Public License as published by the Free Software
# Foundation; either version 2 of the License, or (at your option) any
# later version.
#
# or both in parallel, as here.
#
# The GNU MP Library 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 General Public License
# for more details.
#
# You should have received copies of the GNU General Public License and the
# GNU Lesser General Public License along with the GNU MP Library. If not,
# see https://www.gnu.org/licenses/.
define pz
set __gmpz_dump ($)
end
define pq
set __gmpz_dump ($->_mp_num)
echo /
set __gmpz_dump ($->_mp_den)
end
define pf
set __gmpf_dump ($)
end
Copyright 2011-2013 Free Software Foundation, Inc.
This file is part of the GNU MP Library.
The GNU MP Library is free software; you can redistribute it and/or modify
it under the terms of either:
* the GNU Lesser General Public License as published by the Free
Software Foundation; either version 3 of the License, or (at your
option) any later version.
or
* the GNU General Public License as published by the Free Software
Foundation; either version 2 of the License, or (at your option) any
later version.
or both in parallel, as here.
The GNU MP Library 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 General Public License
for more details.
You should have received copies of the GNU General Public License and the
GNU Lesser General Public License along with the GNU MP Library. If not,
see https://www.gnu.org/licenses/.
This is "mini-gmp", a small implementation of a subset of GMP's mpn
and mpz interfaces.
It is intended for applications which need arithmetic on numbers
larger than a machine word, but which don't need to handle very large
numbers very efficiently. Those applications can include a copy of
mini-gmp to get a GMP-compatible interface with small footprint. One
can also arrange for optional linking with the real GMP library, using
mini-gmp as a fallback when for some reason GMP is not available, or
not desired as a dependency.
The supported GMP subset is declared in mini-gmp.h. The implemented
functions are fully compatible with the corresponding GMP functions,
as specified in the GMP manual, with a few exceptions:
mpz_set_str, mpz_init_set_str, mpz_get_str, mpz_out_str and
mpz_sizeinbase support only |base| <= 36;
mpz_export and mpz_import support only NAILS = 0.
The REALLOC_FUNC and FREE_FUNC registered with
mp_set_memory_functions does not get the correct size of the
allocated block in the corresponding argument. mini-gmp always
passes zero for these rarely used arguments.
The implementation is a single file, mini-gmp.c.
The performance target for mini-gmp is to be at most 10 times slower
than the real GMP library, for numbers of size up to a few hundred
bits. No asymptotically fast algorithms are included in mini-gmp, so
it will be many orders of magnitude slower than GMP for very large
numbers.
You should never "install" mini-gmp. Applications can either just
#include mini-gmp.c (but then, beware that it defines several macros
and functions outside of the advertised interface). Or compile
mini-gmp.c as a separate compilation unit, and use the declarations in
mini-gmp.h.
The tests subdirectory contains a testsuite. To use it, you need GMP
and GNU make. Just run make check in the tests directory. If the
hard-coded compiler settings are not right, you have to either edit the
Makefile or pass overriding values on the make command line (e.g.,
make CC=cc check). Testing is not (yet) as thorough as for the real
GMP.
The current version was put together by Niels Möller
<nisse@lysator.liu.se>, with a fair amount of copy-and-paste from the
GMP sources.
This diff is collapsed.
This diff is collapsed.
......@@ -222,7 +222,7 @@ let dup_global loc actions spec bhv sound_verdict_vi kf vi new_vi =
(* Visitor *)
(* ********************************************************************** *)
type position = Before_gmp | Gmp | After_gmp | Memory_model | Code
type position = Before_gmp | Gmpz | After_gmp | Memory_model | Code
class dup_functions_visitor prj = object (self)
inherit Visitor.frama_c_copy prj
......@@ -253,7 +253,7 @@ class dup_functions_visitor prj = object (self)
vi
method private before_memory_model = match before_memory_model with
| Before_gmp | Gmp | After_gmp -> true
| Before_gmp | Gmpz | After_gmp -> true
| Memory_model | Code -> false
method private insert_libc l =
......@@ -275,7 +275,7 @@ class dup_functions_visitor prj = object (self)
method private next () =
match before_memory_model with
| Before_gmp -> ()
| Gmp -> before_memory_model <- After_gmp
| Gmpz -> before_memory_model <- After_gmp
| After_gmp -> ()
| Memory_model -> before_memory_model <- Code
| Code -> ()
......@@ -380,8 +380,8 @@ if there are memory-related annotations.@]"
| GVarDecl(_, loc) | GFunDecl(_, _, loc) | GFun(_, loc)
when Misc.is_library_loc loc ->
(match before_memory_model with
| Before_gmp -> before_memory_model <- Gmp
| Gmp | Memory_model -> ()
| Before_gmp -> before_memory_model <- Gmpz
| Gmpz | Memory_model -> ()
| After_gmp -> before_memory_model <- Memory_model
| Code -> () (* still processing the GMP and memory model headers,
but reading some libc code *));
......
This diff is collapsed.
......@@ -22,31 +22,36 @@
open Cil_types
let t_torig_ref =
ref
(**************************************************************************)
(***************************** mpz type ***********************************)
(**************************************************************************)
let z_t_torig_ref =
ref
{ torig_name = "";
tname = "";
ttype = TVoid [];
treferenced = false }
let t_struct_torig_ref =
let z_t_struct_torig_ref =
ref
{ torig_name = "";
tname = "";
ttype = TVoid [];
treferenced = false }
let set_t ty = t_torig_ref := ty
let set_t_struct ty = t_struct_torig_ref := ty
let set_z_t ty = z_t_torig_ref := ty
let is_z_now_referenced () = !z_t_torig_ref.treferenced <- true
let is_now_referenced () = !t_torig_ref.treferenced <- true
let z_t () = TNamed(!z_t_torig_ref, [])
let t () = TNamed(!t_torig_ref, [])
let t_ptr () = TNamed(
let z_t_ptr () = TNamed(
{
torig_name = "";
tname = "__e_acsl_mpz_struct *";
ttype = TArray(
TNamed(!t_struct_torig_ref, []),
TNamed(!z_t_struct_torig_ref, []),
Some (Cil.one ~loc:Cil_datatype.Location.unknown),
{scache = Not_Computed},
[]);
......@@ -54,23 +59,71 @@ let t_ptr () = TNamed(
},
[])
let is_t ty =
Cil_datatype.Typ.equal ty (t ()) || Cil_datatype.Typ.equal ty (t_ptr ())
let is_z_t ty = Cil_datatype.Typ.equal ty (z_t ())
let apply_on_var ~loc funname e = Misc.mk_call ~loc ("__gmpz_" ^ funname) [ e ]
(**************************************************************************)
(***************************** mpq type ***********************************)
(**************************************************************************)
let q_t_torig_ref =
ref
{ torig_name = "";
tname = "";
ttype = TVoid [];
treferenced = false }
let set_q_t ty = q_t_torig_ref := ty
let is_q_now_referenced () = !q_t_torig_ref.treferenced <- true
let q_t () = TNamed(!q_t_torig_ref, [])
let is_q_t ty = Cil_datatype.Typ.equal ty (q_t ())
(**************************************************************************)
(******************* Initialization of mpz and mpq types ******************)
(**************************************************************************)
let init_t () =
Options.feedback ~level:2 "initializing GMP types.";
let set_mp_t = object
inherit Cil.nopCilVisitor
method !vglob = function
| GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_t" ->
set_z_t info;
Cil.SkipChildren
| GType({ torig_name = s } as info, _) when s = "__e_acsl_mpq_t" ->
set_q_t info;
Cil.SkipChildren
| _ ->
Cil.SkipChildren
end in
Cil.visitCilFileSameGlobals set_mp_t (Ast.get ())
(**************************************************************************)
(************************* Calls to builtins ******************************)
(**************************************************************************)
let apply_on_var ~loc funname e =
let prefix =
let ty = Cil.typeOf e in
if is_z_t ty then "__gmpz_"
else if is_q_t ty then "__gmpq_"
else assert false
in
Misc.mk_call ~loc (prefix ^ funname) [ e ]
let init ~loc e = apply_on_var "init" ~loc e
let clear ~loc e = apply_on_var "clear" ~loc e
exception Longlong of ikind
let get_set_suffix_and_arg e =
let get_set_suffix_and_arg e =
let ty = Cil.typeOf e in
if is_t ty then "", [ e ]
if is_z_t ty || is_q_t ty then "", [ e ]
else
match Cil.unrollType ty with
| TInt(IChar, _) ->
(if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
else "_si"),
| TInt(IChar, _) ->
(if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
else "_si"),
[ e ]
| TInt((IBool | IUChar | IUInt | IUShort | IULong), _) ->
"_ui", [ e ]
......@@ -80,61 +133,79 @@ let get_set_suffix_and_arg e =
"_str",
(* decimal base for the number given as string *)
[ e; Cil.integer ~loc:e.eloc 10 ]
| _ -> assert false
| TFloat((FDouble | FFloat), _) ->
(* FFloat is a strict subset of FDouble (modulo exceptional numbers)
Hence, calling [set_d] for bor of them is sound.
HOWEVER: the machdep MUST NOT be vulnerable to double rounding *)
"_d", [ e ]
| TFloat(FLongDouble, _) ->
Error.not_yet "creating gmp from long double"
| _ ->
assert false
let generic_affect ~loc fname lv ev e =
let ty = Cil.typeOf ev in
if is_t ty then
if is_z_t ty then begin
assert
(* Missing cast/wrong typing happened previously *)
(not (is_q_t (Cil.typeOf e)));
let suf, args = get_set_suffix_and_arg e in
Misc.mk_call ~loc (fname ^ suf) (ev :: args)
else
end else if is_q_t ty then begin
assert
(* Missing cast/wrong typing happened previously *)
(not (is_z_t (Cil.typeOf e)));
(* TODO: If we try to factorize the following the above
then the result is different... why ?! *)
let suf, args = get_set_suffix_and_arg e in
Misc.mk_call ~loc (fname ^ suf) (ev :: args)
end else
Cil.mkStmtOneInstr ~valid_sid:true (Set(lv, e, e.eloc))
let init_set ~loc lv ev e =
try generic_affect ~loc "__gmpz_init_set" lv ev e
with
let init_set ~loc lv ev e =
let fname =
let ty = Cil.typeOf ev in
if is_z_t ty then
"__gmpz_init_set"
else if is_q_t ty then
Options.fatal "no __gmpq_init_set: init then set separately"
else
""
in
try generic_affect ~loc fname lv ev e
with
| Longlong IULongLong ->
(match e.enode with
| Lval elv ->
let call =
Misc.mk_call ~loc
"__gmpz_import"
[ ev;
Cil.one ~loc;
Cil.one ~loc;
Cil.sizeOf ~loc (TInt(IULongLong, []));
Cil.zero ~loc;
Cil.zero ~loc;
Cil.mkAddrOf ~loc elv ]
assert (is_z_t (Cil.typeOf ev));
let call = Misc.mk_call
~loc
"__gmpz_import"
[ ev;
Cil.one ~loc;
Cil.one ~loc;
Cil.sizeOf ~loc (TInt(IULongLong, []));
Cil.zero ~loc;
Cil.zero ~loc;
Cil.mkAddrOf ~loc elv ]
in
Cil.mkStmt
~valid_sid:true
(Block (Cil.mkBlock [ init ~loc ev; call ]))
| _ -> Error.not_yet "unsigned long long expression requiring GMP")
Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ init ~loc ev; call ]))
| _ ->
Error.not_yet "unsigned long long expression requiring GMP")
| Longlong ILongLong ->
Error.not_yet "long long requiring GMP"
let affect ~loc lv ev e =
try generic_affect ~loc "__gmpz_set" lv ev e
let affect ~loc lv ev e =
let fname =
let ty = Cil.typeOf ev in
if is_z_t ty then "__gmpz_set"
else if is_q_t ty then "__gmpq_set"
else ""
in
try generic_affect ~loc fname lv ev e
with Longlong _ ->
Error.not_yet "quantification over long long and requiring GMP"
let init_t () =
Options.feedback ~level:2 "initializing GMP type.";
let set_mpzt = object
inherit Cil.nopCilVisitor
method !vglob = function
| GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_t" ->
set_t info;
Cil.SkipChildren
| GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_struct" ->
set_t_struct info;
Cil.SkipChildren
| _ ->
Cil.SkipChildren
end in