Commit 9111be29 authored by Benedikt Becker's avatar Benedikt Becker

Merge branch 'why3-pp-addendum-11' into 'master'

Why3pp addendum

See merge request !380
parents 11e2f203 e5cd22e9
......@@ -320,9 +320,24 @@ list_stuff () {
}
test_mlw_printer () {
python3 -m sexpdata || return
bench/test_mlw_printer bench/valid/*.mlw
bench/test_mlw_printer bench/typing/good/*.mlw
why3pp="bin/why3pp$suffix"
if ! python3 -m sexpdata 2> /dev/null; then
echo "Skipping (Python module sexpdata not installed)" >&2
return
fi
if ! "$why3pp" --output=sexp <(echo '') > /dev/null 2>&1; then
echo 'Skipping (s-exp output unavailable for why3pp)' >&2
return
fi
find stdlib examples bench -name '*.mlw' \
-not -path '*/\.*' \
-not -path "bench/parsing/bad/*" \
-not -path "bench/programs/bad-to-keep/*" \
-not -path "examples/in_progress/*" |
sort | \
while read filename; do
bench/test_mlw_printer "$why3pp" "$filename" || exit 1
done
}
echo "=== Checking stdlib ==="
......@@ -498,7 +513,7 @@ list_stuff --list-debug-flags
echo ""
echo "=== Checking realizations ==="
exec bench/check_realizations.sh
bench/check_realizations.sh || exit $?
echo "=== Checking mlw_printer ==="
test_mlw_printer
#!/usr/bin/env python3
import sys
import sexpdata
from subprocess import Popen, PIPE
import math
import os
from subprocess import Popen, PIPE, DEVNULL
# Read a whyml file as a s-exp
def read(filename):
p = Popen(["bin/why3pp", "--output=sexp", filename], stdout=PIPE, encoding='utf8')
return sexpdata.loads(''.join(p.stdout.readlines()))
debug = os.environ.get("DEBUG") != None
# Pretty-print a whyml file and read the result as a s-exp
def print_and_read(filename):
p = Popen(["bin/why3pp", "--output=mlw", filename], stdout=PIPE, encoding='utf8')
p1 = Popen(["bin/why3pp", "--output=sexp", "-"], stdin=p.stdout, stdout=PIPE, encoding='utf8')
return sexpdata.loads(''.join(p1.stdout.readlines()))
loads_kwargs = dict(nil=None, true=None) # Don't convert nil or #t in s-exp
class CommandFailed(Exception):
def __init__(self, msg):
self.msg = msg
class NotEqual(Exception):
def __init__(self, path, sexp0, sexp1):
......@@ -20,54 +19,136 @@ class NotEqual(Exception):
self.sexp0 = sexp0
self.sexp1 = sexp1
# Read a whyml file as a s-exp
def read(why3pp, filename):
p = Popen([why3pp, "--output=sexp", filename], stdout=PIPE, stderr=DEVNULL, encoding='utf8')
s, _ = p.communicate()
if p.returncode == 0:
return sexpdata.loads(s, **loads_kwargs) if s else None
else:
raise CommandFailed("cannot print s-expr for original file (returncode={})"
.format(p2.returncode))
# Pretty-print a whyml file and read the result as a s-exp
def print_and_read(why3pp, filename):
p1 = Popen([why3pp, "--output=mlw", filename], stdout=PIPE, stderr=DEVNULL, encoding='utf8')
p2 = Popen([why3pp, "--output=sexp", "-"], stdin=p1.stdout, stdout=PIPE, stderr=DEVNULL, encoding='utf8')
s, _ = p2.communicate()
if p2.returncode == 0:
return sexpdata.loads(s, **loads_kwargs) if s else None
else:
raise CommandFailed("cannot print s-expr for pretty-printed output (returncode={})"
.format(p2.returncode))
def is_location(sexp):
return (type(sexp) == list and
[type(x) for x in sexp] == [str, int, int, int])
try:
return [type(x) for x in sexp] == [str, int, int, int]
except:
return False
def is_annots(sexp, strs):
try:
return len(sexp) == 1 and sexp[0][0].value() == "ATstr" and sexp[0][1][0][1].value() in strs
except AttributeError:
return False
# Test for sexp (<field_name> _)
def is_field(sexp, field_name):
try:
return len(sexp) == 2 and sexp[0].value() == field_name
except:
return False
def assert_equal(path, sexp0, sexp1):
if sexp0 == sexp1:
return
if is_location(sexp0) and is_location(sexp1):
return # Don't bother with locations
elif sexp1 == sexpdata.Symbol("__todo__"):
return # And accept todos
elif type(sexp0) == list and type(sexp1) == list:
for i, (s0, s1) in enumerate(zip(sexp0, sexp1)):
return assert_equal(path+[i], s0, s1)
if is_field(sexp0, "attr_tag") and is_field(sexp1, "attr_tag"):
return # Don't bother with tags
if type(sexp0) == float and math.isnan(sexp0) and type(sexp1) == float and math.isnan(sexp1):
return # nan != nan
if type(sexp0) == list and type(sexp1) == list:
while True: # Ignore additional parentheses
try:
if sexp0[0].value() == "PTparen" and sexp1[0].value() != "PTparen":
path = path+[1]
sexp0 = sexp0[1]
elif sexp1[0].value() == "PTparen" and sexp0[0].value() != "PTparen":
sexp1 = sexp1[1]
elif sexp0[0].value() == "Pparen" and sexp1[0].value() != "Pparen":
path = path+[1]
sexp0 = sexp0[1][0][1]
elif sexp1[0].value() == "Pparen" and sexp0[0].value() != "Pparen":
sexp1 = sexp1[1][0][1]
elif sexp0[0].value() == "Ptuple" and len(sexp0[1]) == 1 and sexp1[0].value() != "Ptuple":
path = path+[1]
sexp0 = sexp0[1][0][1]
elif sexp1[0].value() == "Ptuple" and len(sexp1[1]) == 1 and sexp0[0].value() != "Ptuple":
sexp1 = sexp1[1][0][1]
else:
break
except AttributeError:
break
ignore_annots = [
"W:unused_variable:N", "extraction:array_make", "extraction:array",
"induction", "mlw:reference_var", "infer", "useraxiom", "W:non_conservative_extension:N",
"model_trace:flag", "model_trace:first_val", "model_trace:sec_val", "model_trace:TEMP_NAME",
"model",
]
# Remove annotations that are not generated from the lists
sexp0 = [s for s in sexp0 if is_annots(sexp0, ignore_annots)]
sexp1 = [s for s in sexp1 if is_annots(sexp0, ignore_annots)]
if len(sexp0) > len(sexp1):
if debug:
print(" ", sexpdata.dumps(sexp0))
print(" ", sexpdata.dumps(sexp1))
raise NotEqual(path+[len(sexp1)], sexp0[len(sexp1)], None)
if len(sexp1) > len(sexp0):
if len(sexp0) < len(sexp1):
if debug:
print(" ", sexpdata.dumps(sexp0))
print(" ", sexpdata.dumps(sexp1))
raise NotEqual(path+[len(sexp0)], None, sexp1[len(sexp0)])
elif sexp0 == sexp1:
return
for i, (s0, s1) in enumerate(zip(sexp0, sexp1)):
assert_equal(path+[i], s0, s1)
else:
if debug:
print(" ", sexpdata.dumps(sexp0))
print(" ", sexpdata.dumps(sexp1))
raise NotEqual(path, sexp0, sexp1)
def trace(path, sexp, sexp1):
if path == []:
return [sexpdata.Symbol("EXPECTED"), sexp,
sexpdata.Symbol("FOUND"), sexp1]
return [sexpdata.Symbol("ERROR"),
[sexpdata.Symbol("EXPECTED"), sexp],
[sexpdata.Symbol("FOUND"), sexp1]]
elif type(sexp) == list:
return [trace(path[1:], sexp[i], sexp1)
if i == path[0] else sexp[i]
for i, x in enumerate(sexp)]
return sexp
def test(filename):
sexp0 = read(filename)
def test(why3pp, filename):
print(" {}: ".format(filename), end='', flush=True)
try:
sexp1 = print_and_read(filename)
sexp0 = read(why3pp, filename)
sexp1 = print_and_read(why3pp, filename)
assert_equal([], sexp0, sexp1)
print("OK:", filename)
print("ok")
return True
except AssertionError:
print("CANT REPARSE:", filename)
return False
except NotEqual as e:
print("FAILED:", filename)
# sexpdata.dump(trace(e.path, sexp0, e.sexp1), sys.stdout)
print("FAILED")
if debug:
sexpdata.dump(trace(e.path, sexp0, e.sexp1), sys.stdout)
return False
except CommandFailed as e:
print("COMMAND FAILED:", e.msg)
return False
def main():
res = all(test(f) for f in sys.argv[1:])
why3pp = sys.argv[1]
files = sys.argv[2:]
res = all(test(why3pp, f) for f in files)
exit(0 if res else 1)
if __name__ == "__main__":
......
module M1
use int.Int
goal g: Int.(=) 4 (Int.(+) 2 2)
goal g: Int.( = ) 4 (Int.( + ) 2 2)
end
module M2
......@@ -10,7 +10,7 @@ module M2
let f (x : int)
requires { x = 6 }
ensures { result = 42 } =
Int.(*) x 7
Int.( * ) x 7
end
module M3
......@@ -18,8 +18,8 @@ module M3
use ref.Ref
let f (_ : ())
ensures { Int.(>=) result 0 } =
let x = Ref.ref 42 in Ref.(!) x
ensures { Int.( >= ) result 0 } =
let x = Ref.ref 42 in Ref.( ! ) x
end
module M4
......@@ -27,9 +27,9 @@ module M4
use array.Array
let f (a : Array.array int)
requires { Int.(>=) (Array.length a) 1 }
returns { _ -> (Array.([]) a 0) = 42 } =
Array.([]<-) a 0 42
requires { Int.( >= ) (Array.length a) 1 }
returns { _ -> (Array.( [] ) a 0) = 42 } =
Array.( []<- ) a 0 42
end
Tasks are:
Task 1: theory Task
......
......@@ -3,10 +3,10 @@ module M1
use ref.Refint
let f (x : ref int)
requires { Int.(<=) (Refint.(!) x) 100 }
returns { _ -> (Refint.(!) x) = 100 } =
while Int.(<) (Refint.(!) x) 100 do
variant { Int.(-) 100 (Refint.(!) x) }
requires { Int.( <= ) (Refint.( ! ) x) 100 }
returns { _ -> (Refint.( ! ) x) = 100 } =
while Int.( < ) (Refint.( ! ) x) 100 do
variant { Int.( - ) 100 (Refint.( ! ) x) }
Refint.incr x
done
end
......
This diff is collapsed.
......@@ -500,7 +500,7 @@ let () =
let f = Filename.(chop_extension (basename filename)) in
deps_file std_formatter true f mlw_file
| Sexp, None, 0 ->
Why3pp_sexp.why3pp_sexp mlw_file
Why3pp_sexp.why3pp_sexp stdout mlw_file
| _, _, _ ->
Getopt.handle_exn Sys.argv "invalid arguments"
)
......
let why3pp_sexp _ =
let why3pp_sexp _ _ =
output_string stderr "error: S-expression output unsupported\n";
exit 1
let why3pp_sexp mlw_file =
Why3.Ptree.sexp_of_mlw_file mlw_file |>
Sexplib.Sexp.output_hum_indent 2 stdout
open Format
open Sexplib.Sexp
(* Check if a string contains only characters [a-zA-Z0-9_-] *)
let is_simple_token s =
let rec loop i =
if i < 0 then
true
else match s.[i] with
| 'a'..'z' | 'A'..'Z' | '0'..'9' | '_' | '-' ->
loop (i-1)
| _ -> false in
loop (String.length s-1)
let rec output fmt = function
| Atom s ->
if is_simple_token s then
fprintf fmt "%s" s
else
fprintf fmt "%S" s
| List l ->
let pp_sep fmt () = fprintf fmt "@ " in
fprintf fmt "@[<hv2>(%a)@]" (pp_print_list ~pp_sep output) l
let why3pp_sexp out mlw_file =
let sexp = Why3.Ptree.sexp_of_mlw_file mlw_file in
output (Format.formatter_of_out_channel out) sexp
(* Functions [Sexplib.Sexp.output*] do not escape brackets and quotes in tokens *)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment