Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
facfd007
Commit
facfd007
authored
Aug 02, 2019
by
Julien Signoles
Browse files
[rational] introduce Gmp.Z and Gmp.Q for integers and rationals, respectively
parent
0324062d
Changes
7
Hide whitespace changes
Inline
Side-by-side
src/plugins/e-acsl/env.ml
View file @
facfd007
...
...
@@ -198,10 +198,10 @@ let acc_list_rev acc l = List.fold_left (fun acc x -> x :: acc) acc l
let
do_new_var
~
loc
?
(
scope
=
Local_block
)
?
(
name
=
""
)
env
t
ty
mk_stmts
=
let
local_env
,
tl_env
=
top
env
in
let
local_block
=
local_env
.
block_info
in
let
is_z_t
=
Gmp
.
is
_z
_t
ty
in
if
is_z_t
then
Gmp
.
is
_z
_now_referenced
()
;
let
is_q_t
=
Gmp
.
is
_q
_t
ty
in
if
is_q_t
then
Gmp
.
is
_q
_now_referenced
()
;
let
is_z_t
=
Gmp
.
Z
.
is_t
ty
in
if
is_z_t
then
Gmp
.
Z
.
is_now_referenced
()
;
let
is_q_t
=
Gmp
.
Q
.
is_t
ty
in
if
is_q_t
then
Gmp
.
Q
.
is_now_referenced
()
;
let
n
=
succ
env
.
cpt
in
let
v
=
Cil
.
makeVarinfo
...
...
@@ -301,7 +301,7 @@ let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
?
name
env
t
(
Gmp
.
z_
t
()
)
(
Gmp
.
Z
.
t
()
)
(
fun
v
e
->
Gmp
.
init
~
loc
e
::
mk_stmts
v
e
)
module
Logic_binding
=
struct
...
...
@@ -322,7 +322,7 @@ module Logic_binding = struct
|
Some
ty
->
ty
|
None
->
match
logic_v
.
lv_type
with
|
Ctype
ty
->
ty
|
Linteger
->
Gmp
.
z_
t
()
|
Linteger
->
Gmp
.
Z
.
t
()
|
Ltype
_
as
ty
when
Logic_const
.
is_boolean_type
ty
->
Cil
.
charType
|
Ltype
_
|
Lvar
_
|
Lreal
|
Larrow
_
as
lty
->
let
msg
=
...
...
src/plugins/e-acsl/gmp.ml
View file @
facfd007
...
...
@@ -23,61 +23,53 @@
open
Cil_types
(**************************************************************************)
(***************************** mpz type
***********************************)
(***************************** mpz type
s
***********************************)
(**************************************************************************)
let
z_t_torig
_ref
=
let
mk_dummy_type_info
_ref
()
=
ref
{
torig_name
=
""
;
tname
=
""
;
ttype
=
TVoid
[]
;
treferenced
=
false
}
let
z_t_struct_torig_ref
=
ref
{
torig_name
=
""
;
tname
=
""
;
ttype
=
TVoid
[]
;
treferenced
=
false
}
let
set_z_t
ty
=
z_t_torig_ref
:=
ty
let
is_z_now_referenced
()
=
!
z_t_torig_ref
.
treferenced
<-
true
let
z_t
()
=
TNamed
(
!
z_t_torig_ref
,
[]
)
let
z_t_ptr
()
=
TNamed
(
{
torig_name
=
""
;
tname
=
"__e_acsl_mpz_struct *"
;
ttype
=
TArray
(
TNamed
(
!
z_t_struct_torig_ref
,
[]
)
,
Some
(
Cil
.
one
~
loc
:
Cil_datatype
.
Location
.
unknown
)
,
{
scache
=
Not_Computed
}
,
[]
);
treferenced
=
true
;
}
,
[]
)
let
is_z_t
ty
=
Cil_datatype
.
Typ
.
equal
ty
(
z_t
()
)
(**************************************************************************)
(***************************** 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
()
)
module
type
S
=
sig
val
t
:
unit
->
typ
val
set_t
:
typeinfo
->
unit
val
is_now_referenced
:
unit
->
unit
val
is_t
:
typ
->
bool
end
module
Make
(
X
:
sig
end
)
=
struct
let
t_torig_ref
=
mk_dummy_type_info_ref
()
let
set_t
ty
=
t_torig_ref
:=
ty
let
is_now_referenced
()
=
!
t_torig_ref
.
treferenced
<-
true
let
t
()
=
TNamed
(
!
t_torig_ref
,
[]
)
let
is_t
ty
=
Cil_datatype
.
Typ
.
equal
ty
(
t
()
)
end
module
Z
=
struct
include
Make
(
struct
end
)
let
t_struct_torig_ref
=
mk_dummy_type_info_ref
()
let
t_ptr
()
=
TNamed
(
{
torig_name
=
""
;
tname
=
"__e_acsl_mpz_struct *"
;
ttype
=
TArray
(
TNamed
(
!
t_struct_torig_ref
,
[]
)
,
Some
(
Cil
.
one
~
loc
:
Cil_datatype
.
Location
.
unknown
)
,
{
scache
=
Not_Computed
}
,
[]
);
treferenced
=
true
;
}
,
[]
)
end
module
Q
=
Make
(
struct
end
)
(**************************************************************************)
(******************* Initialization of mpz and mpq types ******************)
...
...
@@ -89,10 +81,10 @@ let init_t () =
inherit
Cil
.
nopCilVisitor
method
!
vglob
=
function
|
GType
({
torig_name
=
s
}
as
info
,
_
)
when
s
=
"__e_acsl_mpz_t"
->
set_
z_
t
info
;
Z
.
set_t
info
;
Cil
.
SkipChildren
|
GType
({
torig_name
=
s
}
as
info
,
_
)
when
s
=
"__e_acsl_mpq_t"
->
set_
q_
t
info
;
Q
.
set_t
info
;
Cil
.
SkipChildren
|
_
->
Cil
.
SkipChildren
...
...
@@ -106,11 +98,12 @@ let init_t () =
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_"
if
Z
.
is_t
ty
then
"__gmpz_"
else
if
Q
.
is_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
...
...
@@ -118,7 +111,7 @@ exception Longlong of ikind
let
get_set_suffix_and_arg
e
=
let
ty
=
Cil
.
typeOf
e
in
if
is
_z
_t
ty
||
is
_q
_t
ty
then
""
,
[
e
]
if
Z
.
is_t
ty
||
Q
.
is_t
ty
then
""
,
[
e
]
else
match
Cil
.
unrollType
ty
with
|
TInt
(
IChar
,
_
)
->
...
...
@@ -135,8 +128,9 @@ let get_set_suffix_and_arg e =
[
e
;
Cil
.
integer
~
loc
:
e
.
eloc
10
]
|
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 *)
Hence, calling [set_d] for both of them is sound.
HOWEVER: the machdep MUST NOT be vulnerable to double rounding *)
(* TODO RATIONAL: check machdep *)
"_d"
,
[
e
]
|
TFloat
(
FLongDouble
,
_
)
->
Error
.
not_yet
"creating gmp from long double"
...
...
@@ -145,18 +139,19 @@ let get_set_suffix_and_arg e =
let
generic_affect
~
loc
fname
lv
ev
e
=
let
ty
=
Cil
.
typeOf
ev
in
if
is
_z
_t
ty
then
begin
if
Z
.
is_t
ty
then
begin
assert
(* Missing cast/wrong typing happened
previously
*)
(
not
(
is
_q
_t
(
Cil
.
typeOf
e
)));
(* Missing cast/wrong typing happened
in the past
*)
(
not
(
Q
.
is_t
(
Cil
.
typeOf
e
)));
let
suf
,
args
=
get_set_suffix_and_arg
e
in
Misc
.
mk_call
~
loc
(
fname
^
suf
)
(
ev
::
args
)
end
else
if
is
_q
_t
ty
then
begin
end
else
if
Q
.
is_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 ?! *)
(* Missing cast/wrong typing happened in the past *)
(
not
(
Z
.
is_t
(
Cil
.
typeOf
e
)));
(* TODO RATIONAL: [from Fonenantsoa:]
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
...
...
@@ -165,9 +160,9 @@ let generic_affect ~loc fname lv ev e =
let
init_set
~
loc
lv
ev
e
=
let
fname
=
let
ty
=
Cil
.
typeOf
ev
in
if
is
_z
_t
ty
then
if
Z
.
is_t
ty
then
"__gmpz_init_set"
else
if
is
_q
_t
ty
then
else
if
Q
.
is_t
ty
then
Options
.
fatal
"no __gmpq_init_set: init then set separately"
else
""
...
...
@@ -177,7 +172,7 @@ let init_set ~loc lv ev e =
|
Longlong
IULongLong
->
(
match
e
.
enode
with
|
Lval
elv
->
assert
(
is
_z
_t
(
Cil
.
typeOf
ev
));
assert
(
Z
.
is_t
(
Cil
.
typeOf
ev
));
let
call
=
Misc
.
mk_call
~
loc
"__gmpz_import"
...
...
@@ -198,8 +193,8 @@ let init_set ~loc 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"
if
Z
.
is_t
ty
then
"__gmpz_set"
else
if
Q
.
is_t
ty
then
"__gmpq_set"
else
""
in
try
generic_affect
~
loc
fname
lv
ev
e
...
...
src/plugins/e-acsl/gmp.mli
View file @
facfd007
...
...
@@ -24,35 +24,29 @@
open
Cil_types
(**************************************************************************)
(******************************** Types ***********************************)
(**************************************************************************)
val
init_t
:
unit
->
unit
(** Must be called before any use of GMP *)
val
set_z_t
:
typeinfo
->
unit
val
set_q_t
:
typeinfo
->
unit
val
z_t
:
unit
->
typ
(** type [mpz_t] *)
(**************************************************************************)
(******************************** Types ***********************************)
(**************************************************************************)
val
z_t_ptr
:
unit
->
typ
module
type
S
=
sig
val
t
:
unit
->
typ
val
set_t
:
typeinfo
->
unit
val
is_now_referenced
:
unit
->
unit
val
is_t
:
typ
->
bool
end
(** Representation of the unbounded integer type at runtime *)
module
Z
:
sig
include
S
val
t_ptr
:
unit
->
typ
(** type "_mpz_struct *" *)
end
val
q_t
:
unit
->
typ
(** type [mpq_t] *)
val
is_z_now_referenced
:
unit
->
unit
(** Should be called once one variable of type [mpz_t] exists *)
val
is_q_now_referenced
:
unit
->
unit
(** Should be called once one variable of type [mpq_t] exists *)
val
is_z_t
:
typ
->
bool
(** is the type equal to [mpz_t]? *)
val
is_q_t
:
typ
->
bool
(** is the type equal to [mpq_t]? *)
(** Representation of the rational type at runtime *)
module
Q
:
S
(**************************************************************************)
(************************* Calls to builtins ******************************)
...
...
src/plugins/e-acsl/logic_functions.ml
View file @
facfd007
...
...
@@ -41,7 +41,7 @@ let term_to_exp_ref
(* @return true iff the result of the function is provided by reference as the
first extra argument at each call *)
let
result_as_extra_argument
=
Gmp
.
is
_z
_t
let
result_as_extra_argument
=
Gmp
.
Z
.
is_t
(* TODO: to be extended to any compound type? E.g. returning a struct is not
good practice... *)
...
...
@@ -125,7 +125,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
|
Typing
.
Gmpz
->
(* GMP's integer are arrays: consider them as pointers in function's
parameters *)
Gmp
.
z_
t_ptr
()
Gmp
.
Z
.
t_ptr
()
|
Typing
.
C_type
ik
->
TInt
(
ik
,
[]
)
|
Typing
.
Real
->
(* TODO RATIONAL: implement this case *)
...
...
@@ -196,7 +196,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
|
TInt
_
as
ty
->
Interval
.
Env
.
add
lvi
(
Interval
.
interv_of_typ
ty
)
|
ty
->
(* TODO RATIONAL: what to do with rationals? *)
if
Gmp
.
is
_z
_t
ty
then
if
Gmp
.
Z
.
is_t
ty
then
Interval
.
Env
.
add
lvi
(
Ival
.
inject_range
None
None
));
Env
.
Logic_binding
.
add_binding
env
lvi
vi
in
...
...
src/plugins/e-acsl/real.ml
View file @
facfd007
...
...
@@ -27,7 +27,7 @@ let t () =
the following typ MUST be changed into a typ that can represent them.
It is sound to use GMPQ for the time being since irrationals
raise not_yet. *)
Gmp
.
q_
t
()
Gmp
.
Q
.
t
()
let
is_t
ty
=
Cil_datatype
.
Typ
.
equal
ty
(
t
()
)
...
...
@@ -40,7 +40,7 @@ let init_set ~loc lval vi_e e =
Gmp
.
affect
~
loc
lval
vi_e
e
]))
let
mk_real
~
loc
?
name
e
env
t_opt
=
if
Gmp
.
is
_z
_t
(
Cil
.
typeOf
e
)
then
if
Gmp
.
Z
.
is_t
(
Cil
.
typeOf
e
)
then
(* GMPQ has no builtin for creating Q from Z. Hence:
1) Get the MPZ as a string: gmZ_get_str
2) Set the MPQ with that string: gmpQ_set_str *)
...
...
src/plugins/e-acsl/translate.ml
View file @
facfd007
...
...
@@ -73,7 +73,7 @@ let add_cast ~loc ?name env ctx sty t_opt e =
?
name
env
t_opt
(
Gmp
.
z_
t
()
)
(
Gmp
.
Z
.
t
()
)
(
fun
lv
v
->
[
Gmp
.
init_set
~
loc
(
Cil
.
var
lv
)
v
e
])
in
e
,
env
...
...
@@ -88,8 +88,8 @@ let add_cast ~loc ?name env ctx sty t_opt e =
e
,
env
|
Some
ctx
->
let
ty
=
Cil
.
typeOf
e
in
if
Gmp
.
is
_z
_t
ctx
then
if
Gmp
.
is
_z
_t
ty
then
if
Gmp
.
Z
.
is_t
ctx
then
if
Gmp
.
Z
.
is_t
ty
then
e
,
env
else
if
Real
.
is_t
ty
then
Real
.
cast_to_z
~
loc
?
name
e
env
...
...
@@ -113,7 +113,7 @@ let add_cast ~loc ?name env ctx sty t_opt e =
else
Real
.
mk_real
~
loc
?
name
e
env
t_opt
else
(* handle a C-integer context *)
if
Gmp
.
is
_z
_t
ty
||
sty
=
StrZ
then
if
Gmp
.
Z
.
is_t
ty
||
sty
=
StrZ
then
(* we get an mpz, but it fits into a C integer: convert it *)
let
fname
,
new_ty
=
if
Cil
.
isSignedInteger
ctx
then
...
...
@@ -155,7 +155,7 @@ let constant_to_exp ~loc t c =
|
Typing
.
C_type
kind
->
let
cast
=
Typing
.
get_cast
t
in
match
cast
,
kind
with
|
Some
ty
,
(
ILongLong
|
IULongLong
)
when
Gmp
.
is
_z
_t
ty
->
|
Some
ty
,
(
ILongLong
|
IULongLong
)
when
Gmp
.
Z
.
is_t
ty
->
raise
Cil
.
Not_representable
|
Some
ty
,
(
ILongLong
|
IULongLong
)
when
Real
.
is_t
ty
->
mk_real
(
Integer
.
to_string
n
)
...
...
@@ -273,7 +273,7 @@ and context_insensitive_term_to_exp kf env t =
|
TUnOp
(
Neg
|
BNot
as
op
,
t'
)
->
let
ty
=
Typing
.
get_typ
t
in
let
e
,
env
=
term_to_exp
kf
env
t'
in
if
Gmp
.
is
_z
_t
ty
then
if
Gmp
.
Z
.
is_t
ty
then
let
name
,
vname
=
match
op
with
|
Neg
->
"__gmpz_neg"
,
"neg"
|
BNot
->
"__gmpz_com"
,
"bnot"
...
...
@@ -294,7 +294,7 @@ and context_insensitive_term_to_exp kf env t =
Cil
.
new_exp
~
loc
(
UnOp
(
op
,
e
,
ty
))
,
env
,
Not_a_strnum
,
""
|
TUnOp
(
LNot
,
t
)
->
let
ty
=
Typing
.
get_op
t
in
if
Gmp
.
is
_z
_t
ty
then
if
Gmp
.
Z
.
is_t
ty
then
(* [!t] is converted into [t == 0] *)
let
zero
=
Logic_const
.
tinteger
0
in
let
ctx
=
Typing
.
get_number_ty
t
in
...
...
@@ -314,7 +314,7 @@ and context_insensitive_term_to_exp kf env t =
let
ty
=
Typing
.
get_typ
t
in
let
e1
,
env
=
term_to_exp
kf
env
t1
in
let
e2
,
env
=
term_to_exp
kf
env
t2
in
if
Gmp
.
is
_z
_t
ty
then
if
Gmp
.
Z
.
is_t
ty
then
let
name
=
name_of_mpz_arith_bop
bop
in
let
mk_stmts
_
e
=
[
Misc
.
mk_call
~
loc
name
[
e
;
e1
;
e2
]
]
in
let
name
=
Misc
.
name_of_binop
bop
in
...
...
@@ -334,7 +334,7 @@ and context_insensitive_term_to_exp kf env t =
let
ty
=
Typing
.
get_typ
t
in
let
e1
,
env
=
term_to_exp
kf
env
t1
in
let
e2
,
env
=
term_to_exp
kf
env
t2
in
if
Gmp
.
is
_z
_t
ty
then
if
Gmp
.
Z
.
is_t
ty
then
(* TODO: preventing division by zero should not be required anymore.
RTE should do this automatically. *)
let
ctx
=
Typing
.
get_number_ty
t
in
...
...
@@ -352,7 +352,7 @@ and context_insensitive_term_to_exp kf env t =
~
loc
kf
env
Typing
.
gmpz
~
e1
:
e2
~
name
Eq
t2
zero
t
in
let
mk_stmts
_v
e
=
assert
(
Gmp
.
is
_z
_t
ty
);
assert
(
Gmp
.
Z
.
is_t
ty
);
let
vis
=
Env
.
get_visitor
env
in
let
kf
=
Extlib
.
the
vis
#
current_kf
in
let
cond
=
...
...
@@ -904,7 +904,7 @@ exception No_simple_translation of term
let
term_to_exp
typ
t
=
(* infer a context from the given [typ] whenever possible *)
let
ctx_of_typ
ty
=
if
Gmp
.
is
_z
_t
ty
then
Typing
.
gmpz
if
Gmp
.
Z
.
is_t
ty
then
Typing
.
gmpz
else
if
Real
.
is_t
ty
then
Typing
.
libr
else
match
ty
with
...
...
src/plugins/e-acsl/typing.ml
View file @
facfd007
...
...
@@ -107,13 +107,13 @@ let join ty1 ty2 = match ty1, ty2 with
exception
Not_a_number
let
typ_of_number_ty
=
function
|
C_type
ik
->
TInt
(
ik
,
[]
)
|
Gmpz
->
Gmp
.
z_
t
()
|
Gmpz
->
Gmp
.
Z
.
t
()
|
Real
->
Real
.
t
()
|
Nan
->
raise
Not_a_number
let
typ_of_lty
=
function
|
Ctype
cty
->
cty
|
Linteger
->
Gmp
.
z_
t
()
|
Linteger
->
Gmp
.
Z
.
t
()
|
Lreal
->
(* TODO RATIONAL: implement this case *)
assert
false
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment