...
 
Commits (31)
......@@ -38,8 +38,9 @@ why3.conf
/distrib
/why3regtests.err
/why3regtests.out
/.merlin
.merlin
/src/jessie/.merlin
/why3*.install
# /bench/
/bench/programs/good/booleans/
......@@ -338,3 +339,4 @@ pvsbin/
/trash
trywhy3.tar.gz
/_build/
......@@ -152,11 +152,16 @@ endif
# main target
###############
ifeq (@enable_why3_lib@,yes)
all: @OCAMLBEST@
else
all:
endif
.PHONY: dune
all: dune
dune: src/util/config.ml
dune build @install
$(HIDE) mkdir -p bin
clean::
dune clean
plugins: plugins.@OCAMLBEST@
opt: plugins.opt
......@@ -216,7 +221,7 @@ LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer dri
LIB_MLW = ity expr pdecl eval_match typeinv vc pmodule dexpr \
pinterp mltree compile mlinterp pdriver cprinter ml_printer \
ocaml_printer cakeml_printer
ocaml_printer yul_printer cakeml_printer
LIB_PARSER = ptree glob typing parser typing lexer
......@@ -326,10 +331,6 @@ lib/why3/why3.cmx: $(LIBCMX) lib/why3/why3.cmo
# clean and depend
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(LIBDEP)
endif
depend: $(LIBDEP)
CLEANDIRS += src $(addprefix src/, $(LIBDIRS))
......@@ -493,11 +494,6 @@ lib/plugins/python.cmxs: $(PYTHONCMX)
lib/plugins/python.cmo: $(PYTHONCMO)
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(PLUGDEP)
endif
depend: $(PLUGDEP)
CLEANDIRS += plugins $(addprefix plugins/, $(PLUGDIRS)) lib/plugins
......@@ -574,8 +570,9 @@ install-bin::
install_local:: bin/why3 $(addprefix bin/,$(TOOLS_BIN))
bin/%: bin/%.@OCAMLBEST@
ln -sf $(notdir $<) $@
#TODO use dune promote or dune exec
bin/%: dune
$(HIDE) cp _build/install/default/bin/$* $@
install_local:: share/drivers share/stdlib
......@@ -585,10 +582,6 @@ share/drivers:
share/stdlib:
ln -snf ../stdlib share/stdlib
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(TOOLSDEP)
endif
depend: $(TOOLSDEP)
CLEANDIRS += src/tools
......@@ -739,7 +732,7 @@ ifeq (@enable_ide@,yes)
IDEGENERATED = src/ide/gtkcompat.ml
IDE_FILES = gtkcompat gconfig ide_utils why3ide
IDE_FILES = gtkcompat gconfig ide_utils why3_resetgc why3ide
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
......@@ -769,11 +762,6 @@ src/ide/resetgc.o: src/ide/resetgc.c
$(HIDE)$(OCAMLC) -c -ccopt "-Wall -o $@" $<
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(IDEDEP)
endif
depend: $(IDEDEP)
CLEANDIRS += src/ide
......@@ -843,11 +831,6 @@ bin/why3webserver.byte: $(WHY3CMA) $(WEBSERVCMO)
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(WEBSERVDEP)
endif
depend: $(WEBSERVDEP)
CLEANDIRS += src/ide
......@@ -891,10 +874,6 @@ bin/why3session.byte: $(WHY3CMA) $(SESSIONCMO)
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(SESSIONDEP)
endif
depend: $(SESSIONDEP)
CLEANDIRS += src/why3session
......@@ -937,11 +916,6 @@ bin/why3shell.byte: $(WHY3CMA) $(SHELLCMO)
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(SHELLDEP)
endif
depend: $(SHELLDEP)
uninstall-bin::
......@@ -1408,7 +1382,7 @@ endif
install-isabelle: $(GENERATED_PREFIX_ISABELLE)/last_build
install_local:: install-isabelle
####TODO install_local:: install-isabelle
install:: install-isabelle
clean::
......@@ -1416,7 +1390,7 @@ clean::
endif
all: drivers/isabelle-realizations.aux
####TODO all: drivers/isabelle-realizations.aux
install-data::
$(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
......@@ -1499,10 +1473,6 @@ install-lib::
$(INSTALL_DATA) $(wildcard $(addprefix lib/why3/why3extract., $(INSTALLED_LIB_EXTS))) \
$(OCAMLINSTALLLIB)/why3
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(OCAMLLIBS_DEP)
endif
$(OCAMLLIBS_DEP): lib/ocaml/why3__BigInt_compat.ml
depend: $(OCAMLLIBS_DEP)
......@@ -1571,10 +1541,6 @@ bin/why3doc.byte: $(WHY3CMA) $(WHY3DOCCMO)
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(WHY3DOCDEP)
endif
depend: $(WHY3DOCDEP)
CLEANDIRS += src/why3doc
......
module A
use list.List
use int.Int
use ref.Ref
use mach.int.UInt32
use list.Length
use mach.int.Int32
exception Error
let f1 (x:int32) =
x-1
let rec g1 (x:int32)
variant { x }
=
if x < 1 then 1 else (g1 (f1 x) * (2:int32))
(*
type t = { a: int32; b : int32 }
let f () =
{ a = 0; b = 1}
let g [@ evm:external] ()
=
(f ()).b
*)
use mach.evm.Gas
let rec length4 [@ evm:gas_checking] (l:list 'a) : int32
requires { (length l) <= max_int32 }
ensures { !gas - old !gas <= (length l) * 128 + 71 }
ensures { !alloc - old !alloc <= 0 }
ensures { result = length l }
variant { l } =
match l with
| Nil -> add_gas 71 0; 0
| Cons _ l -> add_gas 128 0; 1 + length4 l
end
let rec mk4 [@ evm:gas_checking] (i:int32) : list int32
requires { 0 <= i }
ensures { !gas - old !gas <= i * 185 + 113 }
ensures { !alloc - old !alloc <= i * 96 + 32 }
ensures { i = length result }
variant { i } =
if i <= 0 then (add_gas 113 32; Nil) else
let l = mk4 (i-1) in
add_gas 185 96;
Cons (0x42:int32) l
let g4 [@ evm:gas_checking] (i:int32) : int32
requires { 0 <= i }
ensures { !gas - old !gas <= i * 313 + 242 }
ensures { !alloc - old !alloc <= i * 96 + 32 }
=
add_gas 58 0;
let l = mk4 i in
length4 l
let g4' [@ evm:gas_checking] () : int32
(* raises { Error -> true } *)
=
label H in
add_gas 78 0;
let gas1 = get_remaining_gas () in
let r1 = g4 4 in
let gas2 = get_remaining_gas () in
assert { !gas - (!gas at H) <= 4 * 313 + 242 };
assert { !alloc - (!alloc at H) <= 4 * 96 + 32 };
assert { actual_gas_used (!gas - (!gas at H)) (!alloc - (!alloc at H)) <= 1494 };
(* evm doesn't have the same cost function *)
(* if not (UInt256.(gas1 - gas2 <= 1494)) then raise Error; *)
add_gas 24 0;
r1
type mut = { mutable v: int32 }
let g5 i =
let r = { v = 0 } in
r.v <- i;
r.v
let m6 = { v = 0 }
let g6 i : int32 =
let j = m6.v in
m6.v <- i;
j
let g7 [@ evm:gas_checking] (x:int32) : int32 =
add_gas 66 0;
if x <= 0 then 0 else 2
let g8 [@ evm:gas_checking] (x:int32) : int32 =
if x <= 0 then (add_gas 56 0; 0) else (add_gas 66 0; 2)
let g9 [@ evm:gas_checking] (x:int32) : int32 =
add_gas 109 1;
let r = ref x in
r := !r - (1:int32);
!r
use mach.evm.ArrayUInt32
let g10 [@ evm:gas_checking] (n:uint32) (x:uint32) : uint32
ensures { !alloc = old !alloc + n }
=
add_gas 159 0;
let r = make n in
r[0] <- x;
r[n-1] <- x+(length r);
r[0] + r[n-1]
let g [@ evm:external] () : bool
raises { Error -> true }
=
(* test 1 *)
let () =
let r1 = g1 4 in
let o1 : int32 = (0x10:int32) in
if not (r1 = o1) then raise Error
in
(* test 4 *)
let () =
label H in
let r1 = g4' () in
let o1 : int32 = (4:int32) in
if not (r1 = o1) then raise Error
in
(* test 5 *)
let () =
let r1 = g5 (0x4444) in
let o1 : int32 = (0x4444:int32) in
if not (r1 = o1) then raise Error
in
(* test 6 *)
m6.v <- 0;
let () =
let r1 = g6 4 in
let r2 = g6 5 in
let o1 : int32 = (4:int32) in
if not (r1 = 0) then raise Error;
if not (r2 = o1) then raise Error
in
(* test 7 *)
let () =
let r1 = g7 (0x4) in
let o1 : int32 = (0x2:int32) in
if not (r1 = o1) then raise Error
in
(* test 8 *)
let () =
let r1 = g8 (0x4) in
let o1 : int32 = (0x2:int32) in
if not (r1 = o1) then raise Error
in
(* test 9 *)
let () =
let r1 = g9 (0x4) in
let o1 : int32 = (0x3:int32) in
if not (r1 = o1) then raise Error
in
(* test 10 *)
let () =
let r1 = g10 (0x10) (0x4) in
let o1 : uint32 = (0x18:uint32) in
if not (r1 = o1) then raise Error
in
false
end
(** OCaml driver for 64-bit architecture *)
printer "evm"
theory BuiltIn
syntax type int "Z.t"
syntax predicate (=) "%1 = %2"
end
theory Bool
syntax type bool "bool"
syntax function True "true:bool"
syntax function False "false:bool"
end
theory bool.Ite
syntax function ite "(if %1 then %2 else %3)"
end
theory bool.Bool
syntax function andb "and(%1,%2)"
syntax function orb "or(%1,%2)"
syntax function xorb "xor(%1,%2)"
syntax function notb "not(%1)"
syntax function implb "or(not(%1),%2)"
end
module Ref
syntax type ref ""
syntax function contents "[]"
syntax val ref "[[\"ALLOCATE\",1],\"SWAP1\",\"DUP2\",\"MSTORE\"]"
end
module ref.Ref
syntax val (!_) "[\"MLOAD\"]"
syntax val (:=) "[\"MSTORE\"]"
end
module ref.Refint
syntax val incr "%1 := Z.succ (!%1)"
syntax val decr "%1 := Z.pred (!%1)"
syntax val (+=) "%1 := Z.add (!%1) %2"
syntax val (-=) "%1 := Z.sub (!%1) %2"
syntax val ( *= ) "%1 := Z.mul (!%1) %2"
end
module mach.int.Int32
syntax type int32 "s32"
syntax val ( + ) "[\"ADD\"]"
syntax val ( - ) "[\"SUB\"]"
syntax val (-_) "[[\"PUSH1\",0],\"SWAP1\",\"SUB\"]"
syntax val ( * ) "[\"MUL\"]"
syntax val ( / ) "[\"SDIV\"]"
syntax val ( % ) "[\"SMOD\"]"
syntax val (=) "[\"EQ\"]"
syntax val (<=) "[\"DUP2\",\"DUP2\",\"SLT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (<) "[\"SLT\"]"
syntax val (>=) "[\"DUP2\",\"DUP2\",\"SGT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (>) "[\"SGT\"]"
end
module mach.int.UInt32
syntax type uint32 "u32"
syntax val ( + ) "[\"ADD\"]"
syntax val ( - ) "[\"SUB\"]"
syntax val (-_) "[[\"PUSH1\",0],\"SWAP1\",\"SUB\"]"
syntax val ( * ) "[\"MUL\"]"
syntax val ( / ) "[\"DIV\"]"
syntax val ( % ) "[\"MOD\"]"
syntax val (=) "[\"EQ\"]"
syntax val (<=) "[\"DUP2\",\"DUP2\",\"LT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (<) "[\"LT\"]"
syntax val (>=) "[\"DUP2\",\"DUP2\",\"GT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (>) "[\"GT\"]"
end
module mach.int.Int64
syntax type int64 "s64"
syntax val ( + ) "[\"ADD\"]"
syntax val ( - ) "[\"SUB\"]"
syntax val (-_) "[[\"PUSH1\",0],\"SWAP1\",\"SUB\"]"
syntax val ( * ) "[\"MUL\"]"
syntax val ( / ) "[\"SDIV\"]"
syntax val ( % ) "[\"SMOD\"]"
syntax val (=) "[\"EQ\"]"
syntax val (<=) "[\"DUP2\",\"DUP2\",\"SLT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (<) "[\"SLT\"]"
syntax val (>=) "[\"DUP2\",\"DUP2\",\"SGT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (>) "[\"SGT\"]"
end
module mach.int.UInt64
syntax type uint64 "u64"
syntax val ( + ) "[\"ADD\"]"
syntax val ( - ) "[\"SUB\"]"
syntax val (-_) "[[\"PUSH1\",0],\"SWAP1\",\"SUB\"]"
syntax val ( * ) "[\"MUL\"]"
syntax val ( / ) "[\"DIV\"]"
syntax val ( % ) "[\"MOD\"]"
syntax val (=) "[\"EQ\"]"
syntax val (<=) "[\"DUP2\",\"DUP2\",\"LT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (<) "[\"LT\"]"
syntax val (>=) "[\"DUP2\",\"DUP2\",\"GT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (>) "[\"GT\"]"
end
module mach.int.Int128
syntax type int128 "s128"
syntax val ( + ) "[\"ADD\"]"
syntax val ( - ) "[\"SUB\"]"
syntax val (-_) "[[\"PUSH1\",0],\"SWAP1\",\"SUB\"]"
syntax val ( * ) "[\"MUL\"]"
syntax val ( / ) "[\"SDIV\"]"
syntax val ( % ) "[\"SMOD\"]"
syntax val (=) "[\"EQ\"]"
syntax val (<=) "[\"DUP2\",\"DUP2\",\"SLT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (<) "[\"SLT\"]"
syntax val (>=) "[\"DUP2\",\"DUP2\",\"SGT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (>) "[\"SGT\"]"
end
module mach.int.UInt128
syntax type uint128 "u128"
syntax val ( + ) "[\"ADD\"]"
syntax val ( - ) "[\"SUB\"]"
syntax val (-_) "[[\"PUSH1\",0],\"SWAP1\",\"SUB\"]"
syntax val ( * ) "[\"MUL\"]"
syntax val ( / ) "[\"DIV\"]"
syntax val ( % ) "[\"MOD\"]"
syntax val (=) "[\"EQ\"]"
syntax val (<=) "[\"DUP2\",\"DUP2\",\"LT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (<) "[\"LT\"]"
syntax val (>=) "[\"DUP2\",\"DUP2\",\"GT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (>) "[\"GT\"]"
end
module mach.int.Int256
syntax type int256 "s256"
syntax val ( + ) "[\"ADD\"]"
syntax val ( - ) "[\"SUB\"]"
syntax val (-_) "[[\"PUSH1\",0],\"SWAP1\",\"SUB\"]"
syntax val ( * ) "[\"MUL\"]"
syntax val ( / ) "[\"SDIV\"]"
syntax val ( % ) "[\"SMOD\"]"
syntax val (=) "[\"EQ\"]"
syntax val (<=) "[\"DUP2\",\"DUP2\",\"SLT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (<) "[\"SLT\"]"
syntax val (>=) "[\"DUP2\",\"DUP2\",\"SGT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (>) "[\"SGT\"]"
end
module mach.int.UInt256
syntax type uint256 "u256"
syntax val ( + ) "[\"ADD\"]"
syntax val ( - ) "[\"SUB\"]"
syntax val (-_) "[[\"PUSH1\",0],\"SWAP1\",\"SUB\"]"
syntax val ( * ) "[\"MUL\"]"
syntax val ( / ) "[\"DIV\"]"
syntax val ( % ) "[\"MOD\"]"
syntax val (=) "[\"EQ\"]"
syntax val (<=) "[\"DUP2\",\"DUP2\",\"LT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (<) "[\"LT\"]"
syntax val (>=) "[\"DUP2\",\"DUP2\",\"GT\",\"SWAP2\",\"EQ\",\"OR\"]"
syntax val (>) "[\"GT\"]"
end
module mach.evm.Gas
syntax val add_gas "add_gas"
syntax val get_remaining_gas "get_gas"
end
module mach.evm.ArrayUInt32
(** the pointer is after the stored length *)
syntax val ([]) "[\"SWAP1\",[\"PUSH1\",32],\"MUL\",\"ADD\",\"MLOAD\"]"
syntax val ([]<-) "[\"SWAP1\",[\"PUSH1\",32],\"MUL\",\"ADD\",\"MSTORE\"]"
syntax val length "[[\"PUSH1\",32],\"SWAP1\",\"SUB\",\"MLOAD\"]"
syntax val make "[\"DUP1\",[\"PUSH1\",1],\"ADD\",[\"PUSH1\",32],\"MUL\",\"ALLOCATE_DYN\",\"SWAP1\",\"DUP2\",\"MSTORE\",[\"PUSH1\",32],\"ADD\"]"
end
module mach.evm.ArrayUInt64
syntax val ([]) "[\"SWAP1\",[\"PUSH1\",32],\"MUL\",\"ADD\",\"MLOAD\"]"
syntax val ([]<-) "[\"SWAP1\",[\"PUSH1\",32],\"MUL\",\"ADD\",\"MSTORE\"]"
syntax val length "[[\"PUSH1\",1],\"SWAP1\",\"SUB\",\"MLOAD\"]"
syntax val make "[\"DUP1\",[\"PUSH1\",1],\"ADD\",\"ALLOCATE_DYN\",\"DUP1\",\"MSTORE\",[\"PUSH1\",1],\"ADD\"]"
end
(lang dune 1.6)
(using menhir 2.0)
......@@ -39,8 +39,8 @@ RUN opam repository add coq-released https://coq.inria.fr/opam/released --all-sw
ARG opam_packages
RUN opam install -y depext
RUN opam depext --dry-run menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo
RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo
RUN opam depext --dry-run menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo dune
RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo dune
RUN test -z "$opam_packages" || opam depext --dry-run $opam_packages
RUN test -z "$opam_packages" || opam install -y $opam_packages
(library
(name why3_core)
(public_name why3.core)
(modules
ident ty term pattern decl coercion theory
task pretty dterm env trans printer model_parser
)
(flags -open Why3_util -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util num)
)
(ocamllex driver_lexer parse_smtv2_model_lexer)
(menhir (modules driver_parser parse_smtv2_model_parser))
(library
(name why3_driver)
(public_name why3.driver)
(modules
prove_client call_provers driver_ast driver_parser driver_lexer driver
whyconf autodetection
smt2_model_defs parse_smtv2_model_parser
collect_data_model parse_smtv2_model_lexer parse_smtv2_model
parse_smtv2_model
)
(flags -open Why3_util -open Why3_core -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core num unix)
)
(library
(public_name why3)
(modules v1 v2)
(libraries why3.util why3.core why3.driver why3.parser why3.transform why3.printer why3.session)
)
(executable
(public_name why3ide)
(modules gtkcompat gconfig ide_utils why3ide)
(libraries why3 why3_resetgc
(select gtkcompat.ml from
(lablgtk3 lablgtk3-sourceview3 -> gtkcompat3.ml )
(lablgtk2 lablgtk2.sourceview2 -> gtkcompat2.ml )
)
)
(flags -open Why3.V1 -linkall)
(package why3-ide)
)
(library
(name why3_resetgc)
(modules why3_resetgc)
(c_names resetgc)
)
(executable
(name why3web)
(public_name why3webserver)
(modules wserver why3web)
(libraries why3)
(flags -open Why3.V1 -linkall)
(package why3)
)
external reset_gc : unit -> unit = "ml_reset_gc"
......@@ -18,8 +18,6 @@ open History
open Itp_communication
open Gtkcompat
external reset_gc : unit -> unit = "ml_reset_gc"
let debug = Debug.lookup_flag "ide_info"
let debug_stack_trace = Debug.lookup_flag "stack_trace"
......@@ -952,7 +950,7 @@ let fan =
let update_monitor =
let c = ref 0 in
fun t s r ->
reset_gc ();
Why3_resetgc.reset_gc ();
incr c;
let f = if r = 0 then " " else fan !c in
let text = Printf.sprintf "%s %d/%d/%d" f t s r in
......
(library
(name why3_mlw)
(public_name why3.mlw)
(modules
ity expr pdecl eval_match typeinv vc pmodule dexpr
pinterp mltree compile mlinterp pdriver cprinter ml_printer
ocaml_printer cakeml_printer evm_printer
)
(flags -open Why3_util -open Why3_core -open Why3_driver -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core why3.driver num unix cryptokit)
)
This diff is collapsed.
......@@ -83,6 +83,27 @@ and rdef = {
rec_svar : Stv.t; (* set of type variables *)
}
let rec print_expr fmt e =
match e.e_node with
| Econst _ -> Format.fprintf fmt "Econst"
| Evar v -> Format.fprintf fmt "Evar(%s)" v.Ity.pv_vs.vs_name.Ident.id_string
| Eapp (rs,_) -> Format.fprintf fmt "Eapp(%s)" rs.rs_name.Ident.id_string
| Efun _ -> Format.fprintf fmt "Efun"
| Elet (Lvar (v,e2),e3) -> Format.fprintf fmt "Elet(%s,%a,%a)" v.Ity.pv_vs.vs_name.Ident.id_string print_expr e2 print_expr e3
| Elet _ -> Format.fprintf fmt "Elet"
| Eif _ -> Format.fprintf fmt "Eif"
| Eassign _ -> Format.fprintf fmt "Eassign"
| Ematch _ -> Format.fprintf fmt "Ematch"
| Eblock _ -> Format.fprintf fmt "Eblock"
| Ewhile _ -> Format.fprintf fmt "Ewhile"
(* For loop for Why3's type int *)
| Efor _ -> Format.fprintf fmt "Efor"
| Eraise _ -> Format.fprintf fmt "Eraise"
| Eexn _ -> Format.fprintf fmt "Eexn"
| Eignore _ -> Format.fprintf fmt "Eignore"
| Eabsurd -> Format.fprintf fmt "Eabsurd"
type is_mutable = bool
type typedef =
......
......@@ -258,8 +258,17 @@ type printer =
interf_printer : interf_printer option;
prelude_printer : prelude_printer; }
type printer_only_flat = {
desc_only_flat : Pp.formatted;
file_gen_only_flat : filename_generator;
decls_printer_only_flat : printer_args -> (Pmodule.pmodule * Mltree.decl) list Pp.pp;
}
type printer_spec =
| OnlyFlat of printer_only_flat
| DeclByDecl of printer
let printers : printer Hstr.t = Hstr.create 17
let printers : printer_spec Hstr.t = Hstr.create 17
exception KnownPrinter of string
exception UnknownPrinter of string
......@@ -267,7 +276,11 @@ exception NoPrinter
let register_printer s p =
if Hstr.mem printers s then raise (KnownPrinter s);
Hstr.replace printers s p
Hstr.replace printers s (DeclByDecl p)
let register_printer_only_flat s p =
if Hstr.mem printers s then raise (KnownPrinter s);
Hstr.replace printers s (OnlyFlat p)
let lookup_printer drv =
let p = match drv.drv_printer with
......@@ -290,7 +303,7 @@ let lookup_printer drv =
with Not_found -> raise (UnknownPrinter p)
let list_printers () =
Hstr.fold (fun k { desc = desc; _ } acc -> (k,desc)::acc) printers []
Hstr.fold (fun k (DeclByDecl { desc = desc; _ } | OnlyFlat { desc_only_flat = desc; _ }) acc -> (k,desc)::acc) printers []
(* exception report *)
......
......@@ -68,9 +68,20 @@ type printer =
interf_printer : interf_printer option;
prelude_printer : prelude_printer; }
type printer_only_flat = {
desc_only_flat : Pp.formatted;
file_gen_only_flat : filename_generator;
decls_printer_only_flat : printer_args -> (Pmodule.pmodule * Mltree.decl) list Pp.pp;
}
type printer_spec =
| OnlyFlat of printer_only_flat
| DeclByDecl of printer
val register_printer : string -> printer -> unit
val register_printer_only_flat : string -> printer_only_flat -> unit
val lookup_printer : driver -> printer_args * printer
val lookup_printer : driver -> printer_args * printer_spec
val list_printers : unit -> (string * Pp.formatted) list
......
(ocamllex lexer)
(menhir (modules parser)
(infer false)
(flags --table)
)
(library
(name why3_parser)
(public_name why3.parser)
(modules
ptree glob typing parser typing lexer
)
(flags -open Why3_util -open Why3_core -open Why3_mlw -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core why3.mlw num menhirLib)
)
(library
(name why3_printer)
(public_name why3.printer)
(modules
cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq
pvs isabelle
simplify gappa cvc3 yices mathematica
)
(flags -open Why3_util -open Why3_core -open Why3_transform -open Why3_mlw -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core why3.transform why3.mlw num)
)
(ocamllex xml strategy_parser)
(library
(name why3_session)
(public_name why3.session)
(modules
compress xml termcode session_itp
strategy strategy_parser controller_itp
server_utils itp_communication
itp_server json_util
)
(libraries why3.util why3.core num why3.transform why3.driver why3.parser
(select compress.ml from
(zip -> compress_z.ml)
( -> compress_none.ml))
)
(flags -open Why3_util -open Why3_core -open Why3_transform -open Why3_driver -open Why3_parser -w A-4-9-41-44-45-50-52@5@8@48)
)
(include_subdirs no)
......@@ -818,29 +818,24 @@ let parse_notification_json j =
with
| Not_found -> raise (NotNotification "<from parse_notification_json>")
let parse_json_object (s: string) =
let lb = Lexing.from_string s in
let x = Json_parser.value (fun x -> Json_lexer.read x) lb in
x
let parse_notification (s: string) : notification =
let json = parse_json_object s in
let json = Json_lexer.parse_json_object s in
parse_notification_json json
let parse_request (s: string) : ide_request =
let json = parse_json_object s in
let json = Json_lexer.parse_json_object s in
parse_request_json json
let parse_list_notification (s: string): notification list =
let json = parse_json_object s in
let json = Json_lexer.parse_json_object s in
match json with
| List [Null] -> []
| List l -> List.map parse_notification_json l
| _ -> raise (NotNotification "Not list")
let parse_list_request (s: string): ide_request list =
let json = parse_json_object s in
let json = Json_lexer.parse_json_object s in
match json with
| List l -> List.map parse_request_json l
| _ -> raise (NotRequest "Not list")
(executables
(public_names why3config why3execute why3extract why3prove why3realize why3wc)
(libraries why3)
(modules why3config why3execute why3extract why3prove why3realize why3wc)
(flags -linkall -open Why3.V1)
(package why3)
)
(executable
(name main)
(public_name why3)
(libraries why3)
(modules main)
(flags -linkall -open Why3.V1)
(package why3)
)
(ocamllex why3wc)
(library
(name why3_unix_scheduler)
(modules unix_scheduler)
(libraries why3)
(flags -linkall -open Why3.V1)
)
(executable
(public_name why3replay)
(libraries why3 why3_unix_scheduler)
(modules why3replay)
(flags -linkall -open Why3.V1 -open Why3_unix_scheduler)
(package why3)
)
(executable
(public_name why3shell)
(modules why3shell)
(libraries why3 why3_unix_scheduler)
(flags -linkall -open Why3.V1 -open Why3_unix_scheduler)
(package why3)
)
......@@ -153,6 +153,10 @@ let print_preludes =
let print_mdecls ?fname m mdecls deps =
let pargs, printer = Pdriver.lookup_printer opt_driver in
let printer = match printer with
| Pdriver.DeclByDecl printer -> printer
| Pdriver.OnlyFlat _ -> invalid_arg "printer can't be used in this mode. Only flat allowed"
in
let fg = printer.Pdriver.file_gen in
let pr = printer.Pdriver.decl_printer in
let test_decl_not_driver decl =
......@@ -387,7 +391,6 @@ let () =
| Flat ->
let mm = Queue.fold flat_extraction Mstr.empty opt_queue in
let (pargs, printer) = Pdriver.lookup_printer opt_driver in
let pr = printer.Pdriver.decl_printer in
let cout = match opt_output with
| None -> stdout
| Some file -> open_out file in
......@@ -409,11 +412,6 @@ let () =
Ident.Mid.iter visit_id tm.Mltree.mod_known;
in
Mstr.iter visit_m mm;
let extract fmt { info_id = id } =
let pm = find_module_id mm id in
let m = translate_module pm in
let d = Ident.Mid.find id m.Mltree.mod_known in
pr pargs ~flat:true pm fmt d in
let idl = List.rev !toextract in
let is_local { info_id = id; info_rec = r } =
let (path, m, _) = Pmodule.restore_path id in
......@@ -421,7 +419,25 @@ let () =
let idl = match opt_rec_single with
| Single -> List.filter is_local idl
| Recursive | RecursiveDeps -> idl in
Pp.print_list Pp.nothing extract fmt idl;
begin match printer with
| Pdriver.DeclByDecl printer ->
let pr = printer.Pdriver.decl_printer in
let extract fmt { info_id = id } =
let pm = find_module_id mm id in
let m = translate_module pm in
let d = Ident.Mid.find id m.Mltree.mod_known in
pr pargs ~flat:true pm fmt d in
Pp.print_list Pp.nothing extract fmt idl
| Pdriver.OnlyFlat printer ->
let pr = printer.Pdriver.decls_printer_only_flat in
let extract { info_id = id } =
let pm = find_module_id mm id in
let m = translate_module pm in
let d = Ident.Mid.find id m.Mltree.mod_known in
pm,d in
let idl = List.map extract idl in
pr pargs fmt idl;
end;
if cout <> stdout then close_out cout
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
......
(library
(name why3_transform)
(public_name why3.transform)
(modules
simplify_formula inlining split_goal
args_wrapper detect_polymorphism reduction_engine compute
eliminate_definition eliminate_algebraic
abstract_quantifiers eliminate_unknown_types
eliminate_unknown_lsymbols eliminate_symbol
eliminate_inductive eliminate_let eliminate_if
libencoding discriminate encoding encoding_select
encoding_guards_full encoding_tags_full
encoding_guards encoding_tags encoding_twin
encoding_sort simplify_array filter_trigger
abstraction close_epsilon lift_epsilon
eliminate_epsilon intro_projections_counterexmp
instantiate_predicate smoke_detector
prop_curry eliminate_literal
generic_arg_trans_utils case apply subst
introduction ind_itp destruct cut congruence
intro_vc_vars_counterexmp prepare_for_counterexmp
induction induction_pr matching reflection
)
(flags -open Why3_util -open Why3_core -open Why3_mlw -open Why3_parser -w A-4-9-41-44-45-50-52@5@8@48)
(libraries why3.util why3.core why3.mlw why3.parser num)
)
......@@ -60,6 +60,7 @@ let max = max_big_int
let abs = abs_big_int
let num_digits = num_digits_big_int
let num_bits = num_bits_big_int
let pow_int_pos = power_int_positive_int
let pow_int_pos_bigint = power_int_positive_big_int
......
......@@ -62,6 +62,7 @@ val abs : t -> t
(** number of digits *)
val num_digits : t -> int
val num_bits : t -> int
(** power of small integers. Second arg must be non-negative *)
val pow_int_pos : int -> int -> t
......
(ocamllex rc lexlib json_lexer)
(menhir (modules json_parser))
(library
(name why3_util)
(public_name why3.util)
(modules
config bigInt util opt lists strings
pp extmap extset exthtbl weakhtbl
hashcons wstdlib exn_printer
json_base json_parser json_lexer
debug loc lexlib print_tree
cmdline warning sysutil rc plugin
number vector pqueue
)
(flags -w A-4-9-41-44-45-50-52@5@8@48)
(libraries num dynlink str unix menhirLib)
)
......@@ -64,3 +64,14 @@ and read_string buf =
}
| _ { raise (SyntaxError ("Illegal string character: " ^ (Buffer.contents buf) ^ Lexing.lexeme lexbuf)) }
| eof { raise (SyntaxError ("String is not terminated")) }
{
let parse_json_object (s: string) =
let lb = Lexing.from_string s in
let x = Json_parser.value (fun x -> read x) lb in
x
}
......@@ -110,6 +110,13 @@ let iteri f l =
in
iter 0 l
let iter_right f l =
let rec iter = function
| [] -> ()
| x :: l -> iter l; f x
in
iter l
let mapi f l =
let rec map i = function
| [] -> []
......
......@@ -62,6 +62,7 @@ val first_nth : ('a -> 'b option) -> 'a list -> int * 'b
val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
val iteri : (int -> 'a -> unit) -> 'a list -> unit
val iter_right : ('a -> unit) -> 'a list -> unit
val fold_lefti : ('a -> int -> 'b -> 'a) -> 'a -> 'b list -> 'a
(** similar to List.map, List.iter and List.fold_left,
but with element index passed as extra argument (in 0..len-1) *)
......
module Why3 = struct
include Why3_util
include Why3_core
include Why3_driver
include Why3_mlw
include Why3_parser
include Why3_transform
include Why3_printer
include Why3_session
end
module Util = Why3_util
module Core = Why3_core
module Driver = Why3_driver
module Mlw = Why3_mlw
module Parser = Why3_parser
module Transform = Why3_transform
module Printer = Why3_printer
module Session = Why3_session
(executable
(public_name why3doc)
(name doc_main)
(modules doc_html doc_def doc_lexer doc_main)
(libraries why3)
(flags -linkall -open Why3.V1)
(package why3)
)
(ocamllex doc_lexer)
(executable
(public_name why3session)
(name why3session_main)
(modules why3session_lib why3session_info
why3session_html why3session_latex why3session_update
why3session_main)
(libraries why3)
(flags -open Why3.V1 -linkall)
(package why3)
)
module Gas
use int.Int
use int.ComputerDivision
use ref.Ref
use mach.int.UInt256
val gas: ref int
val alloc: ref int
val add_gas(g:int) (a:int) : unit
requires { 0 <= g }
requires { 0 <= a }
ensures { !gas = old !gas + g }
ensures { !alloc = old !alloc + a }
writes { gas, alloc }
val get_remaining_gas unit : uint256
reads { gas }
function actual_gas_used (gas:int) (alloc:int) : int =
gas + 3 * alloc + div (alloc*2) 512
end
module ArrayUInt32
use int.Int
use mach.int.UInt32
use seq.Seq
use ref.Ref
use Gas as Gas
type array 'a = private {
mutable ghost elts : seq 'a;
length : uint32;
} invariant { 0 <= length = Seq.length elts }
meta coercion function elts
val ([]) (a: array 'a) (i: uint32) : 'a
requires { [@expl:index in array bounds] 0 <= i < a.length }
ensures { result = a[i] }
val ([]<-) (a: array 'a) (i: uint32) (v: 'a) : unit writes {a}
requires { [@expl:index in array bounds] 0 <= i < a.length }
ensures { a.elts = (old a.elts)[i <- v] }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: array 'a) (i: uint32)
ensures { 0 <= i < a.length }
ensures { result = a[i] }
raises { OutOfBounds -> i < 0 \/ i >= a.length }
= if i < 0 || i >= length a then raise OutOfBounds;
a[i]
let defensive_set (a: array 'a) (i: uint32) (v: 'a)
ensures { 0 <= i < a.length }
ensures { a.elts = (old a.elts)[i <- v] }
raises { OutOfBounds -> (i < 0 \/ i >= a.length) /\ a = old a }
= if i < 0 || i >= length a then raise OutOfBounds;
a[i] <- v
val make (n: uint32) : array 'a
requires { [@expl:array creation size] n >= 0 }
ensures { result.length = n }
ensures { !Gas.alloc = old !Gas.alloc + n }
writes { Gas.alloc }
end
module ArrayUInt64
use int.Int
use mach.int.UInt64
use seq.Seq
use ref.Ref
use Gas as Gas
type array 'a = private {
mutable ghost elts : seq 'a;
length : uint64;
} invariant { 0 <= length = Seq.length elts }
meta coercion function elts
val ([]) (a: array 'a) (i: uint64) : 'a
requires { [@expl:index in array bounds] 0 <= i < a.length }
ensures { result = a[i] }
val ([]<-) (a: array 'a) (i: uint64) (v: 'a) : unit writes {a}
requires { [@expl:index in array bounds] 0 <= i < a.length }
ensures { a.elts = (old a.elts)[i <- v] }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: array 'a) (i: uint64)
ensures { 0 <= i < a.length }
ensures { result = a[i] }
raises { OutOfBounds -> i < 0 \/ i >= a.length }
= if i < 0 || i >= length a then raise OutOfBounds;
a[i]
let defensive_set (a: array 'a) (i: uint64) (v: 'a)
ensures { 0 <= i < a.length }
ensures { a.elts = (old a.elts)[i <- v] }
raises { OutOfBounds -> (i < 0 \/ i >= a.length) /\ a = old a }
= if i < 0 || i >= length a then raise OutOfBounds;
a[i] <- v
val make (n: uint64) : array 'a
requires { [@expl:array creation size] n >= 0 }
ensures { result.length = n }
ensures { !Gas.alloc = old !Gas.alloc + n }
writes { Gas.alloc }
end
......@@ -649,3 +649,106 @@ module UInt64GMP
ensures { to_int result = x }
end
module Int128
use int.Int
type int128 = < range -0x8000_0000_0000_0000_0000_0000_0000_0000
0x7fff_ffff_ffff_ffff_ffff_ffff_ffff_ffff >
let constant min_int128 : int = - 0x8000_0000_0000_0000
let constant max_int128 : int = 0x7fff_ffff_ffff_ffff
function to_int (x : int128) : int = int128'int x
clone export Bounded_int with
type t = int128,
constant min = int128'minInt,
constant max = int128'maxInt,
function to_int = int128'int,
lemma to_int_in_bounds,
lemma extensionality
end
module UInt128Gen
use int.Int
type uint128 = < range 0 0xffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff >
let constant max_uint128 : int = 0xffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff
let constant length : int = 128
let constant radix : int = max_uint128 + 1
function to_int (x : uint128) : int = uint128'int x
end
module UInt128
use export UInt128Gen
clone export Unsigned with
type t = uint128,
constant max = uint128'maxInt,
constant radix = radix,
goal radix_def,
function to_int = uint128'int,
lemma zero_unsigned_is_zero,
lemma to_int_in_bounds,
lemma extensionality
end
module Int256
use int.Int
type int256 = < range -0x8000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000
0x7fff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff >
let constant min_int256 : int = - 0x8000_0000_0000_0000
let constant max_int256 : int = 0x7fff_ffff_ffff_ffff
function to_int (x : int256) : int = int256'int x
clone export Bounded_int with
type t = int256,
constant min = int256'minInt,
constant max = int256'maxInt,
function to_int = int256'int,
lemma to_int_in_bounds,
lemma extensionality
end
module UInt256Gen
use int.Int
type uint256 = < range 0 0xffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff >
let constant max_uint256 : int = 0xffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff
let constant length : int = 256
let constant radix : int = max_uint256 + 1
function to_int (x : uint256) : int = uint256'int x
end
module UInt256
use export UInt256Gen
clone export Unsigned with
type t = uint256,
constant max = uint256'maxInt,
constant radix = radix,
goal radix_def,
function to_int = uint256'int,
lemma zero_unsigned_is_zero,
lemma to_int_in_bounds,
lemma extensionality
end