Commit fd59f66e authored by Fonenantsoa Maurica 's avatar Fonenantsoa Maurica
Browse files

Support for let binding.

parent b4567b26
......@@ -190,8 +190,12 @@ let rec infer t =
| Tinter _ -> Error.not_yet "tset intersection"
| Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
| Trange (_,_) -> Error.not_yet "trange"
| Tlet (_,_) -> Error.not_yet "let binding"
| Tlet (li,t) ->
let li_t = Misc.term_of_li li in
let i = infer li_t in
Env.add li.l_var_info i;
infer t
| TConst (LStr _ | LWStr _ | LReal _)
| TBinOp (PlusPI,_,_)
| TBinOp (IndexPI,_,_)
......
......@@ -246,6 +246,10 @@ let rec ptr_index ?(loc=Location.unknown) ?(index=(Cil.zero loc)) exp =
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
-> assert false
let term_of_li li = match li.l_body with
| LBterm t -> t
| LBnone | LBreads _ | LBpred _ | LBinductive _ ->
Options.fatal "li.l_body does not match LBterm(t) in Misc.term_of_li"
(*
Local Variables:
compile-command: "make"
......
......@@ -100,6 +100,10 @@ val ptr_index: ?loc:location -> ?index:exp -> exp
(** Split pointer-arithmetic expression of the type `p + i` into its
pointer and integer parts. *)
val term_of_li: logic_info -> term
(* [term_of_li li] assumes that [li.l_body] matches [LBterm t]
and returns [t]. *)
(*
Local Variables:
compile-command: "make"
......
......@@ -193,6 +193,13 @@ module rec Transfer
let ty = Cil.typeOf e in
is_ptr_or_array ty
let may_alias li = match li.l_var_info.lv_type with
| Ctype ty -> is_ptr_or_array ty
| Linteger | Lreal -> false
| Ltype _ -> Error.not_yet "user defined type"
| Lvar _ -> Error.not_yet "named type"
| Larrow _ -> Error.not_yet "functional type"
let rec base_addr_node = function
| Lval lv | AddrOf lv | StartOf lv ->
(match lv with
......@@ -276,8 +283,14 @@ module rec Transfer
and register_term kf varinfos term = match term.term_node with
| TLval tlv | TAddrOf tlv | TStartOf tlv ->
register_term_lval kf varinfos tlv
| TCastE(_, t) | Tat(t, _) | Tlet(_, t) ->
| TCastE(_, t) | Tat(t, _) ->
register_term kf varinfos t
| Tlet(li, t) ->
if may_alias li then Error.not_yet "let-binding on array or pointer"
else begin
let varinfos = register_term kf varinfos t in
register_body kf varinfos li.l_body
end
| Tif(_, t1, t2) ->
let varinfos = register_term kf varinfos t1 in
register_term kf varinfos t2
......@@ -308,6 +321,12 @@ module rec Transfer
| Tcomprehension _ -> Error.not_yet "set comprehension"
| Trange _ -> Error.not_yet "\\range"
and register_body kf varinfos = function
| LBnone | LBreads _ -> varinfos
| LBterm t -> register_term kf varinfos t
| LBpred _ -> Options.fatal "unexpected predicate"
| LBinductive _ -> Error.not_yet "inductive definitions"
let register_object kf state_ref = object
inherit Visitor.frama_c_inplace
method !vpredicate_node = function
......@@ -322,10 +341,16 @@ module rec Transfer
| Pdangling _ -> Error.not_yet "\\dangling"
| Ptrue | Pfalse | Papp _ | Prel _
| Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _
| Plet _ | Pforall _ | Pexists _ | Pat _ | Psubtype _ ->
| Pforall _ | Pexists _ | Pat _ | Psubtype _ ->
Cil.DoChildren
| Plet(li, _) ->
if may_alias li then Error.not_yet "let-binding on array or pointer"
else begin
state_ref := register_term kf !state_ref (Misc.term_of_li li);
Cil.DoChildren
end
method !vterm term = match term.term_node with
| Tbase_addr(_, t) | Toffset(_, t) | Tblock_length(_, t) ->
| Tbase_addr(_, t) | Toffset(_, t) | Tblock_length(_, t) | Tlet(_, t) ->
state_ref := register_term kf !state_ref t;
Cil.DoChildren
| TConst _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _ | Tnull | Ttype _
......@@ -336,7 +361,7 @@ module rec Transfer
| TLval _ | TAlignOfE _ | TCastE _ | TAddrOf _
| TStartOf _ | Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _
| TCoerce _ | TCoerceE _ | TUpdate _ | Tunion _ | Tinter _
| Tcomprehension _ | Trange _ | Tlet _ | TLogic_coerce _ ->
| Tcomprehension _ | Trange _ | TLogic_coerce _ ->
(* potential sub-term inside *)
Cil.DoChildren
method !vlogic_label _ = Cil.SkipChildren
......
......@@ -498,7 +498,10 @@ and context_insensitive_term_to_exp kf env t =
| Tinter _ -> not_yet env "intersection of tsets"
| Tcomprehension _ -> not_yet env "tset comprehension"
| Trange _ -> not_yet env "range"
| Tlet _ -> not_yet env "let binding"
| Tlet(li, t) ->
let env = env_of_li li kf env loc in
let e, env = term_to_exp kf env t in
e, env, false, ""
(* Convert an ACSL term into a corresponding C expression (if any) in the given
environment. Also extend this environment in order to include the generating
......@@ -663,6 +666,19 @@ and at_to_exp env t_opt label e =
Cil.set_stmt bhv stmt new_stmt;
res, !env_ref, false
and env_of_li li kf env loc =
let li_t = Misc.term_of_li li in
let ty = Typing.get_typ li_t in
let vi, vi_e, env = Env.Logic_binding.add ~ty env li.l_var_info in
let li_e, env = term_to_exp kf env li_t in
let stmt = match Typing.get_integer_ty li_t with
| Typing.C_type _ | Typing.Other ->
Cil.mkStmtOneInstr (Set (Cil.var vi, li_e, loc))
| Typing.Gmp ->
Gmpz.init_set ~loc (Cil.var vi) vi_e li_e
in
Env.add_stmt env stmt
(* Convert an ACSL named predicate into a corresponding C expression (if
any) in the given environment. Also extend this environment which includes
the generating constructs. *)
......@@ -717,7 +733,9 @@ and named_predicate_content_to_exp ?name kf env p =
let (_, env2 as res2) = named_predicate_to_exp kf (Env.push env1) p2 in
let res3 = named_predicate_to_exp kf (Env.push env2) p3 in
conditional_to_exp loc None e1 res2 res3
| Plet _ -> not_yet env "let _ = _ in _"
| Plet(li, p) ->
let env = env_of_li li kf env loc in
named_predicate_to_exp kf env p
| Pforall _ | Pexists _ -> Quantif.quantif_to_exp kf env p
| Pat(p, BuiltinLabel Here) ->
named_predicate_to_exp kf env p
......
......@@ -231,6 +231,15 @@ 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
let infer_if_integer li =
let li_t = Misc.term_of_li li in
match ty_of_logic_ty li_t.term_type with
| C_type _ | Gmp ->
let i = Interval.infer li_t in
Interval.Env.add li.l_var_info i
| Other ->
()
(* type the term [t] in a context [ctx] by taking --e-acsl-gmp-only into account
iff [use_gmp_opt] is true. *)
let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
......@@ -464,7 +473,11 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| Tinter _ -> Error.not_yet "tset intersection"
| Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
| Trange (_,_) -> Error.not_yet "trange"
| Tlet (_,_) -> Error.not_yet "let binding"
| Tlet(li, t) ->
infer_if_integer li;
let li_t = Misc.term_of_li li in
ignore (type_term ~use_gmp_opt:true li_t);
dup (type_term ~use_gmp_opt:true t).ty
| Tlambda (_,_) -> Error.not_yet "lambda"
| TDataCons (_,_) -> Error.not_yet "datacons"
| TUpdate (_,_,_) -> Error.not_yet "update"
......@@ -541,7 +554,11 @@ let rec type_predicate p =
ignore (type_predicate p1);
ignore (type_predicate p2);
c_int
| Plet _ -> Error.not_yet "let _ = _ in _"
| Plet(li, p) ->
infer_if_integer li;
let li_t = Misc.term_of_li li in
ignore (type_term ~use_gmp_opt:true li_t);
(type_predicate p).ty
| Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) })
| Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
......@@ -641,13 +658,12 @@ let extract_typ t ty =
try typ_of_integer_ty ty
with Not_an_integer ->
let lty = t.term_type in
if Cil.isLogicRealType lty then TFloat(FLongDouble, [])
else if Cil.isLogicFloatType lty then Logic_utils.logicCType lty
else
Kernel.fatal "unexpected types %a and %a for term %a"
Printer.pp_logic_type lty
pretty ty
Printer.pp_term t
match lty with
| Ctype _ -> Logic_utils.logicCType lty
| Ltype _ | Lvar _ | Linteger | Lreal | Larrow _ ->
if Cil.isLogicRealType lty then TFloat(FLongDouble, [])
else if Cil.isLogicFloatType lty then Logic_utils.logicCType lty
else Error.not_yet "unsupported logic type"
let get_typ t =
let info = Memo.get t in
......
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