https://github.com/EasyCrypt/easycrypt
Revision ba545a9c82d684be976cec846ab5359fabbcd4dd authored by Benjamin Grégoire on 12 June 2018, 05:31:11 UTC, committed by Pierre-Yves Strub on 12 June 2018, 05:34:41 UTC
The tactic statically unroll while loops of the form
x <- int-constant
while (guard) {
body (does not write x);
x <- f(x);
}
where "guard" and "f" can be statically evaluated at each
iteration. The code is then replaced by the while loop
fully unrolled.
The tactic does not terminate if the unrolling leads to
a infinite process.
1 parent 43fd7aa
Tip revision: ba545a9c82d684be976cec846ab5359fabbcd4dd authored by Benjamin Grégoire on 12 June 2018, 05:31:11 UTC
New tactic for static unrolling of "for-loops"
New tactic for static unrolling of "for-loops"
Tip revision: ba545a9
ecBigIntCore.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
module type TheInterface = sig
type zint
exception Overflow
exception InvalidString
val compare : zint -> zint -> int
val equal : zint -> zint -> bool
val sign : zint -> int
val hash : zint -> int
val le : zint -> zint -> bool
val lt : zint -> zint -> bool
val ge : zint -> zint -> bool
val gt : zint -> zint -> bool
val zero : zint
val one : zint
val add : zint -> zint -> zint
val neg : zint -> zint
val sub : zint -> zint -> zint
val mul : zint -> zint -> zint
val div : zint -> zint -> zint
val ediv : zint -> zint -> zint * zint
val erem : zint -> zint -> zint
val gcd : zint -> zint -> zint
val abs : zint -> zint
val pow : zint -> int -> zint
val pred : zint -> zint
val succ : zint -> zint
val parity : zint -> [`Even | `Odd]
val lshift : zint -> int -> zint
val rshift : zint -> int -> zint
val lgand : zint -> zint -> zint
val lgor : zint -> zint -> zint
val lgxor : zint -> zint -> zint
module Notations : sig
val ( =^ ) : zint -> zint -> bool
val ( +^ ) : zint -> zint -> zint
val ( ~^ ) : zint -> zint
val ( -^ ) : zint -> zint -> zint
val ( *^ ) : zint -> zint -> zint
val ( /^ ) : zint -> zint -> zint
val ( <=^ ) : zint -> zint -> bool
val ( <^ ) : zint -> zint -> bool
val ( >=^ ) : zint -> zint -> bool
val ( >^ ) : zint -> zint -> bool
end
val of_int : int -> zint
val to_int : zint -> int
val of_string : string -> zint
val to_string : zint -> string
val pp_print : Format.formatter -> zint -> unit
end
Computing file changes ...
