From cef75793eb3b261939ed77ab0e6238d3c29aa94f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 30 Mar 2020 15:29:27 +0200
Subject: [PATCH] [kernel] refactor expr-to-term
---
.Makefile.lint | 1 -
src/kernel_internals/typing/asm_contracts.ml | 240 +++++++--------
src/kernel_internals/typing/cabs2cil.ml | 6 +-
src/kernel_services/ast_data/alarms.ml | 73 ++---
.../ast_data/statuses_by_call.ml | 2 +-
.../ast_queries/logic_typing.ml | 2 +-
.../ast_queries/logic_utils.ml | 273 ++++++++++--------
.../ast_queries/logic_utils.mli | 79 +++--
.../ast_transformations/inline.ml | 2 +-
src/plugins/aorai/aorai_dataflow.ml | 2 +-
src/plugins/aorai/aorai_utils.ml | 9 +-
src/plugins/instantiate/basic_blocks.ml | 6 +-
src/plugins/occurrence/register_gui.ml | 2 +-
src/plugins/studia/studia_gui.ml | 2 +-
src/plugins/value/domains/traces_domain.ml | 8 +-
src/plugins/wp/LogicSemantics.ml | 2 +-
tests/spec/expr_to_term.ml | 6 +-
17 files changed, 392 insertions(+), 323 deletions(-)
diff --git a/.Makefile.lint b/.Makefile.lint
index 0fffac31e24..140545ce013 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -10,7 +10,6 @@ ML_LINT_KO+=src/kernel_internals/runtime/messages.ml
ML_LINT_KO+=src/kernel_internals/runtime/messages.mli
ML_LINT_KO+=src/kernel_internals/runtime/special_hooks.ml
ML_LINT_KO+=src/kernel_internals/typing/allocates.ml
-ML_LINT_KO+=src/kernel_internals/typing/asm_contracts.ml
ML_LINT_KO+=src/kernel_internals/typing/frontc.mli
ML_LINT_KO+=src/kernel_internals/typing/infer_annotations.ml
ML_LINT_KO+=src/kernel_internals/typing/mergecil.mli
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 45ea1252e59..d87771d648f 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/src/kernel_internals/typing/asm_contracts.ml
@@ -33,24 +33,24 @@ let emitter =
let find_out_lval l =
let treat_one_lval (output, input) (_,constr, lv) =
- let tlv = Logic_utils.lval_to_term_lval ~cast:false lv in
+ let tlv = Logic_utils.lval_to_term_lval lv in
match constr with
- | "" -> tlv :: output, input
- | _ ->
- (* '+' indicates that the lval is used both as input and as output.
- GNU syntax allows it only at the beginning of the constraint, but
- actual implementation is more liberal and emits only a warning.
- *)
- if String.contains constr '+' then begin
- if constr.[0] <> '+' then
- Kernel.warning
- "output constraint '+' is not at the beginning in output operand";
- tlv::output,
- (* avoid sharing ids *)
- Visitor.visitFramacTermLval
- (new Visitor.frama_c_refresh(Project.current())) tlv
- :: input
- end else tlv::output, input
+ | "" -> tlv :: output, input
+ | _ ->
+ (* '+' indicates that the lval is used both as input and as output.
+ GNU syntax allows it only at the beginning of the constraint, but
+ actual implementation is more liberal and emits only a warning.
+ *)
+ if String.contains constr '+' then begin
+ if constr.[0] <> '+' then
+ Kernel.warning
+ "output constraint '+' is not at the beginning in output operand";
+ tlv::output,
+ (* avoid sharing ids *)
+ Visitor.visitFramacTermLval
+ (new Visitor.frama_c_refresh(Project.current())) tlv
+ :: input
+ end else tlv::output, input
in
let output, input =
List.fold_left treat_one_lval ([],[]) l
@@ -63,7 +63,7 @@ let extract_term_lval acc (_,_,e) =
object
inherit Visitor.frama_c_inplace
method! vlval lv =
- res := Logic_utils.lval_to_term_lval ~cast:false lv :: !res;
+ res := Logic_utils.lval_to_term_lval lv :: !res;
Cil.SkipChildren
end
in
@@ -112,123 +112,123 @@ let extract_mem_terms ~loc l =
List.rev (List.fold_left (extract_mem_term ~loc) [] l)
class visit_assembly =
-object(self)
- inherit Visitor.frama_c_inplace
+ object(self)
+ inherit Visitor.frama_c_inplace
- method! vinst i =
- let stmt = Extlib.the self#current_stmt in
- let kf = Extlib.the self#current_kf in
- match i with
+ method! vinst i =
+ let stmt = Extlib.the self#current_stmt in
+ let kf = Extlib.the self#current_kf in
+ match i with
| Asm(_, _, Some { asm_outputs; asm_inputs; asm_clobbers }, loc) ->
- let lv_out, lv_from = find_out_lval asm_outputs in
- let lv_from = lv_from @ find_input_lval asm_inputs in
- let mem_output = extract_mem_terms ~loc lv_from in
- let lv_out = lv_out @ mem_output in
- let lv_from = lv_from @ mem_output in
- let lv_from =
- List.filter
- (fun lv ->
- not (Logic_utils.isLogicArrayType (Cil.typeOfTermLval lv)))
- lv_from
+ let lv_out, lv_from = find_out_lval asm_outputs in
+ let lv_from = lv_from @ find_input_lval asm_inputs in
+ let mem_output = extract_mem_terms ~loc lv_from in
+ let lv_out = lv_out @ mem_output in
+ let lv_from = lv_from @ mem_output in
+ let lv_from =
+ List.filter
+ (fun lv ->
+ not (Logic_utils.isLogicArrayType (Cil.typeOfTermLval lv)))
+ lv_from
+ in
+ (* the only interesting information for clobbers is the
+ presence of the "memory" keyword, which indicates that
+ memory may have been accessed (read or write) outside of
+ the locations explicitly referred to as output or
+ input. We can't do much more than emitting a warning and
+ considering that nothing is touched beyond normally
+ specified outputs and inputs. *)
+ let mem_clobbered = List.mem "memory" asm_clobbers in
+ if mem_clobbered then begin
+ let source = fst (Cil_datatype.Instr.loc i) in
+ let once = true in
+ Kernel.warning
+ ~once ~source
+ "Clobber list contains \"memory\" argument. Assuming no \
+ side effects beyond those mentioned in operands."
+ end;
+ let to_id_term lv =
+ Logic_const.new_identified_term
+ (Logic_const.term ~loc (TLval lv) (Cil.typeOfTermLval lv))
+ in
+ let to_id_from lv =
+ let typ = Cil.typeOfTermLval lv in
+ let base_term = Logic_const.term ~loc (TLval lv) typ in
+ let term =
+ if Logic_utils.isLogicPointerType typ ||
+ Logic_utils.isLogicArrayType typ
+ then { base_term with term_name = ["indirect"] }
+ else base_term
in
- (* the only interesting information for clobbers is the
- presence of the "memory" keyword, which indicates that
- memory may have been accessed (read or write) outside of
- the locations explicitly referred to as output or
- input. We can't do much more than emitting a warning and
- considering that nothing is touched beyond normally
- specified outputs and inputs. *)
- let mem_clobbered = List.mem "memory" asm_clobbers in
- if mem_clobbered then begin
- let source = fst (Cil_datatype.Instr.loc i) in
- let once = true in
- Kernel.warning
- ~once ~source
- "Clobber list contains \"memory\" argument. Assuming no \
- side effects beyond those mentioned in operands."
- end;
- let to_id_term lv =
- Logic_const.new_identified_term
- (Logic_const.term ~loc (TLval lv) (Cil.typeOfTermLval lv))
- in
- let to_id_from lv =
- let typ = Cil.typeOfTermLval lv in
- let base_term = Logic_const.term ~loc (TLval lv) typ in
- let term =
- if Logic_utils.isLogicPointerType typ ||
- Logic_utils.isLogicArrayType typ
- then { base_term with term_name = ["indirect"] }
- else base_term
- in
- Logic_const.new_identified_term term
- in
- let assigns () =
- Writes
- (List.map
- (fun x -> (to_id_term x, From (List.map to_id_from lv_from)))
- lv_out)
- in
- let filter ca =
- match ca.annot_content with
- (* search for a statement contract that applies to all cases. *)
- | AStmtSpec ([],_) -> true
- | _ -> false
- in
- let contracts = Annotations.code_annot ~filter stmt in
- (match contracts with
- | [] ->
- let assigns = assigns () in
- let bhv = Cil.mk_behavior ~assigns () in
- let spec = Cil.empty_funspec () in
- spec.spec_behavior <- [ bhv ];
- let ca =
- Logic_const.new_code_annotation (AStmtSpec ([],spec))
- in
- Annotations.add_code_annot emitter ~kf stmt ca;
- if not mem_clobbered && Kernel.AsmContractsAutoValidate.get()
- then begin
- let active = [] in
- let ip_assigns =
- Property.ip_assigns_of_behavior kf (Kstmt stmt) ~active bhv in
- let ip_from =
- Property.ip_from_of_behavior kf (Kstmt stmt) ~active bhv in
- List.iter
- Property_status.(
- fun x -> emit emitter ~hyps:[] x True)
- (Extlib.list_of_opt ip_assigns @ ip_from)
- end
- | [ { annot_content = AStmtSpec ([], spec) } ] ->
- (* Already existing contracts. Just add assigns clause for
- behaviors that do not already have one. *)
+ Logic_const.new_identified_term term
+ in
+ let assigns () =
+ Writes
+ (List.map
+ (fun x -> (to_id_term x, From (List.map to_id_from lv_from)))
+ lv_out)
+ in
+ let filter ca =
+ match ca.annot_content with
+ (* search for a statement contract that applies to all cases. *)
+ | AStmtSpec ([],_) -> true
+ | _ -> false
+ in
+ let contracts = Annotations.code_annot ~filter stmt in
+ (match contracts with
+ | [] ->
+ let assigns = assigns () in
+ let bhv = Cil.mk_behavior ~assigns () in
+ let spec = Cil.empty_funspec () in
+ spec.spec_behavior <- [ bhv ];
+ let ca =
+ Logic_const.new_code_annotation (AStmtSpec ([],spec))
+ in
+ Annotations.add_code_annot emitter ~kf stmt ca;
+ if not mem_clobbered && Kernel.AsmContractsAutoValidate.get()
+ then begin
+ let active = [] in
+ let ip_assigns =
+ Property.ip_assigns_of_behavior kf (Kstmt stmt) ~active bhv in
+ let ip_from =
+ Property.ip_from_of_behavior kf (Kstmt stmt) ~active bhv in
List.iter
- (fun bhv ->
- match bhv.b_assigns with
- | WritesAny ->
- let behavior = bhv.b_name in
- let assigns = assigns () in
- let keep_empty = false in
- Annotations.add_assigns
- ~keep_empty emitter kf ~stmt ~behavior assigns;
- | Writes _ -> ())
- spec.spec_behavior
- | _ ->
- Kernel.fatal "Several contracts found for the same statement %a"
- Printer.pp_stmt stmt
- );
- Cil.SkipChildren
+ Property_status.(
+ fun x -> emit emitter ~hyps:[] x True)
+ (Extlib.list_of_opt ip_assigns @ ip_from)
+ end
+ | [ { annot_content = AStmtSpec ([], spec) } ] ->
+ (* Already existing contracts. Just add assigns clause for
+ behaviors that do not already have one. *)
+ List.iter
+ (fun bhv ->
+ match bhv.b_assigns with
+ | WritesAny ->
+ let behavior = bhv.b_name in
+ let assigns = assigns () in
+ let keep_empty = false in
+ Annotations.add_assigns
+ ~keep_empty emitter kf ~stmt ~behavior assigns;
+ | Writes _ -> ())
+ spec.spec_behavior
+ | _ ->
+ Kernel.fatal "Several contracts found for the same statement %a"
+ Printer.pp_stmt stmt
+ );
+ Cil.SkipChildren
| Asm(_,_,None,_) ->
Kernel.feedback
~dkey:Kernel.dkey_asm_contracts "Ignoring basic assembly instruction";
Cil.SkipChildren
| _ -> Cil.SkipChildren
-end
+ end
let transform file =
if Kernel.AsmContractsGenerate.get() then
Visitor.visitFramacFileSameGlobals (new visit_assembly) file
let () =
- File.add_code_transformation_after_cleanup
+ File.add_code_transformation_after_cleanup
~deps:[(module Kernel.AsmContractsGenerate);
(module Kernel.AsmContractsAutoValidate) ]
category
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 57c91da7c3e..6dc8c4bda1a 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -8856,9 +8856,9 @@ and createLocal ghost ((_, sto, _, _) as specs)
(se0 +++ (
let castloc = CurrentLoc.get () in
let talloca_size =
- let telt_size = Logic_utils.expr_to_term ~cast:false elt_size in
- let tlen = Logic_utils.expr_to_term ~cast:false len in
- Logic_const.term (TBinOp (Mult,telt_size,tlen)) telt_size.term_type
+ let size = Logic_utils.expr_to_term ~coerce:true elt_size in
+ let tlen = Logic_utils.expr_to_term ~coerce:true len in
+ Logic_const.term (TBinOp (Mult,size,tlen)) Linteger
in
let pos_size =
let zero = Logic_const.tinteger ~loc:castloc 0 in
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index f251a750c84..903e79bb9f0 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -451,21 +451,21 @@ let overflowed_expr_to_term ~loc e =
let loc = best_loc ~loc e.eloc in
match e.enode with
| UnOp(op, e, ty) ->
- let t = Logic_utils.expr_to_term ~cast:true e in
- let ty = Logic_utils.typ_to_logic_type ty in
+ let t = Logic_utils.expr_to_term ~coerce:true e in
+ let ty = Logic_utils.coerced ty in
Logic_const.term ~loc (TUnOp(op, t)) ty
| BinOp(op, e1, e2, ty) ->
- let t1 = Logic_utils.expr_to_term ~cast:true e1 in
- let t2 = Logic_utils.expr_to_term ~cast:true e2 in
- let ty = Logic_utils.typ_to_logic_type ty in
+ let t1 = Logic_utils.expr_to_term ~coerce:true e1 in
+ let t2 = Logic_utils.expr_to_term ~coerce:true e2 in
+ let ty = Logic_utils.coerced ty in
Logic_const.term ~loc (TBinOp(op, t1, t2)) ty
- | _ -> Logic_utils.expr_to_term ~cast:true e
+ | _ -> Logic_utils.expr_to_term ~coerce:true e
(* Creates \is_finite((fkind)e) or \is_nan((fkind)e) according to
[predicate]. *)
let create_special_float_predicate ~loc e fkind predicate =
let loc = best_loc ~loc e.eloc in
- let t = Logic_utils.expr_to_term ~cast:true e in
+ let t = Logic_utils.expr_to_term e in
let typ = match fkind with
| FFloat -> Cil.floatType
| FDouble -> Cil.doubleType
@@ -490,7 +490,7 @@ let create_predicate ?(loc=Location.unknown) alarm =
| Division_by_zero e ->
(* e != 0 *)
let loc = best_loc ~loc e.eloc in
- let t = Logic_utils.expr_to_term ~cast:true e in
+ let t = Logic_utils.expr_to_term ~coerce:true e in
Logic_const.prel ~loc (Rneq, t, Cil.lzero ())
| Memory_access(lv, read) ->
@@ -500,22 +500,23 @@ let create_predicate ?(loc=Location.unknown) alarm =
| For_writing -> Logic_const.pvalid
in
let e = Cil.mkAddrOrStartOf ~loc lv in
- let t = Logic_utils.expr_to_term ~cast:true e in
+ let t = Logic_utils.expr_to_term e in
valid ~loc (Logic_const.here_label, t)
| Index_out_of_bound(e1, e2) ->
(* 0 <= e1 < e2, left part if None, right part if Some e *)
let loc = best_loc ~loc e1.eloc in
- let t1 = Logic_utils.expr_to_term ~cast:true e1 in
+ let t1 = Logic_utils.expr_to_term ~coerce:true e1 in
(match e2 with
- | None -> Logic_const.prel ~loc (Rle, Cil.lzero (), t1)
+ | None ->
+ Logic_const.prel ~loc (Rle, Cil.lzero (), t1)
| Some e2 ->
- let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+ let t2 = Logic_utils.expr_to_term ~coerce:true e2 in
Logic_const.prel ~loc (Rlt, t1, t2))
| Invalid_pointer e ->
let loc = best_loc ~loc e.eloc in
- let t = Logic_utils.expr_to_term ~cast:true e in
+ let t = Logic_utils.expr_to_term e in
if Cil.isFunPtrType (Cil.typeOf e)
then Logic_const.pvalid_function ~loc t
else Logic_const.pobject_pointer ~loc (Logic_const.here_label, t)
@@ -523,12 +524,12 @@ let create_predicate ?(loc=Location.unknown) alarm =
| Invalid_shift(e, n) ->
(* 0 <= e < n *)
let loc = best_loc ~loc e.eloc in
- let t = Logic_utils.expr_to_term ~cast:true e in
+ let t = Logic_utils.expr_to_term ~coerce:true e in
let low_cmp = Logic_const.prel ~loc (Rle, Cil.lzero (), t) in
(match n with
| None -> low_cmp
| Some n ->
- let tn = Logic_const.tint ~loc (Integer.of_int n) in
+ let tn = Logic_const.tinteger ~loc n in
let up_cmp = Logic_const.prel ~loc (Rlt, t, tn) in
Logic_const.pand ~loc (low_cmp, up_cmp))
@@ -544,21 +545,21 @@ let create_predicate ?(loc=Location.unknown) alarm =
let zero = Cil.lzero () in
Logic_const.term (TCastE (typ, zero)) (Ctype typ)
end
- | Some e -> Logic_utils.expr_to_term ~cast:true e
+ | Some e -> Logic_utils.expr_to_term e
in
- let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+ let t2 = Logic_utils.expr_to_term e2 in
Logic_utils.pointer_comparable ~loc t1 t2
| Differing_blocks(e1, e2) ->
(* \base_addr(e1) == \base_addr(e2) *)
let loc = best_loc ~loc e1.eloc in
- let t1 = Logic_utils.expr_to_term ~cast:true e1 in
+ let t1 = Logic_utils.expr_to_term e1 in
let here = Logic_const.here_label in
let typ = Ctype Cil.charPtrType in
let t1 =
Logic_const.term ~loc:(best_loc loc e1.eloc) (Tbase_addr(here, t1)) typ
in
- let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+ let t2 = Logic_utils.expr_to_term e2 in
let t2 =
Logic_const.term ~loc:(best_loc loc e2.eloc) (Tbase_addr(here, t2)) typ
in
@@ -569,10 +570,10 @@ let create_predicate ?(loc=Location.unknown) alarm =
let loc = best_loc ~loc e.eloc in
let t = match kind with
| Pointer_downcast ->
- let t = Logic_utils.expr_to_term ~cast:true e in
+ let t = Logic_utils.expr_to_term e in
Logic_const.tcast ~loc t Cil.theMachine.upointType
| Signed_downcast | Unsigned_downcast ->
- Logic_utils.expr_to_term ~cast:true e
+ Logic_utils.expr_to_term ~coerce:true e
| _ ->
(* For overflows, the computation must be done on mathematical types,
else the value is necessarily in bounds. *)
@@ -580,7 +581,9 @@ let create_predicate ?(loc=Location.unknown) alarm =
in
let tn = Logic_const.tint ~loc n in
Logic_const.prel ~loc
- (match bound with Lower_bound -> Rle, tn, t | Upper_bound -> Rle, t, tn)
+ (match bound with
+ | Lower_bound -> Rle, tn, t
+ | Upper_bound -> Rle, t, tn)
| Float_to_int(e, n, bound) ->
(* n < e or e < n according to bound *)
@@ -588,27 +591,31 @@ let create_predicate ?(loc=Location.unknown) alarm =
let te = overflowed_expr_to_term ~loc e in
let t = Logic_const.tlogic_coerce ~loc te Lreal in
let n =
- (match bound with Lower_bound -> Integer.sub | Upper_bound -> Integer.add)
+ (match bound with
+ | Lower_bound -> Integer.sub
+ | Upper_bound -> Integer.add)
n Integer.one
in
let tn = Logic_const.tlogic_coerce ~loc (Logic_const.tint ~loc n) Lreal in
Logic_const.prel ~loc
- (match bound with Lower_bound -> Rlt, tn, t | Upper_bound -> Rlt, t, tn)
+ (match bound with
+ | Lower_bound -> Rlt, tn, t
+ | Upper_bound -> Rlt, t, tn)
| Not_separated(lv1, lv2) ->
(* \separated(lv1, lv2) *)
let e1 = Cil.mkAddrOf ~loc lv1 in
- let t1 = Logic_utils.expr_to_term ~cast:true e1 in
+ let t1 = Logic_utils.expr_to_term e1 in
let e2 = Cil.mkAddrOf ~loc lv2 in
- let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+ let t2 = Logic_utils.expr_to_term e2 in
Logic_const.pseparated ~loc [ t1; t2 ]
| Overlap(lv1, lv2) ->
(* (lv1 == lv2) || \separated(lv1, lv2) *)
let e1 = Cil.mkAddrOf ~loc lv1 in
- let t1 = Logic_utils.expr_to_term ~cast:true e1 in
+ let t1 = Logic_utils.expr_to_term e1 in
let e2 = Cil.mkAddrOf ~loc lv2 in
- let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+ let t2 = Logic_utils.expr_to_term e2 in
let eq = Logic_const.prel ~loc (Req, t1, t2) in
let sep = Logic_const.pseparated ~loc [ t1; t2 ] in
Logic_const.por ~loc (eq, sep)
@@ -616,13 +623,13 @@ let create_predicate ?(loc=Location.unknown) alarm =
| Uninitialized lv ->
(* \initialized(lv) *)
let e = Cil.mkAddrOrStartOf ~loc lv in
- let t = Logic_utils.expr_to_term ~cast:false e in
+ let t = Logic_utils.expr_to_term e in
Logic_const.pinitialized ~loc (Logic_const.here_label, t)
| Dangling lv ->
(* !\dangling(lv) *)
let e = Cil.mkAddrOrStartOf ~loc lv in
- let t = Logic_utils.expr_to_term ~cast:false e in
+ let t = Logic_utils.expr_to_term e in
Logic_const.(pnot ~loc (pdangling ~loc (Logic_const.here_label, t)))
| Is_nan_or_infinite (e, fkind) ->
@@ -648,14 +655,14 @@ let create_predicate ?(loc=Location.unknown) alarm =
that has unexpected type %a (unrolled as %a)"
Printer.pp_exp e Printer.pp_typ t Printer.pp_typ t'
in
- let t = Logic_utils.expr_to_term ~cast:true e in
+ let t = Logic_utils.expr_to_term e in
Logic_const.(pvalid_function ~loc t)
| Uninitialized_union llv ->
(* \initialized(lv_1) || ... || \initialized(lv_n) *)
let make_lval_predicate lv =
let e = Cil.mkAddrOrStartOf ~loc lv in
- let t = Logic_utils.expr_to_term ~cast:false e in
+ let t = Logic_utils.expr_to_term e in
Logic_const.pinitialized ~loc (Logic_const.here_label, t)
in
List.fold_left (fun acc lv ->
@@ -666,7 +673,7 @@ let create_predicate ?(loc=Location.unknown) alarm =
| Invalid_bool lv ->
let e = Cil.new_exp ~loc (Lval lv) in
- let t = Logic_utils.expr_to_term ~cast:false e in
+ let t = Logic_utils.expr_to_term ~coerce:true e in
let zero = Logic_const.prel ~loc (Req, t, Cil.lzero ()) in
let one = Logic_const.prel ~loc (Req, t, Cil.lone ()) in
Logic_const.por ~loc (zero, one)
diff --git a/src/kernel_services/ast_data/statuses_by_call.ml b/src/kernel_services/ast_data/statuses_by_call.ml
index d5deb1ab108..2487ade6c49 100644
--- a/src/kernel_services/ast_data/statuses_by_call.ml
+++ b/src/kernel_services/ast_data/statuses_by_call.ml
@@ -160,7 +160,7 @@ let rec associate acc ~formals ~concretes =
| [], _ -> acc
| _, [] -> raise Non_Transposable
| formal :: formals, concrete :: concretes ->
- let term = Logic_utils.expr_to_term ~cast:true concrete in
+ let term = Logic_utils.expr_to_term concrete in
associate ((formal, term) :: acc) ~formals ~concretes
let transpose_pred_at_callsite ~formals ~concretes pred =
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index f6a1c015fb9..27e77ae549a 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -801,7 +801,7 @@ struct
let attrs = Cil.filter_qualifier_attributes attrs in
let field = C.find_comp_field comp f in
let typ = Cil.typeOffset ty field in
- Logic_utils.offset_to_term_offset ~cast:false field,
+ Logic_utils.offset_to_term_offset field,
Ctype (Cil.typeAddAttributes attrs typ)
with Not_found -> C.error loc "cannot find field %s" f)
| _ ->
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index a77518acee2..8a43475ab1c 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -123,11 +123,11 @@ let plain_array_to_ptr ty =
let array_to_ptr = plain_or_set plain_array_to_ptr
-let typ_to_logic_type e_typ =
- let ty = Cil.unrollType e_typ in
+let coerced typ =
+ let ty = Cil.unrollType typ in
if Cil.isIntegralType ty then Linteger
else if Cil.isFloatingType ty then Lreal
- else Ctype e_typ
+ else Ctype typ
let predicate_of_identified_predicate ip = ip.ip_content
@@ -292,7 +292,6 @@ let lconstant_to_constant c = match c with
| LReal r -> CReal (r.r_nearest,FDouble,Some r.r_literal)
| LEnum e -> CEnum e
-
let string_to_float_lconstant string =
let f = snd (Floating_point.parse string) in
(* If the string has suffix 'F' or 'D', then it represents a single or double
@@ -346,24 +345,27 @@ let is_zero_comparable t =
let scalar_term_conversion conversion t =
let loc = t.term_loc in
- let arith_conversion () = conversion ~loc false t (Cil.lzero ~loc ()) in
- let ptr_conversion () =
- conversion ~loc false t (Logic_const.term ~loc Tnull t.term_type)
- in
+ let arith_conversion t =
+ conversion ~loc false t (Cil.lzero ~loc ()) in
+ let real_conversion ?ltyp t =
+ conversion ~loc false t (Logic_const.treal_zero ~loc ?ltyp ()) in
+ let ptr_conversion t =
+ conversion ~loc false t (Logic_const.term ~loc Tnull t.term_type) in
+ let bool_conversion t =
+ let ctrue = Logic_env.Logic_ctor_info.find "\\true" in
+ conversion ~loc true t (term ~loc (TDataCons(ctrue,[])) boolean_type) in
match unroll_type t.term_type with
- | Ctype (TInt _) -> arith_conversion ()
- | Ctype (TFloat _) ->
- conversion ~loc false t (Logic_const.treal_zero ~loc ~ltyp:t.term_type ())
- | Ctype (TPtr _) -> ptr_conversion ()
- | Ctype (TArray _) -> ptr_conversion ()
+ | Ctype (TInt _) -> arith_conversion t
+ | Ctype (TFloat _) as ltyp -> real_conversion ~ltyp t
+ | Ctype (TPtr _) -> ptr_conversion t
+ | Ctype (TArray _) -> ptr_conversion t
(* Could be transformed to \true: an array is never \null *)
- | Ctype (TFun _) -> ptr_conversion ()
+ | Ctype (TFun _) -> ptr_conversion t
(* decay as pointer *)
- | Linteger -> arith_conversion ()
- | Lreal -> conversion ~loc false t (Logic_const.treal_zero ~loc ())
+ | Linteger -> arith_conversion t
+ | Lreal -> real_conversion t
| Ltype ({lt_name = name},[]) when name = Utf8_logic.boolean ->
- let ctrue = Logic_env.Logic_ctor_info.find "\\true" in
- conversion ~loc true t (term ~loc (TDataCons(ctrue,[])) boolean_type)
+ bool_conversion t
| Ltype _ | Lvar _ | Larrow _
| Ctype (TVoid _ | TNamed _ | TComp _ | TEnum _ | TBuiltin_va_list _)
-> Kernel.fatal
@@ -386,124 +388,159 @@ let scalar_term_to_boolean =
(* --- Expr Conversion --- *)
(* -------------------------------------------------------------------------- *)
-let rec expr_to_term ~cast e =
+let is_boolean_binop op =
+ let open Cil_types in
+ match op with
+ | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr -> true
+ | PlusA | PlusPI | IndexPI | MinusA | MinusPI | MinusPP
+ | Mult | Div | Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr -> false
+
+let float_builtin prefix fkind =
+ let name = match fkind with
+ | FFloat -> Printf.sprintf "\\%s_float" prefix
+ | FDouble | FLongDouble -> Printf.sprintf "\\%s_double" prefix
+ in match Logic_env.find_all_logic_functions name with
+ | [ lf ] -> Some lf
+ | _ -> Kernel.fatal "Missing or ambiguous builtin %S" name
+
+let is_float_binop op typ =
+ match typ, op with
+ | TFloat(fkind,_) , PlusA -> float_builtin "add" fkind
+ | TFloat(fkind,_) , MinusA -> float_builtin "sub" fkind
+ | TFloat(fkind,_) , Mult -> float_builtin "mul" fkind
+ | TFloat(fkind,_) , Div -> float_builtin "div" fkind
+ | _ -> None
+
+let is_float_unop op typ =
+ match typ, op with
+ | TFloat(fkind,_) , Neg -> float_builtin "neg" fkind
+ | _ -> None
+
+let rec expr_to_term ?(coerce=false) e =
let loc = e.eloc in
- let typ = unrollType (Cil.typeOf e) in
- let result = match e.enode with
- | Const c -> TConst (constant_to_lconstant c)
- | SizeOf t -> TSizeOf t
- | SizeOfE e -> TSizeOfE (expr_to_term ~cast e)
- | SizeOfStr s -> TSizeOfStr s
- | StartOf lv -> TStartOf (lval_to_term_lval ~cast lv)
- | AddrOf lv -> TAddrOf (lval_to_term_lval ~cast lv)
- | CastE (ty,e) -> (mk_cast (unrollType ty) (expr_to_term ~cast e)).term_node
- | BinOp (op, l, r, _) ->
- let l' = expr_to_term_coerce ~cast l in
- let r' = expr_to_term_coerce ~cast r in
- (* type of the conversion of e in the logic. Beware that boolean
- operators have boolean type. *)
- let tcast =
- match op, cast with
- | ( Cil_types.Lt | Cil_types.Gt | Cil_types.Le | Cil_types.Ge
- | Cil_types.Eq | Cil_types.Ne| Cil_types.LAnd | Cil_types.LOr),
- _ -> Some Logic_const.boolean_type
- | _, true -> Some (typ_to_logic_type typ)
- | _, false -> None
- in
- let tnode = TBinOp (op,l',r') in
- (* if [cast], we add a cast. Otherwise, when [op] is an operator
- returning a boolean, we need to cast the whole expression as an
- integral type, because (1) the recursive subcalls expect an
- integer/float/pointer here, and (2) there is no implicit conversion
- Boolean -> integer. *)
- begin match tcast with
- | Some lt -> (mk_cast typ (Logic_const.term tnode lt)).term_node
- | None -> tnode
+ let typ = Cil.unrollType (Cil.typeOf e) in
+ let ctyp = Ctype typ in
+ let node,ltyp =
+ match e.enode with
+ | Const c -> TConst (constant_to_lconstant c) , coerced typ
+ | StartOf lv -> TStartOf (lval_to_term_lval lv) , ctyp
+ | AddrOf lv -> TAddrOf (lval_to_term_lval lv) , ctyp
+ | BinOp (op, a, b, _) ->
+ if is_boolean_binop op then
+ let tc = expr_to_boolean e in
+ Tif( tc , Cil.lone ~loc () , Cil.lzero ~loc () ),
+ Linteger
+ else begin match is_float_binop op typ with
+ | Some phi ->
+ let va = expr_to_term a in
+ let vb = expr_to_term b in
+ Tapp(phi,[],[va;vb]) , ctyp
+ | None ->
+ let va = expr_to_term ~coerce:true a in
+ let vb = expr_to_term ~coerce:true b in
+ TBinOp(op,va,vb) , coerced typ
end
- | UnOp (op, u, _) ->
- let u' = expr_to_term_coerce ~cast u in
- let u' =
- match op with
- | Cil_types.LNot ->
- (match u'.term_node with
- | TCastE(_, t) when is_boolean_type t.term_type -> t
- | _ when is_boolean_type u'.term_type -> u'
- | _ when is_zero_comparable u' ->
- scalar_term_to_boolean u'
- | _ ->
- Kernel.fatal
- "expr_to_term: unexpected argument of ! operator %a, \
- converted to %a"
- Cil_printer.pp_exp u Cil_printer.pp_term u')
- | _ -> u'
- in
- (* See comments for binop case above. *)
- let tcast = match op, cast with
- | Cil_types.LNot, _ -> Some Logic_const.boolean_type
- | _, true -> Some (typ_to_logic_type typ)
- | _, false -> None
- in
- let tnode = TUnOp (op, u') in
- begin match tcast with
- | Some lt -> (mk_cast typ (Logic_const.term tnode lt)).term_node
- | None -> tnode
+ | UnOp (LNot, c, _) ->
+ let tc = expr_to_boolean c in
+ Tif( tc , Cil.lzero ~loc () , Cil.lone ~loc () ),
+ Linteger
+ | UnOp(op, a, _) ->
+ begin match is_float_unop op typ with
+ | Some phi ->
+ let va = expr_to_term ~coerce:true a in
+ Tapp(phi,[],[va]) , ctyp
+ | None ->
+ let va = expr_to_term ~coerce:true a in
+ TUnOp(op,va) , coerced typ
end
- | AlignOfE e -> TAlignOfE (expr_to_term ~cast e)
- | AlignOf typ -> TAlignOf typ
- | Lval lv -> TLval (lval_to_term_lval ~cast lv)
- | Info (e,_) -> (expr_to_term ~cast e).term_node
+ | SizeOf t -> TSizeOf t, ctyp
+ | SizeOfE e -> TSizeOf (Cil.typeOf e), ctyp
+ | SizeOfStr s -> TSizeOfStr s, ctyp
+ | AlignOf typ -> TAlignOf typ, ctyp
+ | AlignOfE e -> TAlignOf (Cil.typeOf e), ctyp
+ | Lval lv -> TLval (lval_to_term_lval lv), ctyp
+ | CastE (ty,e) ->
+ let t = mk_cast ~loc ty (expr_to_term ~coerce e) in
+ t.term_node , t.term_type
+ | Info (e,_) ->
+ let t = expr_to_term ~coerce e in
+ t.term_node , t.term_type
in
- let tres = Logic_const.term ~loc result (Ctype typ) in
- if cast then tres
- else
- match e.enode with
- (* all immediate values keep their C type by default, and are only lifted
- to integer/real if needed. *)
- | Const _ | Lval _ | CastE _ -> tres
- | _ -> numeric_coerce (typ_to_logic_type typ) tres
-
-and expr_to_term_coerce ~cast e =
- let t = expr_to_term ~cast e in
- match Logic_const.unroll_ltdef t.term_type with
- | Ctype typ when Cil.isIntegralType typ || Cil.isFloatingType typ ->
- let ltyp = typ_to_logic_type typ in
- numeric_coerce ltyp t
- | _ -> t
+ let v = mk_cast ~loc typ @@ Logic_const.term ~loc node ltyp in
+ match typ with
+ | TInt _ when coerce -> numeric_coerce Linteger v
+ | TFloat _ when coerce -> numeric_coerce Lreal v
+ | _ -> v
-and lval_to_term_lval ~cast (host,offset) =
- host_to_term_host ~cast host, offset_to_term_offset ~cast offset
+and lval_to_term_lval (host,offset) =
+ host_to_term_lhost host, offset_to_term_offset offset
-and host_to_term_host ~cast = function
+and host_to_term_lhost = function
| Var s -> TVar (Cil.cvar_to_lvar s)
- | Mem e -> TMem (expr_to_term ~cast e) (*no need of numeric coercion - pointer *)
+ | Mem e -> TMem (expr_to_term e)
-and offset_to_term_offset ~cast:cast = function
+and offset_to_term_offset = function
| NoOffset -> TNoOffset
+ | Field (fi,off) ->
+ TField(fi,offset_to_term_offset off)
| Index (e,off) ->
- TIndex (expr_to_term_coerce ~cast e,offset_to_term_offset ~cast off)
- | Field (fi,off) -> TField(fi,offset_to_term_offset ~cast off)
+ TIndex (expr_to_term ~coerce:true e,offset_to_term_offset off)
-and expr_to_predicate ~cast e =
+and expr_to_boolean e =
let open Cil_types in
+ let tbool n = Logic_const.term n Logic_const.boolean_type in
match e.enode with
- | BinOp ((Lt | Gt | Le | Ge | Eq | Ne as op), l, r, _) ->
- let tl = expr_to_term ~cast l in
- let tr = expr_to_term ~cast r in
- let rel = match op with
- | Lt -> Rlt | Gt -> Rgt | Le -> Rle | Ge -> Rge | Eq -> Req | Ne -> Rneq
- | _ -> assert false
- in
- let pred = Prel (rel, tl, tr) in
- Logic_const.new_predicate (Logic_const.unamed ~loc:e.eloc pred)
+ | UnOp(BNot, a,_) ->
+ tbool @@ TUnOp(BNot, expr_to_boolean a)
+ | BinOp((BAnd|BOr) as op,a,b,_) ->
+ let va = expr_to_boolean a in
+ let vb = expr_to_boolean b in
+ tbool @@ TBinOp(op,va,vb)
+ | BinOp(op, a, b, _) when is_boolean_binop op ->
+ let va = expr_to_term ~coerce:true a in
+ let vb = expr_to_term ~coerce:true b in
+ tbool @@ TBinOp(op,va,vb)
| _ ->
- let t = expr_to_term ~cast e in
+ let t = expr_to_term ~coerce:true e in
if is_zero_comparable t then
- Logic_const.new_predicate (scalar_term_to_predicate t)
+ scalar_term_to_boolean t
else
Kernel.fatal
"Cannot convert into predicate the C expression %a"
Cil_printer.pp_exp e
+and expr_to_predicate e =
+ let open Cil_types in
+ let unamed = Logic_const.unamed ~loc:e.eloc in
+ let prel r a b =
+ let va = expr_to_term ~coerce:true a in
+ let vb = expr_to_term ~coerce:true b in
+ unamed @@ Prel(r,va,vb)
+ in match e.enode with
+ | BinOp(Lt, a, b, _) -> prel Rlt a b
+ | BinOp(Le, a, b, _) -> prel Rle a b
+ | BinOp(Gt, a, b, _) -> prel Rgt a b
+ | BinOp(Ge, a, b, _) -> prel Rge a b
+ | BinOp(Eq, a, b, _) -> prel Req a b
+ | BinOp(Ne, a, b, _) -> prel Rneq a b
+ | BinOp(BAnd, a, b, _) ->
+ unamed @@ Pand(expr_to_predicate a,expr_to_predicate b)
+ | BinOp(BOr, a, b, _) ->
+ unamed @@ Por(expr_to_predicate a,expr_to_predicate b)
+ | UnOp(BNot, a, _) ->
+ unamed @@ Pnot(expr_to_predicate a)
+ | _ ->
+ let t = expr_to_term ~coerce:true e in
+ if is_zero_comparable t then
+ scalar_term_to_predicate t
+ else
+ Kernel.fatal
+ "Cannot convert into predicate the C expression %a"
+ Cil_printer.pp_exp e
+
+and expr_to_ipredicate e =
+ Logic_const.new_predicate (expr_to_predicate e)
+
(* ************************************************************************* *)
(** {1 Various utilities} *)
(* ************************************************************************* *)
@@ -513,8 +550,8 @@ let array_with_range arr size =
let arr = Cil.stripCasts arr in
let typ_arr = typeOf arr in
let no_cast = isAnyCharPtrType typ_arr || isAnyCharArrayType typ_arr in
- let char_ptr = typ_to_logic_type Cil.charPtrType in
- let arr = expr_to_term ~cast:true arr in
+ let char_ptr = Ctype Cil.charPtrType in
+ let arr = expr_to_term arr in
let arr =
if no_cast then arr
else mk_cast ~loc Cil.charPtrType arr
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 3853a02c250..25dff3363f4 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -86,7 +86,7 @@ val logicCType : logic_type -> typ
val array_to_ptr : logic_type -> logic_type
(** C type to logic type, with implicit conversion for arithmetic types. *)
-val typ_to_logic_type : typ -> logic_type
+val coerced : typ -> logic_type
(** {2 Predicates} *)
@@ -157,36 +157,62 @@ val pointer_comparable: ?loc:location -> term -> term -> predicate
(** \pointer_comparable
@since Fluorine-20130401 *)
-(** {2 Conversion from exp to term}
-
- translates a C expression into an "equivalent" logical term.
- [cast] specifies how C arithmetic operators are translated.
- When [cast] is [true], the translation returns a logic [term] having the
- same semantics of the C [expr] by introducing casts (i.e. the C expr [a+b]
- can be translated as [(char)(((char)a)+(char)b)] to preserve the modulo
- feature of the C addition).
- Otherwise, no such casts are introduced and the C arithmetic operators are
- translated into perfect mathematical operators (i.e. a floating point
- addition is translated into an addition of [real] numbers).
- @plugin development guide *)
-val expr_to_term : cast:bool -> exp -> term
+(** {2 Conversion from exp to term} *)
-(** same as {!expr_to_term}, except that if the new term has an arithmetic
- type, it is automatically coerced into real (or integer for integral types).
+val expr_to_term : ?coerce:bool -> exp -> term
+(** Returns a logic term that has exactly the same semantics than the
+ original C-expression. The type of the resulting term is determined
+ by the [~coerce] flag as follows:
+ - when [~coerce:false] is given (the default) the term has the same
+ c-type than the original expression.
+ - when [~coerce:true] is given, if the original expression has an int or
+ float type, then the returned term is coerced into the integer or real
+ logic type, respectively.
- @since Magnesium-20151001
+ Remark: when the original expression is a comparison, it is evaluated as
+ a [_Bool] or [integer] depending on the [~coerce] flag.
+ To obtain a boolean or predicate, use [expr_to_boolean] or
+ [expr_to_predicate] instead.
+
+ @modify Frama-C+dev
+*)
+
+val expr_to_predicate: exp -> predicate
+(** Returns a predicate semantically equivalent to the condition
+ of the original C-expression.
+
+ This is different than [expr_to_term e |> scalar_term_to_predicate]
+ since it directly translate C-relations into logic ones.
+
+ @raise Fatal error if the expression is not a comparison and cannot be
+ compared to zero.
+ @since Sulfur-20171101
+ @modify Frama-C+dev
*)
-val expr_to_term_coerce: cast:bool -> exp -> term
-val expr_to_predicate: cast:bool -> exp -> identified_predicate
-(** same as {expr_to_term}, but the result is a predicate. Expressions starting
- with relational operators ([==], [<=], etc) are translated directly.
- Otherwise, the result of [expr_to_predicate e] is the predicate
- [e <> 0].
+val expr_to_ipredicate: exp -> identified_predicate
+(** Returns a predicate semantically equivalent to the condition
+ of the original C-expression.
+
+ Identical to [expr_to_predicate e |> Logic_const.new_predicate].
+
+ @raise Fatal error if the expression is not a comparison and cannot be
+ compared to zero.
+ @since Sulfur-20171101
+ @modify Frama-C+dev
+*)
+
+val expr_to_boolean: exp -> term
+(** Returns a boolean term semantically equivalent to the condition
+ of the original C-expression.
+
+ This is different than [expr_to_term e |> scalar_term_to_predicate]
+ since it directly translate C-relations into logic ones.
@raise Fatal error if the expression is not a comparison and cannot be
compared to zero.
@since Sulfur-20171101
+ @modify Frama-C+dev
*)
val is_zero_comparable: term -> bool
@@ -212,10 +238,9 @@ val scalar_term_to_predicate: term -> predicate
@since Sulfur-20171101
*)
-val lval_to_term_lval : cast:bool -> lval -> term_lval
-val host_to_term_host : cast:bool -> lhost -> term_lhost
-val offset_to_term_offset :
- cast:bool -> offset -> term_offset
+val lval_to_term_lval : lval -> term_lval
+val host_to_term_lhost : lhost -> term_lhost
+val offset_to_term_offset : offset -> term_offset
val constant_to_lconstant: constant -> logic_constant
val lconstant_to_constant: logic_constant-> constant
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index 5cdbfc0f1e2..c078078909a 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -96,7 +96,7 @@ let inline_call loc caller callee return args =
method! vterm_lval (host,offset) =
match host, return with
| TResult _, Some lv ->
- let tlv = Logic_utils.lval_to_term_lval ~cast:false lv in
+ let tlv = Logic_utils.lval_to_term_lval lv in
let offset = Visitor.visitFramacTermOffset self offset in
Cil.ChangeToPost
(Logic_const.addTermOffsetLval offset tlv, Extlib.id)
diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index e869e3dd345..554af1f3639 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -449,7 +449,7 @@ module Computer(I: Init) = struct
"too few arguments in call to %a" Printer.pp_varinfo f
| p::prms, a::args ->
let lv = Logic_const.tvar (Cil.cvar_to_lvar p) in
- let la = Logic_utils.expr_to_term ~cast:false a in
+ let la = Logic_utils.expr_to_term a in
let value =
Cil_datatype.Term.Map.add
la (Fixed 0) Cil_datatype.Term.Map.empty
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index ff3c2f3a3fe..c4fb25191c1 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -138,7 +138,7 @@ let isCrossableAtInit tr func =
let rec aux t =
match t.term_node with
| TConst (LEnum ei) ->
- aux (Logic_utils.expr_to_term ~cast:false ei.eival)
+ aux (Logic_utils.expr_to_term ei.eival)
| TLval lv ->
(match aux_lv lv with
| Some t -> t
@@ -241,7 +241,7 @@ let isCrossableAtInit tr func =
and aux_init off initinfo =
match off, initinfo with
| TNoOffset, SingleInit e ->
- Some (aux (Logic_utils.expr_to_term ~cast:false e))
+ Some (aux (Logic_utils.expr_to_term e))
| TIndex(t,oth), CompoundInit (ct,initl) ->
(match (aux t).term_node with
| TConst(Integer(i1,_)) ->
@@ -653,7 +653,7 @@ let one_term () = Cil.lconstant Integer.one
(** Returns a term representing the variable associated to the given varinfo *)
let mk_term_from_vi vi =
Logic_const.term
- (TLval((Logic_utils.lval_to_term_lval ~cast:true (Cil.var vi))))
+ (TLval((Logic_utils.lval_to_term_lval (Cil.var vi))))
(Ctype Cil.intType)
(** Given an lval term 'host' and an integer value 'off', it returns a lval term host[off]. *)
@@ -681,8 +681,7 @@ let mk_offseted_array_states_as_enum host off =
(Ctype Cil.intType)
(** Returns a lval term associated to the curState generated variable. *)
-let host_state_term() =
- lval_to_term_lval ~cast:true (state_lval())
+let host_state_term() = lval_to_term_lval (state_lval())
(*
(** Returns a lval term associated to the curStateOld generated variable. *)
let host_stateOld_term () =
diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
index 660db8c83c0..744917afbad 100644
--- a/src/plugins/instantiate/basic_blocks.ml
+++ b/src/plugins/instantiate/basic_blocks.ml
@@ -131,7 +131,7 @@ let rec tunref_range ?loc ptr len =
and tunref_range_unfold ?loc lval typ =
match typ with
| Ctype(TArray(typ, Some e, _, _)) ->
- let len = Logic_utils.expr_to_term ~cast:false e in
+ let len = Logic_utils.expr_to_term ~coerce:true e in
let last = tminus ?loc len (tinteger ?loc 1) in
let range = trange ?loc (Some (tinteger ?loc 0), Some last) in
let lval = addTermOffsetLval (TIndex(range, TNoOffset)) lval in
@@ -218,7 +218,7 @@ and pall_elems_eq ?loc depth t1 t2 len =
and peq_unfold ?loc depth t1 t2 =
match Logic_utils.unroll_type t1.term_type with
| Ctype(TArray(_, Some len, _, _)) ->
- let len = Logic_utils.expr_to_term ~cast:false len in
+ let len = Logic_utils.expr_to_term ~coerce:true len in
pall_elems_eq ?loc depth t1 t2 len
| _ -> prel ?loc (Req, t1, t2)
@@ -236,7 +236,7 @@ and punfold_pred ?loc ?(dyn_len = None) depth t1 pred =
| Ctype(TArray(_, opt_len, _, _)) ->
let len =
match opt_len, dyn_len with
- | Some len, None -> Logic_utils.expr_to_term ~cast:false len
+ | Some len, None -> Logic_utils.expr_to_term ~coerce:true len
| _ , Some len -> len
| None, None ->
Options.fatal "Unfolding array: cannot find a length"
diff --git a/src/plugins/occurrence/register_gui.ml b/src/plugins/occurrence/register_gui.ml
index aafb865f349..d7b8da68dfc 100644
--- a/src/plugins/occurrence/register_gui.ml
+++ b/src/plugins/occurrence/register_gui.ml
@@ -127,7 +127,7 @@ let occurrence_highlighter buffer loc ~start ~stop =
| PTermLval (_,ki,_,term_lval) ->
let same_tlval (_kf, k, l) =
Logic_utils.is_same_tlval
- (Logic_utils.lval_to_term_lval ~cast:true l)
+ (Logic_utils.lval_to_term_lval l)
term_lval
&& Kinstr.equal k ki
in
diff --git a/src/plugins/studia/studia_gui.ml b/src/plugins/studia/studia_gui.ml
index a235a6f490b..65638eed878 100644
--- a/src/plugins/studia/studia_gui.ml
+++ b/src/plugins/studia/studia_gui.ml
@@ -54,7 +54,7 @@ let get_lval_opt main_ui kf localizable =
match localizable with
| Pretty_source.PLval (Some _kf, (Kstmt _stmt), lv) ->
let lv_txt = Pretty_utils.to_string Printer.pp_lval lv in
- let tlv = Logic_utils.lval_to_term_lval ~cast:false lv in
+ let tlv = Logic_utils.lval_to_term_lval lv in
Some (lv_txt, tlv)
| Pretty_source.PTermLval (Some _kf, (Kstmt _stmt), _, tlv) ->
let tlv_txt = Pretty_utils.to_string Printer.pp_term_lval tlv in
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 1761500f38f..72492be5df5 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -1080,10 +1080,12 @@ let rec stmts_of_cfg cfg current var_map locals return_exp acc =
| Assume (_, exp,b) ->
let exp = subst_in_exp var_map exp in
- let predicate = (Logic_utils.expr_to_predicate ~cast:true exp).Cil_types.ip_content in
+ let predicate = Logic_utils.expr_to_predicate exp in
let predicate = if b then predicate else Logic_const.pnot predicate in
- let code_annot = Logic_const.new_code_annotation(Cil_types.AAssert([],Assert,predicate)) in
- let stmt = Cil.mkStmtOneInstr ~valid_sid (Cil_types.Code_annot(code_annot,dummy_loc)) in
+ let code_node = Cil_types.AAssert([],Assert,predicate) in
+ let code_annot = Logic_const.new_code_annotation code_node in
+ let stmt_kind = Cil_types.Code_annot(code_annot,exp.eloc) in
+ let stmt = Cil.mkStmtOneInstr ~valid_sid stmt_kind in
stmts_of_cfg cfg n var_map locals return_exp (stmt::acc)
| EnterScope (_, vs) ->
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 2a90684fe56..b15809c85bb 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -1027,7 +1027,7 @@ struct
(* -------------------------------------------------------------------------- *)
let assigned_of_lval env ~unfold (lv : Cil_types.lval) =
- assignable_lval env ~unfold (Logic_utils.lval_to_term_lval ~cast:false lv)
+ assignable_lval env ~unfold (Logic_utils.lval_to_term_lval lv)
let assigned_of_froms env ~unfold froms =
List.concat
diff --git a/tests/spec/expr_to_term.ml b/tests/spec/expr_to_term.ml
index 17478ac46f1..e6fb35a7376 100644
--- a/tests/spec/expr_to_term.ml
+++ b/tests/spec/expr_to_term.ml
@@ -14,7 +14,7 @@ let check_expr_term check fct s e =
| (_, { ip_content = { pred_content = Papp(_,_,[l;_]) } }) -> l
| _ -> Kernel.fatal "Unexpected ensures %a" Printer.pp_post_cond e
in
- let term' = Logic_utils.expr_to_term ~cast:false exp in
+ let term' = Logic_utils.expr_to_term ~coerce:true exp in
let term' = Logic_utils.mk_cast Cil.intType term' in
if check && not (Cil_datatype.Term.equal term term') then
Kernel.fatal
@@ -29,7 +29,7 @@ let treat_fct check fct =
let stmts = (Kernel_function.get_definition fct).sbody.bstmts in
let stmts =
List.filter
- (function
+ (function
{ skind = Instr (Set (lv,_,_)) } ->
(match lv with (Var v,_) -> v.vglob | _ -> true)
| { skind = If _ } -> true
@@ -41,7 +41,7 @@ let treat_fct check fct =
(* A bit fragile, but should do the trick as long as the test itself does
not get too complicated (regarding the C code at least). *)
if not (List.length stmts = List.length ensures) then
- Kernel.fatal
+ Kernel.fatal
"Stmts:@\n%a@\nPreds:@\n%a@\n"
(Pretty_utils.pp_list ~sep:"@\n@\n" Printer.pp_stmt) stmts
(Pretty_utils.pp_list ~sep:"@\n@\n" Printer.pp_post_cond) ensures;
--
GitLab