[archi] add source subdirectories

src/plugins/e-acsl/.gitignore

@@ -86,3 +86,4 @@ lib/libeacsl-rtl-segment.a
 lib/libeacsl-rtl-bittree-dbg.a
 lib/libeacsl-rtl-segment-dbg.a
 tests/csrv14/*
+src/local_config.ml

src/plugins/e-acsl/Makefile.in

@@ -49,43 +49,75 @@ endif
 CAT?=cat
 SED?=sed
 
+###################
+# Plug-in sources #
+###################
+
+# libraries
+SRC_LIBRARIES:= \
+	error \
+	builtins \
+	functions \
+	misc \
+	gmp_types \
+	varname
+SRC_LIBRARIES:=$(addprefix src/libraries/, $(SRC_LIBRARIES))
+
+# analyses
+SRC_ANALYSES:= \
+	rte \
+	literal_strings \
+	mmodel_analysis \
+	exit_points \
+	lscope \
+	interval \
+	typing
+SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
+
+# project initializer
+SRC_PROJECT_INITIALIZER:= \
+	keep_status \
+	prepare_ast \
+	dup_functions
+SRC_PROJECT_INITIALIZER:=\
+  $(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
+
+# code generator
+SRC_CODE_GENERATOR:= \
+	gmp \
+	label \
+	env \
+	real \
+	loops \
+	quantif \
+	at_with_lscope \
+	mmodel_translate \
+	logic_functions \
+	translate \
+	temporal \
+	visit
+SRC_CODE_GENERATOR:=$(addprefix src/code_generator/, $(SRC_CODE_GENERATOR))
+
 #########################
 # Plug-in configuration #
 #########################
 
 PLUGIN_DIR ?=.
-PLUGIN_EXTRA_DIRS:=src
+PLUGIN_EXTRA_DIRS:=\
+	src \
+	src/libraries \
+	src/analyses \
+	src/project_initializer \
+	src/code_generator
 PLUGIN_ENABLE:=@ENABLE_E_ACSL@
 PLUGIN_DYNAMIC:=@DYNAMIC_E_ACSL@
 PLUGIN_NAME:=E_ACSL
 PLUGIN_CMO:= src/local_config \
 	src/options \
-	src/rte \
-	src/error \
-	src/builtins \
-	src/functions \
-	src/misc \
-	src/gmp \
-	src/literal_strings \
-	src/mmodel_analysis \
-	src/exit_points \
-	src/label \
-	src/lscope \
-	src/env \
-	src/real \
-	src/keep_status \
-	src/dup_functions \
-	src/interval \
-	src/typing \
-	src/loops \
-	src/quantif \
-	src/at_with_lscope \
-	src/mmodel_translate \
-	src/logic_functions \
-	src/translate \
-	src/temporal \
-	src/prepare_ast \
-	src/visit \
+	$(SRC_LIBRARIES) \
+	$(SRC_ANALYSES) \
+	$(SRC_PROJECT_INITIALIZER) \
+	$(SRC_CODE_GENERATOR) \
 	src/main
 
 PLUGIN_HAS_MLI:=yes
@@ -95,9 +127,9 @@ PLUGIN_DISTRIBUTED:=yes
 EACSL_PLUGIN_DIR:=$(PLUGIN_DIR)
 
 # Suppress a spurious warning with OCaml >= 4.04.0
-$(EACSL_PLUGIN_DIR)/src/mmodel_analysis.cmo \
-$(EACSL_PLUGIN_DIR)/src/mmodel_analysis.cmi: E_ACSL_BFLAGS+= -w -60
-$(EACSL_PLUGIN_DIR)/src/mmodel_analysis.cmx: E_ACSL_OFLAGS+= -w -60
+$(EACSL_PLUGIN_DIR)/src/analyses/mmodel_analysis.cmo \
+$(EACSL_PLUGIN_DIR)/src/analyses/mmodel_analysis.cmi: E_ACSL_BFLAGS+= -w -60
+$(EACSL_PLUGIN_DIR)/src/analyses/mmodel_analysis.cmx: E_ACSL_OFLAGS+= -w -60
 
 ###############
 # Local Flags #
@@ -173,6 +205,9 @@ E_ACSL_DEFAULT_TESTS: \
 	$(EACSL_PLUGIN_DIR)/tests/print.cmo
 
 clean::
+	for d in $(E_ACSL_EXTRA_DIRS); do \
+	  $(RM) $$d/*~; \
+	done
 	$(PRINT_RM) cleaning generated test files
 	$(RM) $(E_ACSL_DIR)/tests/*.cm* $(E_ACSL_DIR)/tests/*.o
 	$(RM) $(E_ACSL_DIR)/tests/test_config
@@ -295,10 +330,13 @@ PLUGIN_HEADER_EXCEPTIONS:=
 PLUGIN_DISTRIB_TESTS:= $(EACSL_DISTRIB_TESTS)
 
 # for e-csl-distrib target:
-EACSL_OCAML_FILES = E_ACSL.mli src/*.mli \
-  $(patsubst $(EACSL_PLUGIN_DIR)/%, %, \
-    $(filter-out $(wildcard $(EACSL_PLUGIN_DIR)/src/*local_config.ml), \
-		 $(wildcard $(EACSL_PLUGIN_DIR)/src/*.ml)))
+EACSL_OCAML_FILES = \
+	E_ACSL.mli \
+	src/*.mli src/*/*.mli \
+	$(patsubst $(EACSL_PLUGIN_DIR)/%, %, \
+	  $(filter-out $(wildcard $(EACSL_PLUGIN_DIR)/src/*local_config.ml), \
+	  	 $(wildcard $(EACSL_PLUGIN_DIR)/src/*.ml) \
+			$(EACSL_PLUGIN_DIR/src/*/*.ml))
 
 EACSL_DISTRIB_FILES = \
   $(patsubst $(EACSL_PLUGIN_DIR)/%,%,\
@@ -372,8 +410,12 @@ EACSL_SHARE_BARE= share/e-acsl/*.[ch] share/e-acsl/*/*.[ch]
 EACSL_SHARE=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_SHARE_BARE))
 EACSL_CEA_SHARE=$(filter-out $(EACSL_SPARETIMELABS), $(wildcard $(EACSL_SHARE)))
 
-EACSL_CEA_LGPL_BARE= src/*.ml src/*.mli E_ACSL.mli Makefile.in configure.ac \
-  scripts/*.sh tests/print.ml man/e-acsl-gcc.sh.1
+EACSL_CEA_LGPL_BARE= src/*.ml src/*/*.ml src/*.mli src/*/*.mli \
+	E_ACSL.mli \
+	Makefile.in configure.ac \
+	scripts/*.sh \
+	tests/print.ml \
+	man/e-acsl-gcc.sh.1
 EACSL_CEA_LGPL=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_CEA_LGPL_BARE)) \
                $(EACSL_CEA_SHARE)
 

src/plugins/e-acsl/src/interval.ml → src/plugins/e-acsl/src/analyses/interval.ml

@@ -220,11 +220,11 @@ let rec interv_of_typ ty = match Cil.unrollType ty with
     ival l u
   | TEnum(enuminfo, _) ->
     interv_of_typ (TInt(enuminfo.ekind, []))
-  | _ when Gmp.Z.is_t ty ->
+  | _ when Gmp_types.Z.is_t ty ->
     top_ival
   | TFloat (k, _) ->
     Float(k, None)
-  | _ when Real.is_t ty ->
+  | _ when Gmp_types.Q.is_t ty ->
     Rational (* only rationals are implemented *)
   | TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ ->
     Nan
@@ -593,6 +593,6 @@ include D
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
 End:
  *)

src/plugins/e-acsl/src/interval.mli → src/plugins/e-acsl/src/analyses/interval.mli

@@ -104,6 +104,6 @@ val infer: Cil_types.term -> t
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
 End:
 *)

src/plugins/e-acsl/src/typing.ml → src/plugins/e-acsl/src/analyses/typing.ml

@@ -151,15 +151,15 @@ exception Not_a_number
 let typ_of_number_ty = function
   | C_integer ik -> TInt(ik, [])
   | C_float fk -> TFloat(fk, [])
-  | Gmpz -> Gmp.Z.t ()
+  | Gmpz -> Gmp_types.Z.t ()
   (* for the time being, no reals but rationals instead *)
-  | Rational -> Real.t ()
+  | Rational -> Gmp_types.Q.t ()
   | Real -> Error.not_yet "real number type"
   | Nan -> raise Not_a_number
 
 let typ_of_lty = function
   | Ctype cty -> cty
-  | Linteger -> Gmp.Z.t ()
+  | Linteger -> Gmp_types.Z.t ()
   | Lreal -> Error.not_yet "real type"
   | Ltype _ | Lvar _ | Larrow _ -> Options.fatal "unexpected logic type"
 
@@ -755,6 +755,6 @@ module Datatype = D
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
 End:
 *)

src/plugins/e-acsl/src/typing.mli → src/plugins/e-acsl/src/analyses/typing.mli

@@ -160,6 +160,6 @@ val compute_quantif_guards_ref
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
 End:
 *)

src/plugins/e-acsl/src/at_with_lscope.ml → src/plugins/e-acsl/src/code_generator/at_with_lscope.ml

@@ -242,7 +242,7 @@ let to_exp ~loc kf env pot label =
   let vi_at, e_at, env = Env.new_var
     ~loc
     ~name:"at"
-    ~scope:Env.Function
+    ~scope:Varname.Function
     env
     None
     ty_ptr
@@ -341,3 +341,9 @@ let to_exp ~loc kf env pot label =
   let lval_at_index, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
   let e = Cil.new_exp ~loc (Lval lval_at_index) in
   e, env
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)

src/plugins/e-acsl/src/at_with_lscope.mli → src/plugins/e-acsl/src/code_generator/at_with_lscope.mli

@@ -66,4 +66,10 @@ val predicate_to_exp_ref:
   (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
 
 val term_to_exp_ref:
-  (kernel_function -> Env.t -> term -> exp * Env.t) ref
\ No newline at end of file
+  (kernel_function -> Env.t -> term -> exp * Env.t) ref
+
+(*
+Local Variables:
+compile-command: "make -C ../.."
+End:
+*)

src/plugins/e-acsl/src/env.ml → src/plugins/e-acsl/src/code_generator/env.ml

@@ -29,11 +29,6 @@ type localized_scope =
   | LFunction of kernel_function
   | LLocal_block of kernel_function
 
-type scope =
-  | Global
-  | Function
-  | Local_block
-
 type mp_tbl = {
   new_exps: (varinfo * exp) Term.Map.t;
   (* generated mp variables as exp from terms *)
@@ -76,33 +71,6 @@ type t = {
   (* counter used when generating variables *)
 }
 
-module Varname: sig
-  val get: scope:scope -> string -> string
-  val clear: unit -> unit
-end = struct
-
-  module H = Datatype.String.Hashtbl
-  let tbl = H.create 7
-  let globals = H.create 7
-
-  let get ~scope s =
-    let _, u =
-      Extlib.make_unique_name
-        (fun s -> H.mem tbl s || H.mem globals s)
-        ~sep:"_"
-        s
-    in
-    let add = match scope with
-      | Global -> H.add globals
-      | Function | Local_block -> H.add tbl
-    in
-    add u ();
-    u
-
-  let clear () = H.clear tbl
-
-end
-
 let empty_block =
   { new_block_vars = [];
     new_stmts = [];
@@ -195,13 +163,13 @@ let generate_rte env =
 (* eta-expansion required for typing generalisation *)
 let acc_list_rev acc l = List.fold_left (fun acc x -> x :: acc) acc l
 
-let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
+let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env t ty mk_stmts =
   let local_env, tl_env = top env in
   let local_block = local_env.block_info in
-  let is_z_t = Gmp.Z.is_t ty in
-  if is_z_t then Gmp.Z.is_now_referenced ();
-  let is_q_t = Gmp.Q.is_t ty in
-  if is_q_t then Gmp.Q.is_now_referenced ();
+  let is_z_t = Gmp_types.Z.is_t ty in
+  if is_z_t then Gmp_types.Z.is_now_referenced ();
+  let is_q_t = Gmp_types.Q.is_t ty in
+  if is_q_t then Gmp_types.Q.is_now_referenced ();
   let n = succ env.cpt in
   let v =
     Cil.makeVarinfo
@@ -214,17 +182,17 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
   in
   v.vreferenced <- true;
   let lscope = match scope with
-    | Global -> LGlobal
-    | Function -> LFunction (Extlib.the (current_kf env))
-    | Local_block -> LLocal_block (Extlib.the (current_kf env))
+    | Varname.Global -> LGlobal
+    | Varname.Function -> LFunction (Extlib.the (current_kf env))
+    | Varname.Block -> LLocal_block (Extlib.the (current_kf env))
   in
 (*  Options.feedback "new variable %a (global? %b)" Varinfo.pretty v global;*)
   let e = Cil.evar v in
   let stmts = mk_stmts v e in
   let new_stmts = acc_list_rev local_block.new_stmts stmts in
   let new_block_vars = match scope with
-    | Global | Function -> local_block.new_block_vars
-    | Local_block -> v :: local_block.new_block_vars
+    | Varname.Global | Varname.Function -> local_block.new_block_vars
+    | Varname.Block -> v :: local_block.new_block_vars
   in
   let new_block =
     { new_block_vars = new_block_vars;
@@ -246,7 +214,7 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
           | Some t -> Term.Map.add t (v, e) tbl.new_exps }
     in
     match scope with
-    | Global | Function ->
+    | Varname.Global | Varname.Function ->
       let local_env = { local_env with block_info = new_block } in
       (* also memoize the new variable, but must never be used *)
       { env with
@@ -254,7 +222,7 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
         new_global_vars = (v, lscope) :: env.new_global_vars;
         global_mp_tbl = extend_tbl env.global_mp_tbl;
         env_stack = local_env :: tl_env }
-    | Local_block ->
+    | Varname.Block ->
       let local_env =
         { block_info = new_block;
           mp_tbl = extend_tbl local_env.mp_tbl;
@@ -278,7 +246,7 @@ let do_new_var ~loc ?(scope=Local_block) ?(name="") env t ty mk_stmts =
 
 exception No_term
 
-let new_var ~loc ?(scope=Local_block) ?name env t ty mk_stmts =
+let new_var ~loc ?(scope=Varname.Block) ?name env t ty mk_stmts =
   let local_env, _ = top env in
   let memo tbl =
     try
@@ -291,8 +259,8 @@ let new_var ~loc ?(scope=Local_block) ?name env t ty mk_stmts =
       do_new_var ~loc ~scope ?name env t ty mk_stmts
   in
   match scope with
-  | Global | Function -> memo env.global_mp_tbl
-  | Local_block -> memo local_env.mp_tbl
+  | Varname.Global | Varname.Function -> memo env.global_mp_tbl
+  | Varname.Block -> memo local_env.mp_tbl
 
 let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
   new_var
@@ -301,7 +269,7 @@ let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
     ?name
     env
     t
-    (Gmp.Z.t ())
+    (Gmp_types.Z.t ())
     (fun v e -> Gmp.init ~loc e :: mk_stmts v e)
 
 module Logic_binding = struct
@@ -322,7 +290,7 @@ module Logic_binding = struct
       | Some ty -> ty
       | None -> match logic_v.lv_type with
         | Ctype ty -> ty
-        | Linteger -> Gmp.Z.t ()
+        | Linteger -> Gmp_types.Z.t ()
         | Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
         | Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
           let msg =
@@ -443,7 +411,7 @@ let pop_and_get ?(split=false) env stmt ~global_clear where =
   let local_env, tl = top env in
   let clear =
     if global_clear then begin
-      Varname.clear ();
+      Varname.clear_locals ();
       env.global_mp_tbl.clear_stmts @ local_env.mp_tbl.clear_stmts
     end else
       local_env.mp_tbl.clear_stmts
@@ -551,6 +519,6 @@ let pretty fmt env =
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
 End:
 *)

src/plugins/e-acsl/src/env.mli → src/plugins/e-acsl/src/code_generator/env.mli

@@ -41,17 +41,8 @@ type localized_scope =
   | LFunction of kernel_function
   | LLocal_block of kernel_function
 
-type scope =
-  | Global
-  | Function
-  | Local_block
-
-module Varname: sig
-  val get: scope:scope -> string -> string
-end
-
 val new_var:
-  loc:location -> ?scope:scope -> ?name:string ->
+  loc:location -> ?scope:Varname.scope -> ?name:string ->
   t -> term option -> typ -> 
   (varinfo -> exp (* the var as exp *) -> stmt list) -> 
   varinfo * exp * t
@@ -62,7 +53,7 @@ val new_var:
     initialized by applying it to [mk_stmts]. *)
 
 val new_var_and_mpz_init:
-  loc:location -> ?scope:scope -> ?name:string ->
+  loc:location -> ?scope:Varname.scope -> ?name:string ->
   t -> term option -> 
   (varinfo -> exp (* the var as exp *) -> stmt list) -> 
   varinfo * exp * t
@@ -188,6 +179,6 @@ val pretty: Format.formatter -> t -> unit
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
 End:
 *)