From d49c181bf47964af23b4a310b8d9e455f16b1a87 Mon Sep 17 00:00:00 2001 From: Francois Bobot Date: Fri, 12 Mar 2010 23:21:57 +0000 Subject: [PATCH] Ajout d'une proposition pour les transformations et les plugins dans les drivers --- Makefile.in | 31 +++++++++++++++---- bench/plugins/helloworld.drv | 9 ++++++ bench/plugins/helloworld.ml | 7 +++++ lib/drivers/alt_ergo.drv | 9 +++--- lib/drivers/why3_inline_all.drv | 8 +++++ src/core/theory.ml | 6 ++++ src/core/theory.mli | 2 ++ src/main.ml | 10 +++++- src/output/alt_ergo.ml | 7 +++-- src/output/call_provers.ml | 4 ++- src/output/driver.ml | 31 +++++++++++++++++++ src/output/driver.mli | 6 ++++ src/output/driver_ast.mli | 2 ++ src/output/driver_lexer.mll | 2 ++ src/output/driver_parser.mly | 10 +++++- src/test.why | 4 ++- src/transform/inlining.ml | 27 +++++++++++----- src/transform/inlining.mli | 4 +-- .../simplify_recursive_definition.ml | 3 +- .../simplify_recursive_definition.mli | 2 +- src/transform/transform.ml | 2 +- 21 files changed, 158 insertions(+), 28 deletions(-) create mode 100644 bench/plugins/helloworld.drv create mode 100644 bench/plugins/helloworld.ml create mode 100644 lib/drivers/why3_inline_all.drv diff --git a/Makefile.in b/Makefile.in index 88c4aefc9..b0bf62cc3 100644 --- a/Makefile.in +++ b/Makefile.in @@ -55,9 +55,9 @@ PDFVIEWER = @PDFVIEWER@ INCLUDES = -I src/core -I src/util -I src/parser -I src/output \ -I src/transform -I src/programs -I src -BFLAGS = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cma unix.cma +BFLAGS = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cma unix.cma dynlink.cma # no -warn-error because some do not compile all files (e.g. those linked to APRON) -OFLAGS = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cmxa unix.cmxa +OFLAGS = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cmxa unix.cmxa dynlink.cmxa COQC7 = @COQC7@ COQC8 = @COQC8@ @@ -116,15 +116,18 @@ UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO)) PARSER_CMO := parser.cmo lexer.cmo typing.cmo PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO)) -TRANSFORM_CMO := transform.cmo simplify_recursive_definition.cmo \ - inlining.cmo +TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO)) +DRIVER_CMO := call_provers.cmo driver_parser.cmo driver_lexer.cmo driver.cmo +DRIVER_CMO := $(addprefix src/output/,$(DRIVER_CMO)) + OUTPUT_CMO := call_provers.cmo driver_parser.cmo driver_lexer.cmo driver.cmo \ print_real.cmo alt_ergo.cmo why3.cmo OUTPUT_CMO := $(addprefix src/output/,$(OUTPUT_CMO)) CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) \ + src/transform/transform.cmo $(DRIVER_CMO)\ $(TRANSFORM_CMO) $(OUTPUT_CMO) src/main.cmo CMX = $(CMO:.cmo=.cmx) @@ -160,6 +163,7 @@ PGM_CMO := pgm_parser.cmo pgm_lexer.cmo pgm_main.cmo PGM_CMO := $(addprefix src/programs/, $(PGM_CMO)) WHYL_CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) \ + src/transform/transform.cmo $(DRIVER_CMO)\ $(TRANSFORM_CMO) $(OUTPUT_CMO) $(PGM_CMO) WHYL_CMX = $(WHYL_CMO:.cmo=.cmx) @@ -204,6 +208,17 @@ WHYVO=lib/coq/Why.vo bench:: $(BINARY) sh bench/bench "$(BINARY) -I lib/prelude/" +BENCH_PLUGINS_CMO := helloworld.cmo +BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO)) +BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs) + + +bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte + bin/why.$(OCAMLBEST) --driver bench/plugins/helloworld.drv -I lib/prelude/ \ + --output - --goal Test.G src/test.why + bin/why.byte --driver bench/plugins/helloworld.drv -I lib/prelude/ \ + --output - --goal Test.G src/test.why + # installation ############## @@ -367,7 +382,7 @@ apidoc: $(OCAMLDOCSRC) # generic rules ############### -.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .v .vo .ml4 +.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .v .vo .ml4 .cmxs .mli.cmi: $(if $(QUIET),@echo 'Ocamlc $<' &&) $(OCAMLC) $(APRONLIB) $(ATPLIB) -c $(BFLAGS) $< @@ -384,6 +399,9 @@ apidoc: $(OCAMLDOCSRC) .ml.cmx: $(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) $(APRONLIB) $(ATPLIB) -c $(OFLAGS) $< +.ml.cmxs: + $(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) $(APRONLIB) $(ATPLIB) -shared $(OFLAGS) -o $@ $< + .mll.ml: $(OCAMLLEX) $< @@ -601,6 +619,7 @@ clean:: rm -f $(GENERATED) rm -rf output_why3 rm -f ergo.why + rm -rf bench/plugins/*.cm[iox]* bench/plugins/*.annot # make -C atp clean # make -C doc clean # if test -d examples-v7; then \ @@ -618,7 +637,7 @@ coq-clean:: .PHONY: depend .depend depend: $(GENERATED) rm -f .depend - $(OCAMLDEP) -slash $(INCLUDES) src/*/*.ml src/*/*.mli src/*.ml src/*.mli > .depend + $(OCAMLDEP) -slash $(INCLUDES) src/*/*.ml src/*/*.mli src/*.ml src/*.mli bench/plugins/*.ml > .depend ifeq ($(FRAMAC),yes) # $(MAKE) -C $(JESSIE_PLUGIN_PATH) depend endif diff --git a/bench/plugins/helloworld.drv b/bench/plugins/helloworld.drv new file mode 100644 index 000000000..fe1e4b249 --- /dev/null +++ b/bench/plugins/helloworld.drv @@ -0,0 +1,9 @@ +plugin "helloworld.cmo" "helloworld.cmxs" + +printer "helloworld" + +filename "%f-%t-%s.hw" + +transformations + "helloworld" +end \ No newline at end of file diff --git a/bench/plugins/helloworld.ml b/bench/plugins/helloworld.ml new file mode 100644 index 000000000..8631bbb0e --- /dev/null +++ b/bench/plugins/helloworld.ml @@ -0,0 +1,7 @@ +let print_context _ fmt _ = Format.fprintf fmt "helloworld" + +let transform_context () = Transform.identity + +let () = + Driver.register_printer "helloworld" print_context; + Driver.register_transform "helloworld" transform_context diff --git a/lib/drivers/alt_ergo.drv b/lib/drivers/alt_ergo.drv index f950e2e11..363ea6d3f 100644 --- a/lib/drivers/alt_ergo.drv +++ b/lib/drivers/alt_ergo.drv @@ -10,13 +10,14 @@ call_on_file "alt-ergo %s" valid "Valid" invalid "Invalid" unknown "I don't know" "Unknown" +fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1" -(* -tranformations +(* À discuter *) +transformations "simplify_recursive_definition" - "inlining" ("trivial") + "inline_trivial" end -*) + theory BuiltIn syntax type int "int" diff --git a/lib/drivers/why3_inline_all.drv b/lib/drivers/why3_inline_all.drv new file mode 100644 index 000000000..a1c6a3942 --- /dev/null +++ b/lib/drivers/why3_inline_all.drv @@ -0,0 +1,8 @@ +printer "why3" +filename "%f-%t-%s.why" + +(* À discuter *) +transformations + "simplify_recursive_definition" + "inline_all" +end diff --git a/src/core/theory.ml b/src/core/theory.ml index 235d43f8a..a0c56efc7 100644 --- a/src/core/theory.ml +++ b/src/core/theory.ml @@ -53,6 +53,12 @@ let create_prop n f = { pr_fmla = check_fvs f; } +let shortcut_for_discussion_dont_be_mad_andrei_please n f = +{ + pr_name = n; + pr_fmla = check_fvs f; +} + (** Declarations *) (* type declaration *) diff --git a/src/core/theory.mli b/src/core/theory.mli index 882fd5933..eef7aac49 100644 --- a/src/core/theory.mli +++ b/src/core/theory.mli @@ -34,6 +34,8 @@ module Hpr : Hashtbl.S with type key = prop val create_prop : preid -> fmla -> prop +val shortcut_for_discussion_dont_be_mad_andrei_please : ident -> fmla -> prop + (** Declarations *) (* type declaration *) diff --git a/src/main.ml b/src/main.ml index 385d61d5a..576d5d973 100644 --- a/src/main.ml +++ b/src/main.ml @@ -97,6 +97,8 @@ let rec report fmt = function fprintf fmt "anomaly: unknownident %s" i.Ident.id_short | Driver.Error e -> Driver.report fmt e + | Dynlink.Error e -> + fprintf fmt "Dynlink : %s" (Dynlink.error_message e) | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e) (* @@ -150,6 +152,7 @@ let do_file env drv filename_printer file = match drv with | None -> eprintf "a driver is needed@."; exit 1 | Some drv -> drv in + (* Extract the goal(s) *) let goals = match !which_goals with | Gall -> Mnm.fold (fun _ th acc -> extract_goals env acc th) m [] @@ -182,6 +185,11 @@ let do_file env drv filename_printer file = | Dprop (_,{pr_name = pr_name}) -> Ident.derived_from pr_name pr.pr_name | _ -> assert false) goals in + (* Apply transformations *) + let goals = List.map + (fun (th,ctxt) -> (th,Driver.transform_context drv ctxt)) + goals in + (* Pretty-print the goals or call the prover *) match !output with | None (* we are in the call mode *) -> let call (th,ctxt) = @@ -191,7 +199,7 @@ let do_file env drv filename_printer file = (goal_of_ctxt ctxt).pr_name.Ident.id_long Call_provers.print_prover_result res in List.iter call goals - | Some dir -> + | Some dir (* we are in the output mode *) -> let file = let file = Filename.basename file in let file = Filename.chop_extension file in diff --git a/src/output/alt_ergo.ml b/src/output/alt_ergo.ml index 4f39d3cfa..18255638e 100644 --- a/src/output/alt_ergo.ml +++ b/src/output/alt_ergo.ml @@ -59,7 +59,7 @@ let rec print_term drv fmt t = match t.t_node with assert false | Tconst c -> Pretty.print_const fmt c - | Tvar { vs_name = id } | Tapp ({ ls_name = id }, []) -> + | Tvar { vs_name = id } -> print_ident fmt id | Tapp (ls, tl) -> begin @@ -67,7 +67,10 @@ let rec print_term drv fmt t = match t.t_node with | Driver.Remove -> assert false (* Mettre une erreur *) | Driver.Syntax s -> Driver.syntax_arguments s (print_term drv) fmt tl - | Driver.Tag _ -> + | Driver.Tag _ -> + match tl with + | [] -> print_ident fmt ls.ls_name + | tl -> fprintf fmt "%a(%a)" print_ident ls.ls_name (print_list comma (print_term drv)) tl end diff --git a/src/output/call_provers.ml b/src/output/call_provers.ml index 9e962170e..30d8ff08f 100644 --- a/src/output/call_provers.ml +++ b/src/output/call_provers.ml @@ -42,7 +42,9 @@ type prover_result = pr_stdout : string} let print_prover_result fmt pr = - fprintf fmt "%a (%.2fs)" print_prover_answer pr.pr_answer pr.pr_time + fprintf fmt "%a (%.2fs)" print_prover_answer pr.pr_answer pr.pr_time; + if pr.pr_answer == HighFailure + then fprintf fmt "@\nstdout-stderr : \"%s\"" pr.pr_stdout; type prover = { pr_call_stdin : string option; (* %f pour le nom du fichier *) diff --git a/src/output/driver.ml b/src/output/driver.ml index f123da020..7c3f4a099 100644 --- a/src/output/driver.ml +++ b/src/output/driver.ml @@ -126,6 +126,7 @@ and driver = { drv_prover : Call_provers.prover; drv_prelude : string option; drv_filename : string option; + drv_transformations : Transform.ctxt_t list; drv_rules : theory_rules list; drv_thprelude : string Hid.t; (* the first is the translation only for this ident, the second is also for representant *) @@ -140,6 +141,11 @@ let print_driver fmt driver = (Pp.print_pair print_translation print_translation)) driver.drv_theory +(** registering transformation *) + +let (transforms : (string, unit -> Transform.ctxt_t) Hashtbl.t) = Hashtbl.create 17 + +let register_transform name transform = Hashtbl.replace transforms name transform (** registering printers *) @@ -147,6 +153,17 @@ let (printers : (string, printer) Hashtbl.t) = Hashtbl.create 17 let register_printer name printer = Hashtbl.replace printers name printer + +let () = + Dynlink.allow_only ["Theory";"Term";"Ident";"Transform";"Driver"; + "Pervasives";"Format";"List";"Sys";"Unix"] + + +let load_plugin dir (byte,nat) = + let file = if Dynlink.is_native then nat else byte in + let file = Filename.concat dir file in + Dynlink.loadfile_private file + let load_file file = let c = open_in file in let lb = Lexing.from_channel c in @@ -265,6 +282,7 @@ let load_driver file env = let call_stdin = ref None in let call_file = ref None in let filename = ref None in + let transformations = ref None in let regexps = ref [] in let set_or_raise loc r v error = if !r <> None then errorm ~loc "duplicate %s" error @@ -284,9 +302,17 @@ let load_driver file env = | RegexpUnknown (s1,s2) -> regexps:=(s1,Unknown s2)::!regexps | RegexpFailure (s1,s2) -> regexps:=(s1,Failure s2)::!regexps | Filename s -> set_or_raise loc filename s "filename" + | Transformations s -> set_or_raise loc transformations s "transformations" + | Plugin files -> load_plugin (Filename.dirname file) files in List.iter add f.f_global; let regexps = List.map (fun (s,a) -> (Str.regexp s,a)) !regexps in + let transformations = match !transformations with + | None -> [] | Some l -> l in + let transformations = + List.map (fun (loc,s) -> try (Hashtbl.find transforms s) () + with Not_found -> errorm ~loc "unknown transformation %s" s) + transformations in { drv_printer = !printer; drv_context = Context.init_context env; drv_prover = {Call_provers.pr_call_stdin = !call_stdin; @@ -294,6 +320,7 @@ let load_driver file env = pr_regexps = regexps}; drv_prelude = !prelude; drv_filename = !filename; + drv_transformations = transformations; drv_rules = f.f_rules; drv_thprelude = Hid.create 1; drv_theory = Hid.create 1; @@ -327,6 +354,10 @@ let syntax_arguments s print fmt l = (** using drivers *) +let transform_context drv ctxt = + List.fold_left (fun ctxt t -> Transform.apply t ctxt) + ctxt drv.drv_transformations + let print_context drv fmt ctxt = match drv.drv_printer with | None -> errorm "no printer" | Some f -> let drv = {drv with drv_context = ctxt; diff --git a/src/output/driver.mli b/src/output/driver.mli index 8901a3105..c10d6f7e2 100644 --- a/src/output/driver.mli +++ b/src/output/driver.mli @@ -44,8 +44,14 @@ type printer = driver -> formatter -> context -> unit val register_printer : string -> printer -> unit +val register_transform : string -> (unit -> Transform.ctxt_t) -> unit + (** using drivers *) +(** transform context *) +val transform_context : driver -> context -> context + +(** print_context *) val print_context : printer val filename_of_goal : driver -> Ident.ident_printer -> diff --git a/src/output/driver_ast.mli b/src/output/driver_ast.mli index 5c358cf19..6c9f229b3 100644 --- a/src/output/driver_ast.mli +++ b/src/output/driver_ast.mli @@ -47,6 +47,8 @@ type global = | RegexpUnknown of string * string | RegexpFailure of string * string | Filename of string + | Transformations of (loc * string) list + | Plugin of (string * string) type file = { f_global : (loc * global) list; diff --git a/src/output/driver_lexer.mll b/src/output/driver_lexer.mll index 2e090c8ab..f275f172d 100644 --- a/src/output/driver_lexer.mll +++ b/src/output/driver_lexer.mll @@ -45,6 +45,8 @@ "type", TYPE; "prop", PROP; "filename", FILENAME; + "transformations", TRANSFORMATIONS; + "plugin", PLUGIN ] } diff --git a/src/output/driver_parser.mly b/src/output/driver_parser.mly index 5b1161207..19bce802c 100644 --- a/src/output/driver_parser.mly +++ b/src/output/driver_parser.mly @@ -32,7 +32,7 @@ %token THEORY END SYNTAX REMOVE TAG PRELUDE PRINTER CALL_ON_FILE CALL_ON_STDIN %token VALID INVALID UNKNOWN FAIL %token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF -%token LOGIC TYPE PROP FILENAME +%token LOGIC TYPE PROP FILENAME TRANSFORMATIONS PLUGIN %type file %start file @@ -59,8 +59,16 @@ global: | UNKNOWN STRING STRING { RegexpUnknown ($2, $3) } | FAIL STRING STRING { RegexpFailure ($2, $3) } | FILENAME STRING { Filename $2 } +| TRANSFORMATIONS list0_string END { Transformations $2 } +| PLUGIN STRING STRING { Plugin ($2,$3) } ; +list0_string: +| /* epsilon */ { [] } +| STRING list0_string { (loc_i 1, $1) :: $2 } +; + + list0_theory: | /* epsilon */ { [] } | theory list0_theory { $1 :: $2 } diff --git a/src/test.why b/src/test.why index c2ee6c6cd..d34afaa91 100644 --- a/src/test.why +++ b/src/test.why @@ -4,8 +4,10 @@ theory Test use import prelude.Int logic id(x: int) : int = x + logic id2(x: int) : int = id(x) + logic succ(x:int) : int = id(x+1) logic even(x: int) = 2*(x/2) = x - goal G : forall x:int. 0 = 0 + goal G : forall x:int. 1 = succ(id2(zero)) goal G2 : forall x:int. 0 = 1 end diff --git a/src/transform/inlining.ml b/src/transform/inlining.ml index 19037c4f7..c88cd9321 100644 --- a/src/transform/inlining.ml +++ b/src/transform/inlining.ml @@ -96,7 +96,7 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) = | Dind dl -> env, add_decl ctxt (create_ind_decl (List.map (fun (ps,fmlal) -> ps, List.map (fun pr -> - create_prop (id_dup pr.pr_name) (replacep env pr.pr_fmla)) + create_prop (id_clone pr.pr_name) (replacep env pr.pr_fmla)) fmlal) dl)) | Dlogic dl -> env, add_decl ctxt (create_logic_decl @@ -114,20 +114,33 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) = Lpredicate (ps,Some (make_ps_defn ps vs t)) ) dl)) | Dtype dl -> env,add_decl ctxt d - | Dprop (k,pr) -> env,add_decl ctxt (create_prop_decl k - (create_prop (id_dup pr.pr_name) (replacep env pr.pr_fmla))) + | Dprop (k,pr) -> + let prop = shortcut_for_discussion_dont_be_mad_andrei_please + pr.pr_name (replacep env pr.pr_fmla) in + env,add_decl ctxt (create_prop_decl k prop) | Duse _ | Dclone _ -> env,add_decl ctxt d let t ~isnotinlinedt ~isnotinlinedf = Transform.fold_map (fold isnotinlinedt isnotinlinedf) empty_env -let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false) +let all () = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false) -let trivial = t +let trivial () = t ~isnotinlinedt:(fun m -> match m.t_node with | Tconst _ | Tvar _ -> false | Tapp (ls,tl) when List.for_all - (fun m -> match m.t_node with Tvar _ -> true | _ -> false) tl -> true + (fun m -> match m.t_node with + | Tvar _ -> true + | _ -> false) tl -> false | _ -> true ) - ~isnotinlinedf:(fun m -> match m.f_node with Ftrue | Ffalse | Fapp _ -> false + ~isnotinlinedf:(fun m -> match m.f_node with + | Ftrue | Ffalse -> false + | Fapp (ls,tl) when List.for_all + (fun m -> match m.t_node with + | Tvar _ -> true + | _ -> false) tl -> false | _ -> true) + +let () = + Driver.register_transform "inline_all" all; + Driver.register_transform "inline_trivial" trivial diff --git a/src/transform/inlining.mli b/src/transform/inlining.mli index a9e844d21..1f4aec90b 100644 --- a/src/transform/inlining.mli +++ b/src/transform/inlining.mli @@ -28,12 +28,12 @@ val t : (* Inline them all *) -val all : Transform.ctxt_t +val all : unit -> Transform.ctxt_t (* Inline only the trivial definition : logic c : t = a logic f(x : t,...., ) : t = g(y : t2,...) *) -val trivial : Transform.ctxt_t +val trivial : unit -> Transform.ctxt_t (* Function to use in other transformations if inlining is needed *) diff --git a/src/transform/simplify_recursive_definition.ml b/src/transform/simplify_recursive_definition.ml index a2a245c17..dbeddfe81 100644 --- a/src/transform/simplify_recursive_definition.ml +++ b/src/transform/simplify_recursive_definition.ml @@ -140,5 +140,6 @@ let elt d = | Dind _ -> [d] (* TODO *) | Dprop _ | Dclone _ | Duse _ -> [d] -let t = Transform.elt elt +let t () = Transform.elt elt +let () = Driver.register_transform "simplify_recursive_definition" t diff --git a/src/transform/simplify_recursive_definition.mli b/src/transform/simplify_recursive_definition.mli index eed3d7249..56ce99ad9 100644 --- a/src/transform/simplify_recursive_definition.mli +++ b/src/transform/simplify_recursive_definition.mli @@ -20,7 +20,7 @@ (* Simplify the recursive type and logic definition *) -val t : Transform.ctxt_t +val t : unit -> Transform.ctxt_t (* ungroup recursive definition *) diff --git a/src/transform/transform.ml b/src/transform/transform.ml index 231b54587..2bd80b219 100644 --- a/src/transform/transform.ml +++ b/src/transform/transform.ml @@ -147,7 +147,7 @@ let split_goals = let g = fold_env f (fun env -> init_context env, []) in conv_res g snd -let extract_goals = +let extract_goals () = let f ctxt0 (ctxt,l) = let decl = ctxt0.ctxt_decl in match decl.d_node with -- GitLab