Commit 5c2df65f authored by Julien Signoles's avatar Julien Signoles Committed by Kostyantyn Vorobyov
Browse files

[typing] rename label 'force' to 'use_gmp_opt' (with reverse semantics)

parent 313382da
......@@ -176,7 +176,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
let t1 = match rel1 with
| Rlt ->
let t = t_plus_one t1 in
Typing.type_term ~force:true ~ctx t;
Typing.type_term ~use_gmp_opt:false ~ctx t;
t
| Rle -> t1
| Rgt | Rge | Req | Rneq -> assert false
......@@ -190,7 +190,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
t_plus_one t2, Le
| Rgt | Rge | Req | Rneq -> assert false
in
Typing.type_term ~force:true ~ctx t2_one;
Typing.type_term ~use_gmp_opt:false ~ctx t2_one;
let ctx_one =
let ty1 = Typing.get_integer_ty t1 in
let ty2 = Typing.get_integer_ty t2_one in
......@@ -227,7 +227,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
Logic_const.term ~loc
(TBinOp(bop2, tlv, { t2 with term_node = t2.term_node } )) Linteger
in
Typing.type_term ~force:true ~ctx:Typing.c_int guard;
Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
let guard_exp, env = term_to_exp kf (Env.push env) guard in
let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
let guard_blk, env =
......@@ -245,7 +245,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
(* increment the loop counter [x++] *)
let tlv_one = t_plus_one tlv in
(* previous typing ensures that [x++] fits type [ty] *)
Typing.type_term ~force:true ~ctx:ctx_one tlv_one;
Typing.type_term ~use_gmp_opt:false ~ctx:ctx_one tlv_one;
let incr, env = term_to_exp kf (Env.push env) tlv_one in
let next_blk, env =
Env.pop_and_get
......
......@@ -304,7 +304,7 @@ and context_insensitive_term_to_exp kf env t =
(* [!t] is converted into [t == 0] *)
let zero = Logic_const.tinteger 0 in
let ctx = Typing.get_integer_ty t in
Typing.type_term ~force:false ~ctx zero;
Typing.type_term ~use_gmp_opt:true ~ctx zero;
let e, env =
comparison_to_exp kf ~loc ~name:"not" env Typing.gmp Eq t zero (Some t)
in
......@@ -348,7 +348,7 @@ and context_insensitive_term_to_exp kf env t =
possible values of [t2] *)
(* guarding divisions and modulos *)
let zero = Logic_const.tinteger 0 in
Typing.type_term ~force:false ~ctx zero;
Typing.type_term ~use_gmp_opt:true ~ctx zero;
(* do not generate [e2] from [t2] twice *)
let guard, env =
let name = name_of_binop bop ^ "_guard" in
......@@ -825,7 +825,7 @@ let term_to_exp typ t =
| _ -> Typing.other
in
let ctx = Extlib.opt_map ctx_of_typ typ in
Typing.type_term ~force:false ?ctx t;
Typing.type_term ~use_gmp_opt:true ?ctx t;
let env = Env.empty (new Visitor.frama_c_copy Project_skeleton.dummy) in
let env = Env.push env in
let env = Env.rte env false in
......
......@@ -223,18 +223,16 @@ let offset_ty t =
(** {2 Type system} *)
(******************************************************************************)
(* generate a context [c]. Take --e-acsl-gmp-only into account iff not
[force]. *)
let mk_ctx ~force c =
if force then c
else match c with
| Other -> Other
| Gmp | C_type _ -> if Options.Gmp_only.get () then Gmp else c
(* generate a context [c]. Take --e-acsl-gmp-only into account iff [use_gmp_opt]
is true. *)
let mk_ctx ~use_gmp_opt = function
| Other | Gmp as c -> c
| C_type _ as c -> if use_gmp_opt && Options.Gmp_only.get () then Gmp else c
(* type the term [t] in a context [ctx]. Take --e-acsl-gmp-only into account iff
not [force]. *)
let rec type_term ~force ?(arith_operand=false) ?ctx t =
let ctx = Extlib.opt_map (mk_ctx ~force) ctx in
[use_gmp_opt] is true. *)
let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
let ctx = Extlib.opt_map (mk_ctx ~use_gmp_opt) ctx in
let dup ty = ty, ty in
let compute_ctx ?ctx i =
(* in order to get a minimal amount of generated casts for operators, the
......@@ -243,10 +241,10 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
match ctx with
| None ->
(* no context: factorize *)
dup (mk_ctx ~force:false (ty_of_interv i))
dup (mk_ctx ~use_gmp_opt:true (ty_of_interv i))
| Some ctx ->
mk_ctx ~force:false (ty_of_interv ~ctx i),
mk_ctx ~force:false (ty_of_interv i)
mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx i),
mk_ctx ~use_gmp_opt:true (ty_of_interv i)
in
let infer t =
Cil.CurrentLoc.set t.term_loc;
......@@ -285,7 +283,7 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
try
let i = Interval.infer t in
(* [t'] must be typed, but it is a pointer *)
ignore (type_term ~force:false ~ctx:Other t');
ignore (type_term ~use_gmp_opt:true ~ctx:Other t');
ty_of_interv ?ctx i
with Interval.Not_an_integer ->
assert false (* this term is an integer *)
......@@ -297,8 +295,8 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
try
let i = Interval.infer t in
(* [t1] and [t2] must be typed, but they are pointers *)
ignore (type_term ~force:false ~ctx:Other t1);
ignore (type_term ~force:false ~ctx:Other t2);
ignore (type_term ~use_gmp_opt:true ~ctx:Other t1);
ignore (type_term ~use_gmp_opt:true ~ctx:Other t2);
ty_of_interv ?ctx i
with Interval.Not_an_integer ->
assert false (* this term is an integer *)
......@@ -314,7 +312,7 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
with Interval.Not_an_integer ->
dup Other (* real *)
in
ignore (type_term ~force ~arith_operand:true ~ctx t');
ignore (type_term ~use_gmp_opt ~arith_operand:true ~ctx t');
(match unop with
| LNot -> c_int, ctx_res (* converted into [t == 0] in case of GMP *)
| Neg | BNot -> dup ctx_res)
......@@ -339,8 +337,8 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
| _ -> true
in
let cast_first = cast_first t1 t2 in
ignore (type_term ~force ~arith_operand:cast_first ~ctx t1);
ignore (type_term ~force ~arith_operand:(not cast_first) ~ctx t2);
ignore (type_term ~use_gmp_opt ~arith_operand:cast_first ~ctx t1);
ignore (type_term ~use_gmp_opt ~arith_operand:(not cast_first) ~ctx t2);
dup ctx_res
| TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
......@@ -349,12 +347,12 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
try
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
mk_ctx ~force:false (ty_of_interv ?ctx (Ival.join i1 i2))
mk_ctx ~use_gmp_opt:true (ty_of_interv ?ctx (Ival.join i1 i2))
with Interval.Not_an_integer ->
Other
in
ignore (type_term ~force:false ~ctx t1);
ignore (type_term ~force:false ~ctx t2);
ignore (type_term ~use_gmp_opt:true ~ctx t1);
ignore (type_term ~use_gmp_opt:true ~ctx t2);
let ty = match ctx with
| Other -> c_int
| Gmp | C_type _ -> ctx
......@@ -371,8 +369,8 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
Other
in
(* both operands fit in an int. *)
ignore (type_term ~force:false ~ctx:c_int t1);
ignore (type_term ~force:false ~ctx:c_int t2);
ignore (type_term ~use_gmp_opt:true ~ctx:c_int t1);
ignore (type_term ~use_gmp_opt:true ~ctx:c_int t2);
dup ty
| TBinOp (BAnd, _, _) -> Error.not_yet "bitwise and"
......@@ -391,28 +389,31 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
with Interval.Not_an_integer ->
Other
in
ignore (type_term ~force:false ~ctx t');
ignore (type_term ~use_gmp_opt:true ~ctx t');
dup ctx
| Tif (t1, t2, t3) ->
let ctx1 = mk_ctx ~force:true c_int (* an int must be generated *) in
ignore (type_term ~force:true ~ctx:ctx1 t1);
let ctx1 =
mk_ctx ~use_gmp_opt:false c_int (* an int must be generated *)
in
ignore (type_term ~use_gmp_opt:false ~ctx:ctx1 t1);
let i = Interval.infer t in
let ctx =
try
let i2 = Interval.infer t2 in
let i3 = Interval.infer t3 in
let ctx = ty_of_interv ?ctx (Ival.join i (Ival.join i2 i3)) in
mk_ctx ~force:false ctx
mk_ctx ~use_gmp_opt:true ctx
with Interval.Not_an_integer ->
Other
in
ignore (type_term ~force:false ~ctx t2);
ignore (type_term ~force:false ~ctx t3);
ignore (type_term ~use_gmp_opt:true ~ctx t2);
ignore (type_term ~use_gmp_opt:true ~ctx t3);
dup ctx
| Tat (t, _)
| TLogic_coerce (_, t) -> dup (type_term ~force ~arith_operand ?ctx t).ty
| TLogic_coerce (_, t) ->
dup (type_term ~use_gmp_opt ~arith_operand ?ctx t).ty
| TCoerceE (t1, t2) ->
let ctx =
......@@ -424,8 +425,8 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
with Interval.Not_an_integer ->
Other
in
ignore (type_term ~force:false ~ctx t1);
ignore (type_term ~force:false ~ctx t2);
ignore (type_term ~use_gmp_opt:true ~ctx t1);
ignore (type_term ~use_gmp_opt:true ~ctx t2);
dup ctx
| TAddrOf tlv
......@@ -436,20 +437,20 @@ let rec type_term ~force ?(arith_operand=false) ?ctx t =
| Tbase_addr (_, t) ->
(* it is a pointer, but subterms must be typed. *)
ignore (type_term ~force:false ~ctx:Other t);
ignore (type_term ~use_gmp_opt:true ~ctx:Other t);
dup Other
| TBinOp ((PlusPI | IndexPI | MinusPI), t1, t2) ->
(* both [t1] and [t2] must be typed. *)
ignore (type_term ~force:false ~ctx:Other t1);
ignore (type_term ~use_gmp_opt:true ~ctx:Other t1);
let ctx = offset_ty t2 in
ignore (type_term ~force:true ~ctx t2);
ignore (type_term ~use_gmp_opt:false ~ctx t2);
dup Other
| Tapp(li, _, args) ->
let typ_arg lvi arg =
let ctx = ty_of_logic_ty lvi.lv_type in
ignore (type_term ~force:true ~ctx arg)
ignore (type_term ~use_gmp_opt:false ~ctx arg)
in
List.iter2 typ_arg li.l_profile args;
(* [li.l_type is [None] for predicate only: not possible here.
......@@ -486,7 +487,7 @@ and type_term_lval (host, offset) =
and type_term_lhost = function
| TVar _
| TResult _ -> ()
| TMem t -> ignore (type_term ~force:false ~ctx:Other t)
| TMem t -> ignore (type_term ~use_gmp_opt:true ~ctx:Other t)
and type_term_offset = function
| TNoOffset -> ()
......@@ -494,7 +495,7 @@ and type_term_offset = function
| TModel(_, toff) -> type_term_offset toff
| TIndex(t, toff) ->
let ctx = offset_ty t in
ignore (type_term ~force:true ~ctx t);
ignore (type_term ~use_gmp_opt:false ~ctx t);
type_term_offset toff
let rec type_predicate p =
......@@ -511,12 +512,12 @@ let rec type_predicate p =
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
let i = Ival.join i1 i2 in
mk_ctx ~force:false (ty_of_interv ~ctx:c_int i)
mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:c_int i)
with Interval.Not_an_integer ->
Other
in
ignore (type_term ~force:false ~ctx t1);
ignore (type_term ~force:false ~ctx t2);
ignore (type_term ~use_gmp_opt:true ~ctx t1);
ignore (type_term ~use_gmp_opt:true ~ctx t2);
(match ctx with
| Other -> c_int
| Gmp | C_type _ -> ctx)
......@@ -532,8 +533,8 @@ let rec type_predicate p =
ignore (type_predicate p);
c_int
| Pif(t, p1, p2) ->
let ctx = mk_ctx ~force:true c_int in
ignore (type_term ~force:true ~ctx t);
let ctx = mk_ctx ~use_gmp_opt:false c_int in
ignore (type_term ~use_gmp_opt:false ~ctx t);
ignore (type_predicate p1);
ignore (type_predicate p2);
c_int
......@@ -560,7 +561,7 @@ let rec type_predicate p =
in
let i = Ival.join i1 i2 in
let ctx = match x.lv_type with
| Linteger -> mk_ctx ~force:false (ty_of_interv ~ctx:Gmp i)
| Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmp i)
| Ctype ty ->
(match Cil.unrollType ty with
| TInt(ik, _) -> C_type ik
......@@ -575,8 +576,8 @@ let rec type_predicate p =
in
(* forcing when typing bounds prevents to generate an extra useless
GMP variable when --e-acsl-gmp-only *)
ignore (type_term ~force:true ~ctx t1);
ignore (type_term ~force:true ~ctx t2);
ignore (type_term ~use_gmp_opt:false ~ctx t1);
ignore (type_term ~use_gmp_opt:false ~ctx t2);
Interval.Env.add x i)
guards;
(type_predicate goal).ty
......@@ -587,7 +588,7 @@ let rec type_predicate p =
| Pvalid(_, t)
| Pvalid_read(_, t)
| Pvalid_function t ->
ignore (type_term ~force:false ~ctx:Other t);
ignore (type_term ~use_gmp_opt:true ~ctx:Other t);
c_int
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
......@@ -598,10 +599,10 @@ let rec type_predicate p =
in
coerce ~arith_operand:false ~ctx:c_int ~op c_int
let type_term ~force ?ctx t =
let type_term ~use_gmp_opt ?ctx t =
Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
Printer.pp_term t (Pretty_utils.pp_opt pretty) ctx;
ignore (type_term ~force ?ctx t)
ignore (type_term ~use_gmp_opt ?ctx t)
let type_named_predicate ?(must_clear=true) p =
Options.feedback ~dkey ~level:3 "typing predicate '%a'."
......
......@@ -81,9 +81,9 @@ val join: integer_ty -> integer_ty -> integer_ty
(** {2 Typing} *)
(******************************************************************************)
val type_term: force:bool -> ?ctx:integer_ty -> term -> unit
val type_term: use_gmp_opt:bool -> ?ctx:integer_ty -> term -> unit
(** Compute the type of each subterm of the given term in the given context. If
[force] is true, then the conversion to the given context is done even if
[use_gmp_opt] is false, then the conversion to the given context is done even if
-e-acsl-gmp-only is set. *)
val type_named_predicate: ?must_clear:bool -> predicate -> unit
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment