Skip to content
Snippets Groups Projects
Commit 2e10b36d authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

[Kernel] Split logic_interp into three independent modules

parent 9128695e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 527 additions and 405 deletions
src/kernel_services/analysis/logic_interp.ml
+ 1
− 380
View file @ 2e10b36d
...@@ -24,365 +24,7 @@ open Cil ...@@ -24,365 +24,7 @@ open Cil
open Cil_types open Cil_types
open Cil_datatype open Cil_datatype
exception Error of Cil_types.location * string exception Error = Logic_parse_string.Error
exception Unbound of string
let find_var kf kinstr ?label var =
let vi =
try
let vi = Globals.Vars.find_from_astinfo var (VLocal kf) in
(match kinstr with
| Kglobal -> vi (* don't refine search: the Kglobal here
does not indicate the function contract, but merely
the fact that we do not have any information about
the targeted program point. Hence, no scope check
can be performed or we might reject many legitimate
terms and predicates.
*)
| Kstmt stmt ->
let scope =
match label with
| None | Some "Here" | Some "Post" | Some "Old" -> stmt
| Some "Pre" -> raise Not_found (* no local variable in scope. *)
| Some "Init" -> raise Not_found (* no local variable in scope. *)
| Some "LoopEntry" | Some "LoopCurrent" ->
if not (Kernel_function.stmt_in_loop kf stmt) then
Kernel.fatal
"Use of LoopEntry or LoopCurrent outside of a loop";
Kernel_function.find_enclosing_loop kf stmt
| Some l ->
(try let s = Kernel_function.find_label kf l in !s
with Not_found ->
Kernel.fatal
"Use of label %s that does not exist in function %a"
l Kernel_function.pretty kf)
in
if Kernel_function.var_is_in_scope scope vi then vi
else raise Not_found)
with Not_found ->
try
Globals.Vars.find_from_astinfo var (VFormal kf)
with Not_found ->
Globals.Vars.find_from_astinfo var VGlobal
in
cvar_to_lvar vi
(** Create a logic typer, the interpretation being done for the given
kernel_function and stmt (the stmt is used check that loop invariants
are allowed). *)
(* It is theoretically possible to use a first-class module instead, but the
required signatures are not exported in Logic_typing. *)
module DefaultLT (X:
sig
val kf: Kernel_function.t
val kinstr: Cil_types.kinstr
end) =
Logic_typing.Make
(struct
let anonCompFieldName = Cabs2cil.anonCompFieldName
let conditionalConversion = Cabs2cil.logicConditionalConversion
let is_loop () =
match X.kinstr with
| Kglobal -> false
| Kstmt s -> Kernel_function.stmt_in_loop X.kf s
let find_macro _ = raise Not_found
let find_var ?label var = find_var X.kf X.kinstr ?label var
let find_enum_tag x =
try
Globals.Types.find_enum_tag x
with Not_found ->
(* The ACSL typer tries to parse a string, first as a variable,
then as an enum. We report the "Unbound variable" message
here, as it is nicer for the user. However, this short-circuits
the later stages of resolution, for example global logic
variables. *)
raise (Unbound ("Unbound variable " ^ x))
let find_comp_field info s =
let field = Cil.getCompField info s in
Field(field,NoOffset)
let find_type = Globals.Types.find_type
let find_label s = Kernel_function.find_label X.kf s
include Logic_env
let add_logic_function =
add_logic_function_gen Logic_utils.is_same_logic_profile
let remove_logic_info =
remove_logic_info_gen Logic_utils.is_same_logic_profile
let integral_cast ty t =
raise
(Failure
(Format.asprintf
"term %a has type %a, but %a is expected."
Printer.pp_term t
Printer.pp_logic_type Linteger
Printer.pp_typ ty))
let error loc msg =
Pretty_utils.ksfprintf (fun e -> raise (Error (loc, e))) msg
let on_error f rollback x =
try f x with Error (loc,msg) as exn -> rollback (loc,msg); raise exn
end)
(** Set up the parser for the infamous 'C hack' needed to parse typedefs *)
let sync_typedefs () =
Logic_env.reset_typenames ();
Globals.Types.iter_types
(fun name _ ns ->
if ns = Logic_typing.Typedef then Logic_env.add_typename name)
let wrap f parsetree loc =
match parsetree with
| None -> raise (Error (loc, "Syntax error in annotation"))
| Some annot -> try f annot with Unbound s -> raise (Error (loc, s))
let code_annot kf stmt s =
sync_typedefs ();
let module LT = DefaultLT(struct
let kf = kf
let kinstr = Kstmt stmt
end) in
let loc = Stmt.loc stmt in
let pa =
Option.bind
(Logic_lexer.annot (fst loc,s))
(function (_, Logic_ptree.Acode_annot (_,a)) -> Some a | _ -> None)
in
let parse pa =
LT.code_annot
(Stmt.loc stmt)
(Logic_utils.get_behavior_names (Annotations.funspec kf))
(Ctype (Kernel_function.get_return_type kf)) pa
in
wrap parse pa loc
let default_term_env () =
Logic_typing.append_here_label (Logic_typing.Lenv.empty())
let term kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
sync_typedefs ();
let module LT = DefaultLT(struct
let kf = kf
let kinstr = Kglobal
end) in
let pa_expr = Option.map snd (Logic_lexer.lexpr (fst loc, s)) in
let parse pa_expr = LT.term env pa_expr in
wrap parse pa_expr loc
let term_lval kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
match (term kf ~loc ~env s).term_node with
| TLval lv -> lv
| _ -> raise (Error (loc, "Syntax error (expecting an lvalue)"))
let predicate kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
sync_typedefs ();
let module LT = DefaultLT(struct
let kf = kf
let kinstr = Kglobal
end) in
let pa_expr = Option.map snd (Logic_lexer.lexpr (fst loc, s)) in
let parse pa_expr = LT.predicate env pa_expr in
wrap parse pa_expr loc
let error_lval () = raise Db.Properties.Interp.No_conversion
let rec logic_type_to_typ = function
| Ctype typ -> typ
| Linteger -> TInt(ILongLong,[]) (*TODO: to have an unlimited integer type
in the logic interpretation*)
| Lreal -> TFloat(FDouble,[]) (* TODO: handle reals, not floats... *)
| Ltype({lt_name = name},[]) when name = Utf8_logic.boolean ->
TInt(ILongLong,[])
| Ltype({lt_name = "set"},[t]) -> logic_type_to_typ t
| Ltype _ | Lvar _ | Larrow _ -> error_lval ()
(* Expect conversion to be possible on all sub-terms, otherwise raise an error. *)
let logic_var_to_var { lv_origin = lv } =
match lv with
| None -> error_lval ()
| Some lv -> lv
let create_const_list loc kind low high =
let rec aux acc i =
if Integer.lt i low then acc
else
aux (new_exp ~loc (Const (CInt64 (i,kind,None)))::acc) (Integer.pred i)
in aux [] high
let range low high =
let loc = fst low.eloc, snd high.eloc in
match (Cil.constFold true low).enode, (Cil.constFold true high).enode with
Const(CInt64(low,kind,_)), Const(CInt64(high,_,_)) ->
create_const_list loc kind low high
| _ -> error_lval()
let singleton f loc =
match f loc with
[ l ] -> l
| _ -> error_lval()
let rec loc_lval_to_lval ~result (lh, lo) =
Extlib.product
(fun x y -> (x,y))
(loc_lhost_to_lhost ~result lh)
(loc_offset_to_offset ~result lo)
and loc_lhost_to_lhost ~result = function
| TVar lvar -> [Var (logic_var_to_var lvar)]
| TMem lterm -> List.map (fun x -> Mem x) (loc_to_exp ~result lterm)
| TResult _ ->
( match result with
None -> error_lval()
| Some v -> [Var v])
and loc_offset_to_offset ~result = function
| TNoOffset -> [NoOffset]
| TModel _ -> error_lval ()
| TField (fi, lo) ->
List.map (fun x -> Field (fi,x)) (loc_offset_to_offset ~result lo)
| TIndex (lexp, lo) ->
Extlib.product
(fun x y -> Index(x,y))
(loc_to_exp ~result lexp)
(loc_offset_to_offset ~result lo)
and loc_to_exp ~result {term_node = lnode ; term_type = ltype; term_loc = loc} =
match lnode with
| TLval lv ->
List.map (fun x -> new_exp ~loc (Lval x)) (loc_lval_to_lval ~result lv)
| TAddrOf lv ->
List.map (fun x -> new_exp ~loc (AddrOf x)) (loc_lval_to_lval ~result lv)
| TStartOf lv ->
List.map (fun x -> new_exp ~loc (StartOf x)) (loc_lval_to_lval ~result lv)
| TSizeOfE lexp ->
List.map (fun x -> new_exp ~loc (SizeOfE x)) (loc_to_exp ~result lexp)
| TAlignOfE lexp ->
List.map (fun x -> new_exp ~loc (AlignOfE x)) (loc_to_exp ~result lexp)
| TUnOp (unop, lexp) ->
List.map
(fun x -> new_exp ~loc (UnOp (unop, x, logic_type_to_typ ltype)))
(loc_to_exp ~result lexp)
| TBinOp (binop, lexp1, lexp2) ->
Extlib.product
(fun x y -> new_exp ~loc (BinOp (binop, x,y, logic_type_to_typ ltype)))
(loc_to_exp ~result lexp1)
(loc_to_exp ~result lexp2)
| TSizeOfStr string -> [new_exp ~loc (SizeOfStr string)]
| TConst constant ->
(* TODO: Very likely to fail on large integer and incorrect on reals not
representable as floats *)
[new_exp ~loc (Const (Logic_utils.lconstant_to_constant constant))]
| TCastE (typ, lexp) ->
List.map
(fun x -> new_exp ~loc (CastE (typ, x))) (loc_to_exp ~result lexp)
| TAlignOf typ -> [new_exp ~loc (AlignOf typ)]
| TSizeOf typ -> [new_exp ~loc (SizeOf typ)]
| Trange (Some low, Some high) ->
let low = singleton (loc_to_exp ~result) low in
let high = singleton (loc_to_exp ~result) high in
range low high
| Tunion l -> List.concat (List.map (loc_to_exp ~result) l)
| Tempty_set -> []
| Tinter _ | Tcomprehension _ -> error_lval()
| Tat ({term_node = TAddrOf (TVar _, TNoOffset)} as taddroflval, _) ->
loc_to_exp ~result taddroflval
| TLogic_coerce(Linteger, t) when Logic_typing.is_integral_type t.term_type ->
loc_to_exp ~result t
| TLogic_coerce(Lreal, t) when Logic_typing.is_integral_type t.term_type ->
List.map
(fun x -> new_exp ~loc (CastE (logic_type_to_typ Lreal, x)))
(loc_to_exp ~result t)
| TLogic_coerce(Lreal, t) when Logic_typing.is_arithmetic_type t.term_type ->
loc_to_exp ~result t
| TLogic_coerce (set, t)
when
Logic_const.is_set_type set &&
Logic_utils.is_same_type
(Logic_typing.type_of_set_elem set) t.term_type ->
loc_to_exp ~result t
| Tnull -> [ Cil.mkCast ~newt:(TPtr(TVoid [], [])) (Cil.zero ~loc) ]
(* additional constructs *)
| Tapp _ | Tlambda _ | Trange _ | Tlet _
| TDataCons _
| Tif _
| Tat _
| Tbase_addr _
| Toffset _
| Tblock_length _
| TUpdate _ | Ttypeof _ | Ttype _
| TLogic_coerce _
-> error_lval ()
let rec loc_to_lval ~result t =
match t.term_node with
| TLval lv -> loc_lval_to_lval ~result lv
| TAddrOf lv -> loc_lval_to_lval ~result lv
| TStartOf lv -> loc_lval_to_lval ~result lv
| Tunion l1 -> List.concat (List.map (loc_to_lval ~result) l1)
| Tempty_set -> []
(* coercions to arithmetic types cannot be lval. We only have to consider
a coercion to set here.
*)
| TLogic_coerce(set, t) when
Logic_typing.is_set_type set &&
Logic_utils.is_same_type
(Logic_typing.type_of_set_elem set) t.term_type ->
loc_to_lval ~result t
| Tinter _ -> error_lval() (* TODO *)
| Tcomprehension _ -> error_lval()
| TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TSizeOfStr _
| TConst _ | TCastE _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
| Tat _ | Toffset _ | Tbase_addr _ | Tblock_length _ | Tnull | Trange _
| TDataCons _ | TUpdate _ | Tlambda _
| Ttypeof _ | Ttype _ | Tlet _ | TLogic_coerce _ ->
error_lval ()
let loc_to_offset ~result loc =
let rec aux h =
function
TLval(h',o) | TStartOf (h',o) ->
(match h with None -> Some h', loc_offset_to_offset ~result o
| Some h when Logic_utils.is_same_lhost h h' ->
Some h, loc_offset_to_offset ~result o
| Some _ -> error_lval()
)
| Tat ({ term_node = TLval(TResult _,_)} as lv, BuiltinLabel Post) ->
aux h lv.term_node
| Tunion locs -> List.fold_left
(fun (b,l) x ->
let (b,l') = aux b x.term_node in b, l @ l') (h,[]) locs
| Tempty_set -> h,[]
| Trange _ | TAddrOf _ | Tat _
| TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TSizeOfStr _
| TConst _ | TCastE _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
| Toffset _ | Tbase_addr _ | Tblock_length _ | Tnull
| TDataCons _ | TUpdate _ | Tlambda _
| Ttypeof _ | Ttype _ | Tcomprehension _ | Tinter _ | Tlet _
| TLogic_coerce _
-> error_lval ()
in snd (aux None loc.term_node)
let term_lval_to_lval ~result = singleton (loc_lval_to_lval ~result)
let term_to_lval ~result = singleton (loc_to_lval ~result)
let term_to_exp ~result = singleton (loc_to_exp ~result)
let term_offset_to_offset ~result = singleton (loc_offset_to_offset ~result)
(** Utilities to identify [Locations.Zone.t] involved into (** Utilities to identify [Locations.Zone.t] involved into
...@@ -1071,21 +713,6 @@ let to_result_from_pred p = ...@@ -1071,21 +713,6 @@ let to_result_from_pred p =
let () = let () =
Db.Properties.Interp.code_annot := code_annot;
Db.Properties.Interp.term_lval := term_lval;
Db.Properties.Interp.term := term;
Db.Properties.Interp.predicate := predicate;
Db.Properties.Interp.term_lval_to_lval := term_lval_to_lval;
Db.Properties.Interp.term_to_exp := term_to_exp;
Db.Properties.Interp.term_to_lval := term_to_lval;
Db.Properties.Interp.term_offset_to_offset := term_offset_to_offset;
Db.Properties.Interp.loc_to_lval := loc_to_lval;
Db.Properties.Interp.loc_to_offset := loc_to_offset;
Db.Properties.Interp.loc_to_exp := loc_to_exp;
Db.Properties.Interp.To_zone.code_annot_filter := To_zone.code_annot_filter; Db.Properties.Interp.To_zone.code_annot_filter := To_zone.code_annot_filter;
Db.Properties.Interp.To_zone.mk_ctx_func_contrat := Db.Properties.Interp.To_zone.mk_ctx_func_contrat :=
To_zone.mk_ctx_func_contrat; To_zone.mk_ctx_func_contrat;
...@@ -1102,9 +729,3 @@ let () = ...@@ -1102,9 +729,3 @@ let () =
Db.Properties.Interp.To_zone.from_func_annots := To_zone.from_func_annots; Db.Properties.Interp.To_zone.from_func_annots := To_zone.from_func_annots;
Db.Properties.Interp.to_result_from_pred := to_result_from_pred; Db.Properties.Interp.to_result_from_pred := to_result_from_pred;
(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)
src/kernel_services/analysis/logic_interp.mli
+ 0
− 12
View file @ 2e10b36d
...@@ -20,12 +20,6 @@ ...@@ -20,12 +20,6 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
(** All the interesting functions of this module are exported through
{!Db.Interp}. *)
(* TODO: remove the module Properties from Db and export directly the
functions from here. *)
open Cil_types open Cil_types
module To_zone : sig module To_zone : sig
...@@ -35,9 +29,3 @@ module To_zone : sig ...@@ -35,9 +29,3 @@ module To_zone : sig
end end
exception Error of location * string exception Error of location * string
(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)
src/kernel_services/ast_queries/logic_parse_string.ml 0 → 100644
+ 195
− 0
View file @ 2e10b36d
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It 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 Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Cil
open Cil_types
open Cil_datatype
exception Error of Cil_types.location * string
exception Unbound of string
let find_var kf kinstr ?label var =
let vi =
try
let vi = Globals.Vars.find_from_astinfo var (VLocal kf) in
(match kinstr with
| Kglobal -> vi (* don't refine search: the Kglobal here
does not indicate the function contract, but merely
the fact that we do not have any information about
the targeted program point. Hence, no scope check
can be performed or we might reject many legitimate
terms and predicates.
*)
| Kstmt stmt ->
let scope =
match label with
| None | Some "Here" | Some "Post" | Some "Old" -> stmt
| Some "Pre" -> raise Not_found (* no local variable in scope. *)
| Some "Init" -> raise Not_found (* no local variable in scope. *)
| Some "LoopEntry" | Some "LoopCurrent" ->
if not (Kernel_function.stmt_in_loop kf stmt) then
Kernel.fatal
"Use of LoopEntry or LoopCurrent outside of a loop";
Kernel_function.find_enclosing_loop kf stmt
| Some l ->
(try let s = Kernel_function.find_label kf l in !s
with Not_found ->
Kernel.fatal
"Use of label %s that does not exist in function %a"
l Kernel_function.pretty kf)
in
if Kernel_function.var_is_in_scope scope vi then vi
else raise Not_found)
with Not_found ->
try
Globals.Vars.find_from_astinfo var (VFormal kf)
with Not_found ->
Globals.Vars.find_from_astinfo var VGlobal
in
cvar_to_lvar vi
(** Create a logic typer, the interpretation being done for the given
kernel_function and stmt (the stmt is used check that loop invariants
are allowed). *)
(* It is theoretically possible to use a first-class module instead, but the
required signatures are not exported in Logic_typing. *)
module DefaultLT (X:
sig
val kf: Kernel_function.t
val kinstr: Cil_types.kinstr
end) =
Logic_typing.Make
(struct
let anonCompFieldName = Cabs2cil.anonCompFieldName
let conditionalConversion = Cabs2cil.logicConditionalConversion
let is_loop () =
match X.kinstr with
| Kglobal -> false
| Kstmt s -> Kernel_function.stmt_in_loop X.kf s
let find_macro _ = raise Not_found
let find_var ?label var = find_var X.kf X.kinstr ?label var
let find_enum_tag x =
try
Globals.Types.find_enum_tag x
with Not_found ->
(* The ACSL typer tries to parse a string, first as a variable,
then as an enum. We report the "Unbound variable" message
here, as it is nicer for the user. However, this short-circuits
the later stages of resolution, for example global logic
variables. *)
raise (Unbound ("Unbound variable " ^ x))
let find_comp_field info s =
let field = Cil.getCompField info s in
Field(field,NoOffset)
let find_type = Globals.Types.find_type
let find_label s = Kernel_function.find_label X.kf s
include Logic_env
let add_logic_function =
add_logic_function_gen Logic_utils.is_same_logic_profile
let remove_logic_info =
remove_logic_info_gen Logic_utils.is_same_logic_profile
let integral_cast ty t =
raise
(Failure
(Format.asprintf
"term %a has type %a, but %a is expected."
Printer.pp_term t
Printer.pp_logic_type Linteger
Printer.pp_typ ty))
let error loc msg =
Pretty_utils.ksfprintf (fun e -> raise (Error (loc, e))) msg
let on_error f rollback x =
try f x with Error (loc,msg) as exn -> rollback (loc,msg); raise exn
end)
(** Set up the parser for the infamous 'C hack' needed to parse typedefs *)
let sync_typedefs () =
Logic_env.reset_typenames ();
Globals.Types.iter_types
(fun name _ ns ->
if ns = Logic_typing.Typedef then Logic_env.add_typename name)
let wrap f parsetree loc =
match parsetree with
| None -> raise (Error (loc, "Syntax error in annotation"))
| Some annot -> try f annot with Unbound s -> raise (Error (loc, s))
let code_annot kf stmt s =
sync_typedefs ();
let module LT = DefaultLT(struct
let kf = kf
let kinstr = Kstmt stmt
end) in
let loc = Stmt.loc stmt in
let pa =
Option.bind
(Logic_lexer.annot (fst loc,s))
(function (_, Logic_ptree.Acode_annot (_,a)) -> Some a | _ -> None)
in
let parse pa =
LT.code_annot
(Stmt.loc stmt)
(Logic_utils.get_behavior_names (Annotations.funspec kf))
(Ctype (Kernel_function.get_return_type kf)) pa
in
wrap parse pa loc
let default_term_env () =
Logic_typing.append_here_label (Logic_typing.Lenv.empty())
let term kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
sync_typedefs ();
let module LT = DefaultLT(struct
let kf = kf
let kinstr = Kglobal
end) in
let pa_expr = Option.map snd (Logic_lexer.lexpr (fst loc, s)) in
let parse pa_expr = LT.term env pa_expr in
wrap parse pa_expr loc
let term_lval kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
match (term kf ~loc ~env s).term_node with
| TLval lv -> lv
| _ -> raise (Error (loc, "Syntax error (expecting an lvalue)"))
let predicate kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
sync_typedefs ();
let module LT = DefaultLT(struct
let kf = kf
let kinstr = Kglobal
end) in
let pa_expr = Option.map snd (Logic_lexer.lexpr (fst loc, s)) in
let parse pa_expr = LT.predicate env pa_expr in
wrap parse pa_expr loc
src/kernel_services/ast_queries/logic_parse_string.mli 0 → 100644
+ 44
− 0
View file @ 2e10b36d
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It 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 Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Cil_types
exception Error of Cil_types.location * string
exception Unbound of string
(** For the three functions below, [env] can be used to specify which
logic labels are parsed. By default, only [Here] is accepted. All
the C labels inside the function are also accepted, regardless of
[env]. [loc] is used as the source for the beginning of the string.
All three functions may raise {!Logic_interp.Error} or
{!Parsing.Parse_error}. *)
val code_annot : kernel_function -> stmt -> string -> code_annotation
val term_lval :
kernel_function -> ?loc:location -> ?env:Logic_typing.Lenv.t -> string ->
Cil_types.term_lval
val term :
kernel_function -> ?loc:location -> ?env:Logic_typing.Lenv.t -> string ->
Cil_types.term
val predicate :
kernel_function -> ?loc:location -> ?env:Logic_typing.Lenv.t -> string ->
Cil_types.predicate
src/kernel_services/ast_queries/logic_to_c.ml 0 → 100644
+ 215
− 0
View file @ 2e10b36d
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It 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 Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Cil
open Cil_types
exception No_conversion
let error_lval () = raise No_conversion
let rec logic_type_to_typ = function
| Ctype typ -> typ
| Linteger -> TInt(ILongLong,[]) (*TODO: to have an unlimited integer type
in the logic interpretation*)
| Lreal -> TFloat(FDouble,[]) (* TODO: handle reals, not floats... *)
| Ltype({lt_name = name},[]) when name = Utf8_logic.boolean ->
TInt(ILongLong,[])
| Ltype({lt_name = "set"},[t]) -> logic_type_to_typ t
| Ltype _ | Lvar _ | Larrow _ -> error_lval ()
(* Expect conversion to be possible on all sub-terms, otherwise raise an error. *)
let logic_var_to_var { lv_origin = lv } =
match lv with
| None -> error_lval ()
| Some lv -> lv
let create_const_list loc kind low high =
let rec aux acc i =
if Integer.lt i low then acc
else
aux (new_exp ~loc (Const (CInt64 (i,kind,None)))::acc) (Integer.pred i)
in aux [] high
let range low high =
let loc = fst low.eloc, snd high.eloc in
match (Cil.constFold true low).enode, (Cil.constFold true high).enode with
Const(CInt64(low,kind,_)), Const(CInt64(high,_,_)) ->
create_const_list loc kind low high
| _ -> error_lval()
let singleton f loc =
match f loc with
[ l ] -> l
| _ -> error_lval()
let rec loc_lval_to_lval ~result (lh, lo) =
Extlib.product
(fun x y -> (x,y))
(loc_lhost_to_lhost ~result lh)
(loc_offset_to_offset ~result lo)
and loc_lhost_to_lhost ~result = function
| TVar lvar -> [Var (logic_var_to_var lvar)]
| TMem lterm -> List.map (fun x -> Mem x) (loc_to_exp ~result lterm)
| TResult _ ->
( match result with
None -> error_lval()
| Some v -> [Var v])
and loc_offset_to_offset ~result = function
| TNoOffset -> [NoOffset]
| TModel _ -> error_lval ()
| TField (fi, lo) ->
List.map (fun x -> Field (fi,x)) (loc_offset_to_offset ~result lo)
| TIndex (lexp, lo) ->
Extlib.product
(fun x y -> Index(x,y))
(loc_to_exp ~result lexp)
(loc_offset_to_offset ~result lo)
and loc_to_exp ~result {term_node = lnode ; term_type = ltype; term_loc = loc} =
match lnode with
| TLval lv ->
List.map (fun x -> new_exp ~loc (Lval x)) (loc_lval_to_lval ~result lv)
| TAddrOf lv ->
List.map (fun x -> new_exp ~loc (AddrOf x)) (loc_lval_to_lval ~result lv)
| TStartOf lv ->
List.map (fun x -> new_exp ~loc (StartOf x)) (loc_lval_to_lval ~result lv)
| TSizeOfE lexp ->
List.map (fun x -> new_exp ~loc (SizeOfE x)) (loc_to_exp ~result lexp)
| TAlignOfE lexp ->
List.map (fun x -> new_exp ~loc (AlignOfE x)) (loc_to_exp ~result lexp)
| TUnOp (unop, lexp) ->
List.map
(fun x -> new_exp ~loc (UnOp (unop, x, logic_type_to_typ ltype)))
(loc_to_exp ~result lexp)
| TBinOp (binop, lexp1, lexp2) ->
Extlib.product
(fun x y -> new_exp ~loc (BinOp (binop, x,y, logic_type_to_typ ltype)))
(loc_to_exp ~result lexp1)
(loc_to_exp ~result lexp2)
| TSizeOfStr string -> [new_exp ~loc (SizeOfStr string)]
| TConst constant ->
(* TODO: Very likely to fail on large integer and incorrect on reals not
representable as floats *)
[new_exp ~loc (Const (Logic_utils.lconstant_to_constant constant))]
| TCastE (typ, lexp) ->
List.map
(fun x -> new_exp ~loc (CastE (typ, x))) (loc_to_exp ~result lexp)
| TAlignOf typ -> [new_exp ~loc (AlignOf typ)]
| TSizeOf typ -> [new_exp ~loc (SizeOf typ)]
| Trange (Some low, Some high) ->
let low = singleton (loc_to_exp ~result) low in
let high = singleton (loc_to_exp ~result) high in
range low high
| Tunion l -> List.concat (List.map (loc_to_exp ~result) l)
| Tempty_set -> []
| Tinter _ | Tcomprehension _ -> error_lval()
| Tat ({term_node = TAddrOf (TVar _, TNoOffset)} as taddroflval, _) ->
loc_to_exp ~result taddroflval
| TLogic_coerce(Linteger, t) when Logic_typing.is_integral_type t.term_type ->
loc_to_exp ~result t
| TLogic_coerce(Lreal, t) when Logic_typing.is_integral_type t.term_type ->
List.map
(fun x -> new_exp ~loc (CastE (logic_type_to_typ Lreal, x)))
(loc_to_exp ~result t)
| TLogic_coerce(Lreal, t) when Logic_typing.is_arithmetic_type t.term_type ->
loc_to_exp ~result t
| TLogic_coerce (set, t)
when
Logic_const.is_set_type set &&
Logic_utils.is_same_type
(Logic_typing.type_of_set_elem set) t.term_type ->
loc_to_exp ~result t
| Tnull -> [ Cil.mkCast ~newt:(TPtr(TVoid [], [])) (Cil.zero ~loc) ]
(* additional constructs *)
| Tapp _ | Tlambda _ | Trange _ | Tlet _
| TDataCons _
| Tif _
| Tat _
| Tbase_addr _
| Toffset _
| Tblock_length _
| TUpdate _ | Ttypeof _ | Ttype _
| TLogic_coerce _
-> error_lval ()
let rec loc_to_lval ~result t =
match t.term_node with
| TLval lv -> loc_lval_to_lval ~result lv
| TAddrOf lv -> loc_lval_to_lval ~result lv
| TStartOf lv -> loc_lval_to_lval ~result lv
| Tunion l1 -> List.concat (List.map (loc_to_lval ~result) l1)
| Tempty_set -> []
(* coercions to arithmetic types cannot be lval. We only have to consider
a coercion to set here.
*)
| TLogic_coerce(set, t) when
Logic_typing.is_set_type set &&
Logic_utils.is_same_type
(Logic_typing.type_of_set_elem set) t.term_type ->
loc_to_lval ~result t
| Tinter _ -> error_lval() (* TODO *)
| Tcomprehension _ -> error_lval()
| TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TSizeOfStr _
| TConst _ | TCastE _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
| Tat _ | Toffset _ | Tbase_addr _ | Tblock_length _ | Tnull | Trange _
| TDataCons _ | TUpdate _ | Tlambda _
| Ttypeof _ | Ttype _ | Tlet _ | TLogic_coerce _ ->
error_lval ()
let loc_to_offset ~result loc =
let rec aux h =
function
TLval(h',o) | TStartOf (h',o) ->
(match h with None -> Some h', loc_offset_to_offset ~result o
| Some h when Logic_utils.is_same_lhost h h' ->
Some h, loc_offset_to_offset ~result o
| Some _ -> error_lval()
)
| Tat ({ term_node = TLval(TResult _,_)} as lv, BuiltinLabel Post) ->
aux h lv.term_node
| Tunion locs -> List.fold_left
(fun (b,l) x ->
let (b,l') = aux b x.term_node in b, l @ l') (h,[]) locs
| Tempty_set -> h,[]
| Trange _ | TAddrOf _ | Tat _
| TSizeOfE _ | TAlignOfE _ | TUnOp _ | TBinOp _ | TSizeOfStr _
| TConst _ | TCastE _ | TAlignOf _ | TSizeOf _ | Tapp _ | Tif _
| Toffset _ | Tbase_addr _ | Tblock_length _ | Tnull
| TDataCons _ | TUpdate _ | Tlambda _
| Ttypeof _ | Ttype _ | Tcomprehension _ | Tinter _ | Tlet _
| TLogic_coerce _
-> error_lval ()
in snd (aux None loc.term_node)
let term_lval_to_lval ~result = singleton (loc_lval_to_lval ~result)
let term_to_lval ~result = singleton (loc_to_lval ~result)
let term_to_exp ~result = singleton (loc_to_exp ~result)
let term_offset_to_offset ~result = singleton (loc_offset_to_offset ~result)
src/kernel_services/ast_queries/logic_to_c.mli 0 → 100644
+ 59
− 0
View file @ 2e10b36d
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2022 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It 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 Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Cil_types
exception No_conversion
val logic_type_to_typ : logic_type -> typ
val logic_var_to_var : logic_var -> varinfo
val loc_lval_to_lval : result:varinfo option -> term_lval -> lval list
val loc_lhost_to_lhost : result:varinfo option -> term_lhost -> lhost list
val loc_offset_to_offset : result:varinfo option -> term_offset -> offset list
val loc_to_exp : result:varinfo option -> term -> exp list
(** @return a list of C expressions.
@raise No_conversion if the argument is not a valid set of
expressions. *)
val loc_to_lval : result:varinfo option -> term -> lval list
(** @return a list of C locations.
@raise No_conversion if the argument is not a valid set of
left values. *)
val loc_to_offset : result:varinfo option -> term -> offset list
(** @return a list of C offset provided the term denotes locations who
have all the same base address.
@raise No_conversion if the given term does not match the precondition *)
val term_lval_to_lval : result:varinfo option -> term_lval -> lval
(** @raise No_conversion if the argument is not a left value. *)
val term_to_lval : result:varinfo option -> term -> lval
(** @raise No_conversion if the argument is not a left value. *)
val term_to_exp : result:varinfo option -> term -> exp
(** @raise No_conversion if the argument is not a valid expression. *)
val term_offset_to_offset : result:varinfo option -> term_offset -> offset
(** @raise No_conversion if the argument is not a valid offset. *)
src/kernel_services/plugin_entry_points/db.ml
+ 13
− 13
View file @ 2e10b36d
...@@ -694,25 +694,25 @@ module Properties = struct ...@@ -694,25 +694,25 @@ module Properties = struct
module Interp = struct module Interp = struct
exception No_conversion exception No_conversion = Logic_to_c.No_conversion
(** Interpretation and conversions of of formulas *) (** Interpretation and conversions of of formulas *)
let code_annot = mk_fun "Properties.Interp.code_annot" let code_annot = ref Logic_parse_string.code_annot
let term_lval = mk_fun "Properties.Interp.term_lval" let term_lval = ref Logic_parse_string.term_lval
let term = mk_fun "Properties.Interp.term" let term = ref Logic_parse_string.term
let predicate = mk_fun "Properties.Interp.predicate" let predicate = ref Logic_parse_string.predicate
let term_lval_to_lval = mk_resultfun "Properties.Interp.term_lval_to_lval"
let term_to_exp = mk_resultfun "Properties.Interp.term_to_exp" let term_lval_to_lval = ref Logic_to_c.term_lval_to_lval
let term_to_lval = mk_resultfun "Properties.Interp.term_to_lval" let term_to_exp = ref Logic_to_c.term_to_exp
let loc_to_lval = mk_resultfun "Properties.Interp.loc_to_lval" let term_to_lval = ref Logic_to_c.term_to_lval
let loc_to_lval = ref Logic_to_c.loc_to_lval
(* loc_to_loc and loc_to_locs are defined in Value/Eval_logic, not (* loc_to_loc and loc_to_locs are defined in Value/Eval_logic, not
in Logic_interp *) in Logic_interp *)
let loc_to_loc = mk_resultfun "Properties.Interp.loc_to_loc" let loc_to_loc = mk_resultfun "Properties.Interp.loc_to_loc"
let loc_to_loc_under_over = mk_resultfun "Properties.Interp.loc_to_loc_with_deps" let loc_to_loc_under_over = mk_resultfun "Properties.Interp.loc_to_loc_with_deps"
let loc_to_offset = mk_resultfun "Properties.Interp.loc_to_offset" let loc_to_offset = ref Logic_to_c.loc_to_offset
let loc_to_exp = mk_resultfun "Properties.Interp.loc_to_exp" let loc_to_exp = ref Logic_to_c.loc_to_exp
let term_offset_to_offset = let term_offset_to_offset = ref Logic_to_c.term_offset_to_offset
mk_resultfun "Properties.Interp.term_offset_to_offset"
module To_zone : sig module To_zone : sig
(** The signature of the mli is copy pasted here because of (** The signature of the mli is copy pasted here because of
......
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