...
  View open merge request
Commits (28)
......@@ -204,7 +204,7 @@ LIB_UTIL = config bigInt mlmpfr_wrapper util opt lists strings \
hashcons wstdlib exn_printer \
json_base json_parser json_lexer \
debug loc lexlib print_tree \
cmdline warning sysutil rc plugin bigInt number vector pqueue
cmdline warning sysutil rc plugin bigInt number constant vector pqueue
LIB_CORE = ident ty term pattern decl coercion theory \
task pretty dterm env trans printer model_parser
......
......@@ -11,9 +11,9 @@
</goal>
</theory>
<theory name="A">
<goal name="B.f&#39;VC" expl="VC for f">
<goal name="B.f&#39;vc" expl="VC for f">
</goal>
<goal name="C.f&#39;VC" expl="VC for f">
<goal name="C.f&#39;vc" expl="VC for f">
</goal>
</theory>
</file>
......
......@@ -78,6 +78,9 @@ and syntax = parse
Buffer.clear idx;
Buffer.clear full_kw;
inquote lexbuf }
| '"' '"' {
print_char '"';
syntax lexbuf }
| '"' {
Buffer.clear idx;
Buffer.clear full_kw;
......
......@@ -21,5 +21,17 @@
\
exponent ::= ("e" | "E") ("-" | "+")? digit+
\
h-exponent ::= ("p" | "P") ("-" | "+")? digit+ %
h-exponent ::= ("p" | "P") ("-" | "+")? digit+
\
char ::= "a" - "z" | "A" - "Z" | "0" - "9" ;
| " " | "!" | "#" | "$" | "%" | "&" | "'" | "("
| ")" | "*" | "+" | "," | "-" | "." | "/" | ":" ;
| ";" | "<" | "=" | ">" | "?" | "@" | "[" | "]"
| "^" | "_" | "`" | "\\" | "\n" | "\t" | "\""" ;
| "\" ("0" | "1") digit digit
| "\" "2" ("0" - "5") ("0" - "5") ;
| "\x" hex-digit hex-digit ;
| "\o" ("0" - "3" ) oct-digit oct-digit
\
string ::= ""char*"" %
\end{syntax}
......@@ -20,12 +20,27 @@ and line feed. Blanks separate lexemes but are otherwise ignored.
Comments are enclosed by \texttt{(*} and \texttt{*)} and can be nested.
Note that \texttt{(*)} does not start a comment.
Strings are enclosed in double quotes (\verb!"!). Double quotes can be
escaped inside strings using the backslash character (\verb!\!).
The other special sequences are \verb!\n! for line feed and \verb!\t!
for horizontal tab.
In the following, strings are referred to with the non-terminal
\nonterm{string}{}\spacefalse.
Strings are enclosed in double quotes \texttt{"\ldots"}. The backslash character
\texttt{\textbackslash}, is used for escaping purposes. The following
escape sequences are allowed:
\begin{itemize}
\item \texttt{\textbackslash} followed by a \emph{new line} allows for
multi-line strings. The leading spaces immediately after the new
line are ignored.
\item \texttt{\textbackslash\textbackslash}, \texttt{\textbackslash
\textquotedbl}, and \texttt{\textbackslash \textquotesingle} for the
backslash, double quote, and single quote character.
\item \texttt{\textbackslash n}, \texttt{\textbackslash n}, and
\texttt{\textbackslash t} for the new line feed, carriage return,
and horizontal tab character.
\item \texttt{\textbackslash DDD}, \texttt{\textbackslash oOOO}, and
\texttt{\textbackslash xXX}, where \texttt{DDD} is a decimal value
in the interval \texttt{0-255}, \texttt{OOO} an octal value in the
interval \texttt{0-377}, and \texttt{XX} and hexadecimal value.
Sequences of this form can be used to encode Unicode characters, in
particular non printable \texttt{ASCII} characters.
\item any other escape sequence results in a parsing error.
\end{itemize}
%\subsection{Constants}
The syntax for numerical constants is given by the following rules:
......
This diff is collapsed.
......@@ -21,12 +21,12 @@ transformation "simplify_formula"
theory BuiltIn
prelude "
Require Import ssreflect ssrbool ssrfun ssrnat seq eqtype ssrint.
Require Import ssrint ssrwhy3.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
prelude "\n\
Require Import ssreflect ssrbool ssrfun ssrnat seq eqtype ssrint.\n\
Require Import ssrint ssrwhy3.\n\
Set Implicit Arguments.\n\
Unset Strict Implicit.\n\
Unset Printing Implicit Defensive.\n\
"
syntax type int "int"
......@@ -65,9 +65,9 @@ end
theory int.Int
prelude "
Require Import ssralg ssrnum.
Import GRing.Theory Num.Theory.
prelude "\n\
Require Import ssralg ssrnum.\n\
Import GRing.Theory Num.Theory.\n\
Local Open Scope ring_scope."
syntax function zero "0%:Z"
......
(** Why3 driver for CVC4 >= 1.6 (with floating point support) *)
prelude "(set-info :smt-lib-version 2.6)"
prelude "(set-logic AUFBVFPDTNIRA)"
prelude "(set-logic ALL_SUPPORTED)"
(*
A : Array
UF : Uninterpreted Function
......
......@@ -10,3 +10,26 @@ theory BuiltIn
meta "supports_smt_get_info_unknown_reason" ""
end
theory string.RegExpr
syntax type re "RegLan"
syntax function to_re "(str.to.re %1)"
syntax predicate in_re "(str.in.re %1 %2)"
syntax function concat "(re.++ %1 %2)"
syntax function union "(re.union %1 %2)"
syntax function inter "(re.inter %1 %2)"
syntax function star "(re.* %1)"
syntax function plus "(re.+ %1)"
syntax function none "re.nostr"
syntax function allchar "re.allchar"
syntax function opt "(re.opt %1)"
syntax function range "(re.range %1 %2)"
syntax function power "(re.loop %2 %1 %1)"
syntax function loop "(re.loop %3 %1 %2)"
end
\ No newline at end of file
......@@ -5,6 +5,7 @@ printer "ocaml"
module BuiltIn
syntax type int "Z.t"
syntax type string "string"
end
module HighOrd
......@@ -331,16 +332,16 @@ module mach.onetime.OneTime
syntax val split "(%1-%2, %2)" prec 0 13 13
end
module string.Char
syntax type char "char"
syntax val chr "Char.chr (Z.to_int %1)" prec 4 3
syntax val code "Z.of_int (Char.code %1)" prec 4 3
syntax val uppercase "Char.uppercase %1" prec 4 3
syntax val lowercase "Char.lowercase %1" prec 4 3
end
(* module string.Char *)
(* syntax type char "char" *)
(* syntax val chr "Char.chr (Z.to_int %1)" prec 4 3 *)
(* syntax val code "Z.of_int (Char.code %1)" prec 4 3 *)
(* syntax val uppercase "Char.uppercase %1" prec 4 3 *)
(* syntax val lowercase "Char.lowercase %1" prec 4 3 *)
(* end *)
module io.StdIO
syntax val print_char "Pervasives.print_char %1" prec 4 3
syntax val print_string "Pervasives.print_char %1" prec 4 3
syntax val print_int "Pervasives.print_string (Z.to_string %1)" prec 4 3
syntax val print_newline "Pervasives.print_newline %1" prec 4 3
end
......
......@@ -25,8 +25,10 @@ valid "^unsat$"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax type string "String"
syntax predicate (=) "(= %1 %2)"
meta "literal:keep" type string
meta "encoding:kept" type int
meta "encoding:ignore_polymorphism_ls" predicate (=)
end
......@@ -132,8 +134,8 @@ theory real.FromInt
end
theory real.Truncate
syntax function truncate "(ite (>= %1 0.0)
(to_int %1)
syntax function truncate "(ite (>= %1 0.0) \
(to_int %1) \
(- (to_int (- %1))))"
syntax function floor "(to_int %1)"
syntax function ceil "(- (to_int (- %1)))"
......@@ -196,3 +198,49 @@ theory map.Const
meta "encoding:lskept" function const
(* syntax function const "(const[%t0] %1)" *)
end
theory string.String
prelude ";;; SMT-LIB2: string theory"
syntax function concat "(str.++ %1 %2)"
syntax function length "(str.len %1)"
syntax predicate lt "(str.< %1 %2)"
syntax predicate le "(str.<= %1 %2)"
syntax function indexof "(str.indexof %1 %2 %3)"
syntax function replace "(str.replace %1 %2 %3)"
syntax function replaceall "(str.replaceall %1 %2 %3)"
syntax function substring "(str.substr %1 %2 %3)"
syntax function ([]) "(str.at %1 %2)"
syntax predicate contains "(str.contains %1 %2)"
syntax predicate prefixof "(str.prefixof %1 %2)"
syntax predicate suffixof "(str.suffixof %1 %2)"
(* syntax function is_digit "(str.is_digit %1)" *)
syntax function to_int "(str.to.int %1)"
syntax function from_int "(int.to.str %1)"
end
theory string.StringRealization
prelude ";;; SMT-LIB2: string theory"
syntax function concat "(str.++ %1 %2)"
syntax function length "(str.len %1)"
syntax predicate lt "(str.< %1 %2)"
syntax predicate le "(str.<= %1 %2)"
syntax function indexof "(str.indexof %1 %2 %3)"
syntax function replace "(str.replace %1 %2 %3)"
syntax function replaceall "(str.replaceall %1 %2 %3)"
syntax function substring "(str.substr %1 %2 %3)"
syntax function ([]) "(str.at %1 %2)"
syntax predicate contains "(str.contains %1 %2)"
syntax predicate prefixof "(str.prefixof %1 %2)"
syntax predicate suffixof "(str.suffixof %1 %2)"
(* syntax function is_digit "(str.is_digit %1)" *)
syntax function to_int "(str.to.int %1)"
syntax function from_int "(int.to.str %1)"
end
......@@ -102,3 +102,26 @@ end
theory real.Square
remove allprops
end
theory string.RegExpr
syntax type re "(RegEx String)"
syntax function to_re "(str.to.re %1)"
syntax predicate in_re "(str.in.re %1 %2)"
syntax function concat "(re.++ %1 %2)"
syntax function union "(re.union %1 %2)"
syntax function inter "(re.inter %1 %2)"
syntax function star "(re.* %1)"
syntax function plus "(re.+ %1)"
syntax function none "re.nostr"
syntax function allchar "re.allchar"
syntax function opt "(re.opt %1)"
syntax function range "(re.range %1 %2)"
syntax function power "(re.loop %2 %1 %1)"
syntax function loop "(re.loop %3 %1 %2)"
end
\ No newline at end of file
......@@ -14,12 +14,12 @@ use seq.FreeMonoid
type char
val constant space: char
val function eq (x y: char): bool ensures { result <-> x = y }
type string = seq char
type char_string = seq char
(** The specification uses a function `remove_spaces`.
It is recursively defined over a string, from left to right. *)
let rec function remove_spaces (s: string) : string
let rec function remove_spaces (s: char_string) : char_string
variant { length s }
= if length s = 0 then s
else if eq s[0] space then remove_spaces s[1..]
......@@ -36,7 +36,7 @@ let rec function remove_spaces (s: string) : string
So instead we use an invariant which refers to the *suffixes* of `x`
and `y`. *)
let rec compare_up_to_spaces (x y: string) : bool
let rec compare_up_to_spaces (x y: char_string) : bool
ensures { result <-> remove_spaces x = remove_spaces y }
= let n = length x in
let m = length y in
......
......@@ -29,9 +29,9 @@ module Leftpad
use array.Array
type char (* whatever it is *)
type string = array char
type char_string = array char
let leftpad (pad: char) (n: int) (s: string) : string
let leftpad (pad: char) (n: int) (s: char_string) : char_string
ensures { length result = max n (length s) }
ensures { forall i. 0 <= i < length result - length s -> result[i] = pad }
ensures { forall i. 0 <= i < length s ->
......
......@@ -13,7 +13,7 @@ module M
forall i j:int. n <= i <= m -> n <= j <= m ->
a[i] = a[j] -> i = j
type string
type char_string
(* Capucine memory model *)
......@@ -35,13 +35,13 @@ val new_pointer (_tt:unit) : pointer writes { alloc }
(*
record Student =
name: string;
name: char_string;
mark: int
inv(this) { 0 <= this.mark <= 100 }
end
*)
type student = (string, int)
type student = (char_string, int)
predicate invStudent (this:student) =
let (_,m) = this in 0 <= m <= 100
......@@ -132,7 +132,7 @@ let createCourse (r: (ref (region course))) : pointer
c
(*
fun RegisterStudent(R:[Course], c: [R], name: string): [R.Rstud]
fun RegisterStudent(R:[Course], c: [R], name: char_string): [R.Rstud]
consumes R^c
produces R^c
=
......@@ -147,7 +147,7 @@ fun RegisterStudent(R:[Course], c: [R], name: string): [R.Rstud]
*)
let registerStudent
(r: (ref (region course))) (c:pointer) (name:string) : pointer
(r: (ref (region course))) (c:pointer) (name:char_string) : pointer
requires { valid !alloc c /\ invCourse !alloc !r[c] }
ensures { valid !alloc result }
= let s = new_pointer () in
......
......@@ -6,25 +6,25 @@ module String
type char
constant dummy_char: char
type string = { length: int; chars: int -> char }
type char_string = { length: int; chars: int -> char }
function ([]) (s: string) (i: int) : char = s.chars i
function ([]) (s: char_string) (i: int) : char = s.chars i
constant empty : string = { length = 0; chars = fun (_: int) -> dummy_char }
constant empty : char_string = { length = 0; chars = fun (_: int) -> dummy_char }
val get (s: string) (i:int) : char
val get (s: char_string) (i:int) : char
requires { 0 <= i < s.length }
ensures { result = s.chars i }
function app (s1 s2: string) : string =
function app (s1 s2: char_string) : char_string =
{ length = s1.length + s2.length;
chars = fun i ->
if i < s1.length then s1.chars i else s2.chars (i - s1.length) }
function sub (s: string) (ofs: int) (len: int) : string =
function sub (s: char_string) (ofs: int) (len: int) : char_string =
{ length = len; chars = fun i -> s.chars (i - ofs) }
predicate (==) (s1 s2: string) =
predicate (==) (s1 s2: char_string) =
s1.length = s2.length /\
forall i:int. 0 <= i < s1.length -> s1.chars i = s2.chars i
......
module LadderStringMelseqiQR
(* According to MELSEQ iQ-R programming manual *)
use string.String as S
use int.Int
type astring = String string
| WString string
(** type for MELSEQ iQ-R any_string *)
type aint = int
(** type for MELSEQ iQ-R any_int TODO *)
let function string_of_astring (s: astring) =
match s with
| String s -> s
| WString s -> s
end
meta coercion function string_of_astring
predicate satisfy_size (s: astring) =
match s with
| String s -> S.length s <= 255
| WString s -> S.length s < 128
end
val function length (s: astring) : aint
requires {satisfy_size s}
ensures {result = S.length s}
val function left (s: astring) (x: aint) : astring
requires {satisfy_size s}
requires {0 <= x < S.length s}
ensures {result = S.substring s 0 x}
val function right (s: astring) (x: aint) : astring
requires {satisfy_size s}
requires {0 <= x <= S.length s}
ensures {result = S.substring s (S.length s - x) x}
val function middle (s: astring) (x i: aint) : astring
requires {satisfy_size s}
requires {0 < i <= S.length s}
requires {0 <= x <= S.length s - i + 1}
ensures {result = S.substring s (i-1) x}
val function concat2 (s1 s2: astring) : astring
requires {satisfy_size s1 && satisfy_size s2}
ensures {result = S.substring (S.concat s1 s2) 0 256}
(* TODO check if this actually happens in iQ-R *)
val function concat3 (s1 s2 s3: astring) : astring
requires {satisfy_size s1 && satisfy_size s2 && satisfy_size s3}
ensures {result = S.substring (S.concat (S.concat s1 s2) s3) 0 256}
(* TODO check if this actually happens in iQ-R *)
val function concat4 (s1 s2 s3 s4: astring) : astring
requires {satisfy_size s1 && satisfy_size s2 && satisfy_size s3 &&
satisfy_size s4}
ensures {result = S.substring (S.concat (S.concat s1 s2) (S.concat s3 s4)) 0 256}
(* TODO check if this actually happens in iQ-R *)
val function concat5 (s1 s2 s3 s4 s5: astring) : astring
requires {satisfy_size s1 && satisfy_size s2 && satisfy_size s3 &&
satisfy_size s4 && satisfy_size s5}
ensures {result =
S.substring (S.concat (S.concat s1 s2) (S.concat s3 (S.concat s4 s5))) 0 256}
(* TODO check if this actually happens in iQ-R *)
val function insert (s1: astring) (s2: astring) (i: aint) : astring
requires {satisfy_size s1 && satisfy_size s2}
requires {0 < i <= S.length s1}
requires {length s1 + length s2 < 256}
ensures {result = S.concat (S.concat (S.substring s1 0 i)
s2)
(S.substring s1 i (length s1))}
val function delete (s: astring) (x i: aint) : astring
requires {satisfy_size s}
requires {0 < i < S.length s}
requires {0 <= x <= S.length s - i + 1}
ensures {result = S.concat (S.substring s 0 (i - 1))
(S.substring s (i + x - 1)
(S.length s - i - x + 1))}
val function replace (s1: astring) (s2: astring) (x i: aint) : astring
requires {satisfy_size s1 && satisfy_size s2}
requires {0 < i < S.length s1}
requires {0 <= x <= length s1 - i + 1}
requires {S.length s2 >= x}
(* this is not part of MELSEQ iQ-R manual, but the simulator seems
to have this behavior *)
ensures {result = S.concat (S.concat (S.substring s1 0 i)
(S.substring s2 0 x))
(S.substring s1 (i + x - 1) (S.length s1))}
val function find (s1: astring) (s2: astring) : aint
requires {satisfy_size s1 && satisfy_size s2}
ensures {result = S.indexof s1 s2 0 + 1}
end
(* module LadderString1 (* According to IEC 61131-3 *) *)
(* type char *)
(* type wchar *)
(* type string *)
(* type wstring *)
(* type any_char = Char char *)
(* | WChar wchar *)
(* type any_string = String string *)
(* | WString wstring *)
(* type any_chars = AChar any_char *)
(* | AString any_string *)
(* type any_int *)
(* function len (s: any_string) : any_int *)
(* function left (s: any_string) (i: any_int) : any_string *)
(* function right (s: any_string) (i: any_int) : any_string *)
(* function middle (s: any_string) (i o: any_int) : any_string *)
(* function concat2 (s1 s2: any_chars) : any_string *)
(* function concat3 (s1 s2 s3: any_chars) : any_string *)
(* function concat4 (s1 s2 s3 s4: any_chars) : any_string *)
(* function concat5 (s1 s2 s3 s4 s5: any_chars) : any_string *)
(* function insert (s1: any_string) (s2: any_chars) (i: any_int) : any_string *)
(* function delete (s: any_string) (o i: any_int) : any_string *)
(* function replace (s1: any_string) (s2: any_chars) (o i: any_int) : any_string *)
(* function find (s1: any_string) (s2: any_chars) : any_int *)
(* end *)
(* module LaddeeString2 *)
(* type char *)
(* type wchar *)
(* type string *)
(* type wstring *)
(* function len (s: wstring) : int *)
(* function left (s: wstring) (i: int) : wstring *)
(* function right (s: wstring) (i: int) : wstring *)
(* function middle (s: wstring) (i o: int) : wstring *)
(* function concat2 (s1 s2: wstring) : wstring *)
(* function concat3 (s1 s2 s3: wstring) : wstring *)
(* function concat4 (s1 s2 s3 s4: wstring) : wstring *)
(* function concat5 (s1 s2 s3 s4 s5: wstring) : wstring *)
(* function insert (s1 s2: wstring) (i: int) : wstring *)
(* function delete (s: wstring) (o i: int) : wstring *)
(* function replace (s1 s2: wstring) (o i: int) : wstring *)
(* function find (s1 s2: wstring) : int *)
(* end *)
\ No newline at end of file
module sqrt.Sqrt1
prelude "
#include \"sqrtinit.h\"
uint64_t rsa_estimate (uint64_t a) {
uint64_t abits, x0;
abits = a >> 55;
x0 = 0x100 | invsqrttab[abits - 0x80];
return x0;
}
prelude "\n\
#include \"sqrtinit.h\"\n\
\n\
uint64_t rsa_estimate (uint64_t a) {\n\
uint64_t abits, x0;\n\
abits = a >> 55;\n\
x0 = 0x100 | invsqrttab[abits - 0x80];\n\
return x0;\n\
}\n\
"
end
module powm.Powm
prelude "#include \"binverttab.h\"
uint64_t binvert_limb_table (uint64_t n) {
return (uint64_t)binverttab[n];
}
prelude "#include \"binverttab.h\"\n\
\n\
uint64_t binvert_limb_table (uint64_t n) {\n\
return (uint64_t)binverttab[n];\n\
}\n\
"
end
module mach.int.UInt64GMP
prelude "
typedef unsigned __int128 uint128_t;
struct __mul64_double_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)
{
uint128_t z = (uint128_t)x * (uint128_t)y;
struct __mul64_double_result result = { z, z >> 64 };
return result;
}
uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
{
return (((uint128_t)uh << 64) | ul) / d;
}
prelude "\n\
typedef unsigned __int128 uint128_t;\n\
\n\
struct __mul64_double_result\n\
{ uint64_t __field_0;\n\
uint64_t __field_1;\n\
};\n\
\n\
struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)\n\
{\n\
uint128_t z = (uint128_t)x * (uint128_t)y;\n\
struct __mul64_double_result result = { z, z >> 64 };\n\
return result;\n\
}\n\
\n\
uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)\n\
{\n\
return (((uint128_t)uh << 64) | ul) / d;\n\
}\n\
"
interface "
typedef unsigned __int128 uint128_t;
struct __mul64_double_result
{ uint64_t __field_0;
uint64_t __field_1;
};
static inline struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)
{
uint128_t z = (uint128_t)x * (uint128_t)y;
struct __mul64_double_result result = { z, z >> 64 };
return result;
}
static inline uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
{
return (((uint128_t)uh << 64) | ul) / d;
}
interface "\n\
typedef unsigned __int128 uint128_t;\n\
\n\
struct __mul64_double_result\n\
{ uint64_t __field_0;\n\
uint64_t __field_1;\n\
};\n\
\n\
static inline struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)\n\
{\n\
uint128_t z = (uint128_t)x * (uint128_t)y;\n\
struct __mul64_double_result result = { z, z >> 64 };\n\
return result;\n\
}\n\
\n\
static inline uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)\n\
{\n\
return (((uint128_t)uh << 64) | ul) / d;\n\
}\n\
"
(* "
......@@ -92,107 +92,107 @@ end
module add_alias.AddAlias
prelude "
struct __open_sep_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_rx_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_ry_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_rxy_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_sep_result open_sep (uint64_t * r, uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy)
{
struct __open_sep_result result;
result.__field_0 = r;
result.__field_1 = x;
result.__field_2 = y;
return result;
}
struct __open_rx_result open_rx (uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy)
{
struct __open_sep_result result;
result.__field_0 = x;
result.__field_1 = x;
result.__field_2 = y;
return result;
}
struct __open_ry_result open_ry (uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy)
{
struct __open_sep_result result;
result.__field_0 = y;
result.__field_1 = x;
result.__field_2 = y;
return result;
}
struct __open_rxy_result open_rxy (uint64_t * x, int32_t sx)
{
struct __open_sep_result result;
result.__field_0 = x;
result.__field_1 = x;
result.__field_2 = x;
return result;
}
prelude "\n\
struct __open_sep_result\n\
{ uint64_t *__field_0;\n\
uint64_t *__field_1;\n\
uint64_t *__field_2;\n\
}\n\
\n\
struct __open_rx_result\n\
{ uint64_t *__field_0;\n\
uint64_t *__field_1;\n\
uint64_t *__field_2;\n\
}\n\
\n\
struct __open_ry_result\n\
{ uint64_t *__field_0;\n\
uint64_t *__field_1;\n\
uint64_t *__field_2;\n\
}\n\
\n\
struct __open_rxy_result\n\
{ uint64_t *__field_0;\n\
uint64_t *__field_1;\n\
uint64_t *__field_2;\n\
}\n\
\n\
struct __open_sep_result open_sep (uint64_t * r, uint64_t * x, int32_t sx,\n\
uint64_t * y, int32_t sy)\n\
{\n\
struct __open_sep_result result;\n\
result.__field_0 = r;\n\
result.__field_1 = x;\n\
result.__field_2 = y;\n\
return result;\n\
}\n\
\n\
\n\
struct __open_rx_result open_rx (uint64_t * x, int32_t sx,\n\
uint64_t * y, int32_t sy)\n\
{\n\
struct __open_sep_result result;\n\
result.__field_0 = x;\n\
result.__field_1 = x;\n\
result.__field_2 = y;\n\
return result;\n\
}\n\
\n\
struct __open_ry_result open_ry (uint64_t * x, int32_t sx,\n\
uint64_t * y, int32_t sy)\n\
{\n\
struct __open_sep_result result;\n\
result.__field_0 = y;\n\
result.__field_1 = x;\n\
result.__field_2 = y;\n\
return result;\n\
}\n\
\n\
struct __open_rxy_result open_rxy (uint64_t * x, int32_t sx)\n\
{\n\
struct __open_sep_result result;\n\
result.__field_0 = x;\n\
result.__field_1 = x;\n\
result.__field_2 = x;\n\
return result;\n\
}\n\
"
interface "
struct __open_sep_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_rx_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_ry_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_rxy_result
{ uint64_t *__field_0;
uint64_t *__field_1;
uint64_t *__field_2;
}
struct __open_sep_result open_sep (uint64_t * r, uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy);
struct __open_rx_result open_rx (uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy);
struct __open_ry_result open_ry (uint64_t * x, int32_t sx,
uint64_t * y, int32_t sy);
struct __open_rxy_result open_rxy (uint64_t * x, int32_t sx);
interface "\n\
struct __open_sep_result\n\
{ uint64_t *__field_0;\n\
uint64_t *__field_1;\n\
uint64_t *__field_2;\n\
}\n\
\n\
struct __open_rx_result\n\
{ uint64_t *__field_0;\n\
uint64_t *__field_1;\n\
uint64_t *__field_2;\n\
}\n\
\n\
struct __open_ry_result\n\
{ uint64_t *__field_0;\n\
uint64_t *__field_1;\n\
uint64_t *__field_2;\n\
}\n\
\n\
struct __open_rxy_result\n\
{ uint64_t *__field_0;\n\
uint64_t *__field_1;\n\
uint64_t *__field_2;\n\
}\n\
\n\
struct __open_sep_result open_sep (uint64_t * r, uint64_t * x, int32_t sx,\n\
uint64_t * y, int32_t sy);\n\
\n\
struct __open_rx_result open_rx (uint64_t * x, int32_t sx,\n\
uint64_t * y, int32_t sy);\n\
\n\
struct __open_ry_result open_ry (uint64_t * x, int32_t sx,\n\
uint64_t * y, int32_t sy);\n\
\n\
struct __open_rxy_result open_rxy (uint64_t * x, int32_t sx);\n\
"
syntax val open_sep "open_sep"
......
......@@ -21,60 +21,60 @@ module String
type char
constant dummy_char: char
type string
type char_string
(* axiomatized function length *)
val function length string: int
val function length char_string: int
ensures { 0 <= result }
(* string access routine *)
val function ([]) (s: string) (i:int) : char
val function ([]) (s: char_string) (i:int) : char
requires { 0 <= i < s.length }
val constant empty: string
val constant empty: char_string
ensures { length result = 0 }
(* extensional equality for strings *)
predicate (==) (s1 s2: string) =
predicate (==) (s1 s2: char_string) =
length s1 = length s2 /\
forall i:int. 0 <= i < length s1 -> s1[i] = s2[i]
axiom extensionality:
forall s1 s2: string. s1 == s2 -> s1 = s2
forall s1 s2: char_string. s1 == s2 -> s1 = s2
(* axiomatized concatenation *)
function app string string: string
function app char_string char_string: char_string
axiom app_def1:
forall s1 s2: string. length (app s1 s2) = length s1 + length s2
forall s1 s2: char_string. length (app s1 s2) = length s1 + length s2
axiom app_def2:
forall s1 s2: string, i: int.
forall s1 s2: char_string, i: int.
0 <= i < length s1 -> (app s1 s2)[i] = s1[i]
axiom app_def3:
forall s1 s2: string, i: int.
forall s1 s2: char_string, i: int.
length s1 <= i < length s1 + length s2 ->
(app s1 s2)[i] = s2[i - length s1]
lemma app_assoc:
forall s1 s2 s3: string. app s1 (app s2 s3) == app (app s1 s2) s3
forall s1 s2 s3: char_string. app s1 (app s2 s3) == app (app s1 s2) s3
(* axiomatized substring *)
function sub string int int: string
function sub char_string int int: char_string
axiom sub_def1:
forall s: string, ofs len: int.
forall s: char_string, ofs len: int.
0 <= len -> 0 <= ofs <= length s -> ofs + len <= length s ->
length (sub s ofs len) = len
axiom sub_def2:
forall s: string, ofs len: int.
forall s: char_string, ofs len: int.
0 <= len -> 0 <= ofs <= length s -> ofs + len <= length s ->
forall i: int. 0 <= i < len -> (sub s ofs len)[i] = s[ofs + i]
(* substring routine *)
val sub (s: string) (ofs len: int) : string
val sub (s: char_string) (ofs len: int) : char_string
requires { 0 <= len /\ 0 <= ofs <= length s /\ ofs + len <= length s }
ensures { result = sub s ofs len }
......@@ -89,7 +89,7 @@ module Sig
type rope
function string rope: string
function string rope: char_string
(** a rope is a string *)
function length rope: int
......@@ -100,7 +100,7 @@ module Sig
val is_empty (r: rope) : bool
ensures { result <-> string r == empty }
val of_string (s: string) : rope
val of_string (s: char_string) : rope
requires { 0 <= S.length s }
ensures { string result == s}
......@@ -132,7 +132,7 @@ module Rope (* : Sig *)
(* ***** Logical description of rope type **** *)
type rope =
| Emp
| Str string int int (* Str s ofs len is s[ofs..ofs+len[ *)
| Str char_string int int (* Str s ofs len is s[ofs..ofs+len[ *)
| App rope rope int (* concatenation and total length *)
let function length (r: rope) : int =
......@@ -156,7 +156,7 @@ module Rope (* : Sig *)
end
(* the string model of a rope *)
function string (r: rope) : string = match r with
function string (r: rope) : char_string = match r with
| Emp -> S.empty
| Str s ofs len -> S.sub s ofs len
| App l r _ -> S.app (string l) (string r)
......@@ -181,7 +181,7 @@ module Rope (* : Sig *)
= match r with Emp -> true | _ -> false end
(* string conversion into a rope *)
let of_string (s: string) : rope
let of_string (s: char_string) : rope
requires { 0 <= S.length s }
ensures { string result == s}
ensures { inv result }
......@@ -248,7 +248,7 @@ module Balance
val constant max : int (* e.g. = 100 *)
ensures { 2 <= result }
function string_of_array (q: array rope) (l u: int) : string
function string_of_array (q: array rope) (l u: int) : char_string
(** `q[u-1] + q[u-2] + ... + q[l]` *)
axiom string_of_array_empty:
......@@ -304,7 +304,7 @@ module Balance
ensures { string_of_array q l u == S.empty }
= variant { u - l } if l < u then string_of_array_concat_empty q (l+1) u
function string_of_queue (q: array rope) : string =
function string_of_queue (q: array rope) : char_string =
string_of_array q 2 (Array.length q)
let rec insert (q: array rope) (i: int) (r: rope) : unit
......
module StringCheck
use string.StringRealization as SR
clone string.String
with
function concat = SR.concat,
function length = SR.length,
predicate lt = SR.lt,
predicate le = SR.le,
function ([]) = SR.([]),
function substring = SR.substring,
predicate prefixof = SR.prefixof,
predicate suffixof = SR.suffixof,
predicate contains = SR.contains,
function indexof = SR.indexof,
function replace = SR.replace,
function replaceall = SR.replaceall,
(*predicate is_digit = SR.is_digit,*)
function to_int = SR.to_int,
function from_int = SR.from_int
end
\ No newline at end of file
This diff is collapsed.
module Test
use string.String
use io.StdIO
let main = print_string ("hello world!\n")
end
\ No newline at end of file
module Test
use string.String
goal T0: length "this is a test" = 14
goal T1: length "\x17" = 1
goal T2: length "\o027" = 1
goal T3: length "\t" = 1
goal T4: length "\\" = 1
goal T5: length "\"" = 1
goal T6: length "\n" = 1
(* goal T7: length "\p" = 1 *)
(* goal T9: length "a *)
(* b" = 2 *)
goal T10: length "'" = 1
goal T11: length "/" = 1
goal T12: length "`" = 1
(* à is the same as \195\160 *)
(* goal T13: length "à" = 1 *)
(* goal T14: length "Ϯ" = 1 *)
(* á is the same as \195\161, \o303\o241, \xC3\xA1 *)
(* goal T15: length "á" = 1 *)
goal T16: length "\o303\o241" = 2
goal T17: length "\xC3\xA1" = 2
(* goal T18: length "\o477" = 2 *)
goal T19: length "\xFFA" = 2
goal T20: length "\000" = 2
goal T21: length "\161" = 2
goal T22: length "\r" = 1
goal T23: length "\'" = 1
(* goal T24: length "\256" = 2 *)
goal T25: length "this \
is a \
test" = 14
end
\ No newline at end of file
module TestString
use string.String
use int.Int
goal Empty: "" = ""
goal Empty2: empty = ""
goal Test0: not ("a" = "b")
constant a: string
goal Test1:
(if 2 + 2 = 4 then "a" = a else "b" = a) -> "a" = a
(* this should be proved even with alt-ergo due to the sharing of
literals *)
goal Test2:
let a = if 2 + 2 = 4 then "a" else "" in
let b = if 2 + 2 = 4 then "b" else "" in
not (a = b)
goal Test3:
let a = if 2 + 2 = 4 then "a" else "" in
let b = if 2 + 2 = 4 then "a" else "" in
a = b
goal Test4:
let s = "abcdef" in substring s 2 3 = "cde"
goal TestConcat1:
let s1 = "abc" in
let s2 = "defg" in
concat s1 s2 = "abcdefg"
goal TestConcat5:
concat "" "" = ""
goal TestLength1: length "a" = 1
goal TestLength2: length "ab" = 2
goal TestLength3: length "abc" = 3
goal TestLength4: length (concat "ab" "12") = 4
(* TODO \xC3\xA9 is the encoding of 'é' *)
(* TODO goal TestLength5: length "\xC3\xA9" = 2 *)
goal TestLt1: lt "" "a"
goal TestLt2: lt "a" "b"
goal TestLt3: lt "ab" "b"
goal TestLt4: lt "abcde" "b"
goal TestLt5: lt "a" "1"
goal TestLt6: lt "A" "a"
goal lt_transitive: forall s1 s2 s3. (* CHECK - not proved *)
lt s1 s2 && lt s2 s3 -> lt s1 s3
goal le_transitive: forall s1 s2 s3. (* CHECK - not proved *)
le s1 s2 && le s2 s3 -> le s1 s3
goal TestAt1:
"abc"[3] = empty
goal TestSubstring1:
substring "abcdef" 1 3 = "bcd"
goal TestSubstring2:
substring "abcdef" 1 10 = "bcdef"
goal containsTest1: contains "" ""
goal substring_contains: forall s1 s2.
contains s1 s2 -> exists i. substring s1 i (length s2) = s2
goal TestIndefof1:
indexof "" "" 0 = 0
goal TestIndefof2:
indexof "a" "" 0 = 0
goal TestIndefof3:
indexof "" "a" 0 = -1
goal TestIndefof4:
indexof "a" "" 1 = 1
goal TestIndefof5:
indexof "a" "" 2 = -1
goal TestIndefof6:
indexof "ab" "" 2 = 2
goal TestIndefof7:
indexof "abcdef" "c" 0 = 2
goal TestIndefof8:
indexof "abcdef" "c" 2 = 2
goal TestIndefof9:
indexof "abcdef" "c" 3 = -1
goal TestIndefof10:
indexof "abcdef" "cdef" 0 = 2
goal TestIndexof11: forall s1.
indexof s1 "" 0 = 0
goal TestReplace1: forall s2 s3.
s2 <> "" -> replace "" s2 s3 = ""
goal TestReplace2: forall s1 s3. (* check standard to see if this makes sense *)
replace s1 "" s3 = concat s3 s1
goal TestReplace3:
replace "abcde" "bc" "1234" = "a1234de"
goal TestReplace4:
replace "abcdefg" "fg" "" = "abcde"
goal TestReplace5:
replace "abcdefabcdef" "bc" "123" = "a123defabcdef"
goal TestIsDigit:
is_digit "0" && is_digit "1" && is_digit "2" && is_digit "3" &&
is_digit "4" && is_digit "5" && is_digit "6" && is_digit "7" &&
is_digit "8" && is_digit "9"
goal TestIsDigit2:
not (is_digit "00") && not (is_digit "q") && not (is_digit "-1") &&
not (is_digit "10") && not (is_digit "!") && not (is_digit "\xAA")
goal TestTo_int1: to_int "1" = 1
goal TestTo_int2: to_int "11" = 11
goal TestTo_int3: to_int "123" = 123
goal TestTo_int4: to_int "" = -1
goal TestTo_int5: to_int "a" = -1
goal TestTo_int6: to_int "-1" = -1
goal TestTo_int7: to_int "-2" = -1
goal TestTo_int8: to_int "-11" = -1
goal TestTo_int9: to_int "1a1" = -1
goal TestFrom_int: from_int 1 = "1"
end
module TestRegExpr
use string.String as S
use string.RegExpr
(* in_re and to_re *)
goal TestIn1:
in_re "a" (to_re "a")
goal TestIn2:
in_re "abc" (to_re "abc")
goal TestIn3:
not (in_re "abc" (to_re "abd"))
lemma TestToReInRe: forall s.
in_re s (to_re s)
(* concat *)
goal TestConcat1:
let r1 = to_re "a" in
let r2 = to_re "b" in
in_re "ab" (concat r1 r2)
goal TestConcat2:
let r1 = to_re "a" in
let r2 = to_re "b" in
not (in_re "ba" (concat r1 r2))
goal TestConcat3:
let r1 = to_re "abc" in
let r2 = to_re "def" in
in_re "abcdef" (concat r1 r2)
goal TestConcat4:
let r1 = to_re "a" in
in_re (S.concat "a" "a") (concat r1 r1)
lemma concat: forall s1 s2.
let r1 = to_re s1 in
let r2 = to_re s2 in
in_re (S.concat s1 s2) (concat r1 r2)
goal concat_exists: forall s r1 r2.
in_re s (concat r1 r2) -> exists s1 s2.
S.concat s1 s2 = s && in_re s1 r1 && in_re s2 r2
(* union *)
goal TestUnion1:
let r1 = to_re "a" in
let r2 = to_re "b" in
in_re "a" (union r1 r2) && in_re "b" (union r1 r2)
goal TestUnion2:
let r1 = to_re "a" in
forall re. in_re "a" (union r1 re) && in_re "a" (union re r1)
goal in_union1: forall s1 r1 r2.
in_re s1 r1 -> in_re s1 (union r1 r2)
goal in_union2: forall s1 r1 r2.
in_re s1 r2 -> in_re s1 (union r1 r2)
goal in_union: forall s1 r1 r2.
in_re s1 r1 || in_re s1 r2 -> in_re s1 (union r1 r2)
(* inter *)
goal TestInter1:
let r1 = to_re "a" in
let r2 = to_re "b" in
not (in_re "a" (inter r1 r2))
goal TestInter2:
let r1 = to_re "a" in
let r = to_re "b" in
let r2 = union r1 r in
in_re "a" (inter r1 r2)
lemma in_inter1: forall s1:string, r1:re, r2:re.
in_re s1 (inter r1 r2) -> in_re s1 r1
lemma in_inter2: forall s1:string, r1:re, r2:re.
in_re s1 (inter r1 r2) -> in_re s1 r2
(* star *)
goal TestInStar1:
let a = star (to_re "a") in
in_re "aaa" a &&
not (in_re "aba" a)
goal TestInStar2:
let a = to_re "a" in
let b = to_re "b" in
let ab = star (union a b) in
in_re "a" ab &&
in_re "b" ab &&
in_re "babab" ab &&
in_re "baaa" ab &&
in_re "aaaa" ab &&
in_re "bbbb" ab &&
not (in_re "acaab") ab
goal TestDigit:
let d = union (to_re "0") (union (to_re "1") (union (to_re "2")
(union (to_re "3") (union (to_re "4") (union (to_re "5")
(union (to_re "6") (union (to_re "7") (union (to_re "8")
(to_re "9"))))))))) in
let ds = star d in
let is_digit x = in_re x d in
let are_digits x = in_re x ds in
is_digit "1" && is_digit "9" && is_digit "0" &&
not (is_digit "a") && not (is_digit "12") &&
are_digits "0" && are_digits "4" && are_digits "9" &&
are_digits "1850" && are_digits "10" && are_digits "000" &&
not (are_digits "1 ") && not (are_digits " 1") &&
not (are_digits "1a") && not (are_digits "a1") &&
not (are_digits "a")
goal star1: forall s re.
in_re s re -> in_re s (star re)
lemma star2: forall re.
in_re S.empty (star re)
(* plus *)
goal TestPlus1:
let a = plus (to_re "a") in
in_re "a" a && in_re "aaa" a && not (in_re "b" a) &&
not (in_re "ab" a) && not (in_re "" a)
lemma def_plus: forall re.
plus re = concat re (star re)
goal plus_star: forall s r.
in_re s (plus r) -> in_re s (star r)
(* none, all, allchar *)
goal TestAllChar:
in_re "a" allchar && in_re "1" allchar && in_re "!" allchar &&
not (in_re "aa" allchar) && not (in_re "!!" allchar)
goal TestAll:
in_re "as 3hoiqjndhfgasohn123^*&(T@GIGDSOA" all
lemma allchar: forall s.
S.length s = 1 -> in_re s allchar
lemma in_re_none: forall s: string.
not (in_re s none)
lemma all_allchar: forall s.
in_re s (star allchar)
lemma in_re_all: forall s.
in_re s all
lemma union_all: forall r.
union all r = union r all = all
lemma inter_all: forall r.
inter r all = inter all r = r
lemma star_all: star all = all
(* opt *)
goal TestOpt1:
let a = to_re "a" in
in_re "a" (opt a) && in_re "" (opt a) && not (in_re "ab" (opt a))
lemma empty_opt: forall re.
in_re "" (opt re)
lemma in_opt: forall s.
in_re s (opt (to_re s))
(* range *)
goal TestRange1:
in_re "b" (range "a" "c") &&
in_re "b" (range "b" "c") &&
in_re "b" (range "a" "b") &&
not (in_re "d" (range "a" "c"))
goal TestRange2:
not (in_re "abc" (range "a" "b"))
goal range_negative: forall s.
not (in_re s (range "b" "a"))
goal range_not_singleton: forall s.
not (in_re s (range "ba" "a"))
(* power, loop *)
goal TestPower1:
let a = to_re "a" in
in_re "aa" (power 2 a)
goal TestPower2:
let ab = to_re "ab" in
in_re "ababab" (power 3 ab)
goal TestPower3: forall i.
let ab = to_re "ab" in
in_re "ababab" (power i ab)
goal TestLoop1:
let a = to_re "a" in
in_re "aa" (loop 2 3 a)
end
This diff is collapsed.
......@@ -73,7 +73,7 @@ let d2 =
let body =
(* building expression "ref 42" *)
let e =
let c0 = Expr.e_const (Number.int_const_of_int 42) Ity.ity_int in
let c0 = Expr.e_const (Constant.int_const_of_int 42) Ity.ity_int in
let refzero_type = Ity.ity_app ref_type [Ity.ity_int] [] in
Expr.e_app ref_fun [c0] [] refzero_type
in
......
......@@ -53,7 +53,7 @@ let param0 = [Loc.dummy_position, None, false, Some (PTtuple [])]
let param1 id ty = [Loc.dummy_position, Some id, false, Some ty]
let mk_const i =
Number.(ConstInt { il_kind = ILitDec; il_int = BigInt.of_int i })
Constant.(ConstInt Number.{ il_kind = ILitDec; il_int = BigInt.of_int i })
let mk_tconst i = mk_term (Tconst (mk_const i))
......
......@@ -43,9 +43,10 @@ let mk_ref ~loc e =
let array_set ~loc a i v =
mk_expr ~loc (Eidapp (set_op ~loc, [a; i; v]))
let constant ~loc i =
mk_expr ~loc (Econst (Number.int_const_of_int i))
mk_expr ~loc (Econst (Constant.int_const_of_int i))
let constant_s ~loc s =
mk_expr ~loc (Econst (Number.(ConstInt (int_literal ILitDec ~neg:false s))))
let int_lit = Number.(int_literal ILitDec ~neg:false s) in
mk_expr ~loc (Econst (Constant.ConstInt int_lit))
let break ~loc =
Qident (mk_id ~loc "Break")
let break_handler ~loc =
......
......@@ -423,7 +423,7 @@ term_arg: mk_term(term_arg_) { $1 }
term_arg_:
| ident { Tident (Qident $1) }
| INTEGER { Tconst Number.(ConstInt (int_literal ILitDec ~neg:false $1)) }
| INTEGER { Tconst (Constant.ConstInt Number.(int_literal ILitDec ~neg:false $1)) }
| TRUE { Ttrue }
| FALSE { Tfalse }
| term_sub_ { $1 }
......
......@@ -49,9 +49,10 @@ let mk_ref ~loc e =
let array_set ~loc a i v =
mk_expr ~loc (Eidapp (set_op ~loc, [a; i; v]))
let constant ~loc i =
mk_expr ~loc (Econst (Number.int_const_of_int i))
mk_expr ~loc (Econst (Constant.int_const_of_int i))
let constant_s ~loc s =
mk_expr ~loc (Econst (Number.(ConstInt (int_literal ILitDec ~neg:false s))))
let int_lit = Number.(int_literal ILitDec ~neg:false s) in
mk_expr ~loc (Econst (Constant.ConstInt int_lit))
let len ~loc =
Qident (mk_id ~loc "len")
let break ~loc =
......
......@@ -314,7 +314,7 @@ term_arg: mk_term(term_arg_) { $1 }
term_arg_:
| ident { Tident (Qident $1) }
| INTEGER { Tconst Number.(ConstInt (int_literal ILitDec ~neg:false $1)) }
| INTEGER { Tconst (Constant.ConstInt Number.(int_literal ILitDec ~neg:false $1)) }
| NONE { Ttuple [] }
| TRUE { Ttrue }
| FALSE { Tfalse }
......
......@@ -117,7 +117,7 @@ let number_format_metitarski = {
(fun fmt i n -> fprintf fmt "(%s / %s)" i n));
}
let print_number info fmt c = Number.print (match info.info_num with
let print_number info fmt c = Constant.print (match info.info_num with
| TPTP -> number_format | MetiTarski -> number_format_metitarski) fmt c
let rec print_app info fmt ls tl oty =
......@@ -384,7 +384,7 @@ and print_term info fmt t = match t.t_node with
| Tapp (ls, tl) ->
print_app info fmt ls tl t.t_ty
| Tconst c ->
Number.print number_format fmt c
Constant.print number_format fmt c
| Tlet _ -> unsupportedTerm t
"DFG does not support let, use eliminate_let"
| Tif _ -> unsupportedTerm t
......