From 2e10b36d8cce6fff951fc825df23b96f0e38ba4a Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 1 Aug 2022 22:48:26 +0200
Subject: [PATCH] [Kernel] Split logic_interp into three independent modules
---
src/kernel_services/analysis/logic_interp.ml | 381 +-----------------
src/kernel_services/analysis/logic_interp.mli | 12 -
.../ast_queries/logic_parse_string.ml | 195 +++++++++
.../ast_queries/logic_parse_string.mli | 44 ++
src/kernel_services/ast_queries/logic_to_c.ml | 215 ++++++++++
.../ast_queries/logic_to_c.mli | 59 +++
src/kernel_services/plugin_entry_points/db.ml | 26 +-
7 files changed, 527 insertions(+), 405 deletions(-)
create mode 100644 src/kernel_services/ast_queries/logic_parse_string.ml
create mode 100644 src/kernel_services/ast_queries/logic_parse_string.mli
create mode 100644 src/kernel_services/ast_queries/logic_to_c.ml
create mode 100644 src/kernel_services/ast_queries/logic_to_c.mli
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index e76accf2cc9..924a9b2894e 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -24,365 +24,7 @@ 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
-
-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)
-
+exception Error = Logic_parse_string.Error
(** Utilities to identify [Locations.Zone.t] involved into
@@ -1071,21 +713,6 @@ let to_result_from_pred p =
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.mk_ctx_func_contrat :=
To_zone.mk_ctx_func_contrat;
@@ -1102,9 +729,3 @@ let () =
Db.Properties.Interp.To_zone.from_func_annots := To_zone.from_func_annots;
Db.Properties.Interp.to_result_from_pred := to_result_from_pred;
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/analysis/logic_interp.mli b/src/kernel_services/analysis/logic_interp.mli
index 09165c84558..5020269dbe0 100644
--- a/src/kernel_services/analysis/logic_interp.mli
+++ b/src/kernel_services/analysis/logic_interp.mli
@@ -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
module To_zone : sig
@@ -35,9 +29,3 @@ module To_zone : sig
end
exception Error of location * string
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/ast_queries/logic_parse_string.ml b/src/kernel_services/ast_queries/logic_parse_string.ml
new file mode 100644
index 00000000000..1b1308c18a1
--- /dev/null
+++ b/src/kernel_services/ast_queries/logic_parse_string.ml
@@ -0,0 +1,195 @@
+(**************************************************************************)
+(* *)
+(* 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
diff --git a/src/kernel_services/ast_queries/logic_parse_string.mli b/src/kernel_services/ast_queries/logic_parse_string.mli
new file mode 100644
index 00000000000..0083f8bfb0f
--- /dev/null
+++ b/src/kernel_services/ast_queries/logic_parse_string.mli
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(* *)
+(* 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
diff --git a/src/kernel_services/ast_queries/logic_to_c.ml b/src/kernel_services/ast_queries/logic_to_c.ml
new file mode 100644
index 00000000000..bf728a97492
--- /dev/null
+++ b/src/kernel_services/ast_queries/logic_to_c.ml
@@ -0,0 +1,215 @@
+(**************************************************************************)
+(* *)
+(* 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)
diff --git a/src/kernel_services/ast_queries/logic_to_c.mli b/src/kernel_services/ast_queries/logic_to_c.mli
new file mode 100644
index 00000000000..9ceaacced24
--- /dev/null
+++ b/src/kernel_services/ast_queries/logic_to_c.mli
@@ -0,0 +1,59 @@
+(**************************************************************************)
+(* *)
+(* 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. *)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 539411cd3e6..87865669f87 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -694,25 +694,25 @@ module Properties = struct
module Interp = struct
- exception No_conversion
+ exception No_conversion = Logic_to_c.No_conversion
(** Interpretation and conversions of of formulas *)
- let code_annot = mk_fun "Properties.Interp.code_annot"
- let term_lval = mk_fun "Properties.Interp.term_lval"
- let term = mk_fun "Properties.Interp.term"
- let predicate = mk_fun "Properties.Interp.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_to_lval = mk_resultfun "Properties.Interp.term_to_lval"
- let loc_to_lval = mk_resultfun "Properties.Interp.loc_to_lval"
+ let code_annot = ref Logic_parse_string.code_annot
+ let term_lval = ref Logic_parse_string.term_lval
+ let term = ref Logic_parse_string.term
+ let predicate = ref Logic_parse_string.predicate
+
+ let term_lval_to_lval = ref Logic_to_c.term_lval_to_lval
+ let term_to_exp = ref Logic_to_c.term_to_exp
+ 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
in Logic_interp *)
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_offset = mk_resultfun "Properties.Interp.loc_to_offset"
- let loc_to_exp = mk_resultfun "Properties.Interp.loc_to_exp"
- let term_offset_to_offset =
- mk_resultfun "Properties.Interp.term_offset_to_offset"
+ let loc_to_offset = ref Logic_to_c.loc_to_offset
+ let loc_to_exp = ref Logic_to_c.loc_to_exp
+ let term_offset_to_offset = ref Logic_to_c.term_offset_to_offset
module To_zone : sig
(** The signature of the mli is copy pasted here because of
--
GitLab