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
| File | Mode | Size |
|---|---|---|
| phl | ||
| system | ||
| ec.ml | -rw-r--r-- | 11.1 KB |
| ecAlgTactic.ml | -rw-r--r-- | 8.5 KB |
| ecAlgTactic.mli | -rw-r--r-- | 1.5 KB |
| ecAlgebra.ml | -rw-r--r-- | 13.7 KB |
| ecAlgebra.mli | -rw-r--r-- | 4.9 KB |
| ecBaseLogic.ml | -rw-r--r-- | 842 bytes |
| ecBigInt.ml | -rw-r--r-- | 4.9 KB |
| ecBigInt.mli | -rw-r--r-- | 390 bytes |
| ecBigIntCore.ml | -rw-r--r-- | 2.0 KB |
| ecCommands.ml | -rw-r--r-- | 29.2 KB |
| ecCommands.mli | -rw-r--r-- | 1.9 KB |
| ecCoreFol.ml | -rw-r--r-- | 52.8 KB |
| ecCoreFol.mli | -rw-r--r-- | 13.7 KB |
| ecCoreGoal.ml | -rw-r--r-- | 35.9 KB |
| ecCoreGoal.mli | -rw-r--r-- | 16.5 KB |
| ecCoreHiPhl.ml | -rw-r--r-- | 2.6 KB |
| ecCoreHiPhl.mli | -rw-r--r-- | 985 bytes |
| ecCoreLib.ml | -rw-r--r-- | 5.9 KB |
| ecCoreLib.mli | -rw-r--r-- | 4.3 KB |
| ecDecl.ml | -rw-r--r-- | 8.6 KB |
| ecDecl.mli | -rw-r--r-- | 4.8 KB |
| ecEnv.ml | -rw-r--r-- | 104.8 KB |
| ecEnv.mli | -rw-r--r-- | 14.5 KB |
| ecField.ml | -rw-r--r-- | 6.3 KB |
| ecField.mli | -rw-r--r-- | 882 bytes |
| ecFol.ml | -rw-r--r-- | 24.3 KB |
| ecFol.mli | -rw-r--r-- | 5.9 KB |
| ecFortune.ml | -rw-r--r-- | 1.8 KB |
| ecFortune.mli | -rw-r--r-- | 488 bytes |
| ecGState.ml | -rw-r--r-- | 3.5 KB |
| ecGState.mli | -rw-r--r-- | 1.6 KB |
| ecGenRegexp.ml | -rw-r--r-- | 10.5 KB |
| ecHiGoal.ml | -rw-r--r-- | 59.0 KB |
| ecHiGoal.mli | -rw-r--r-- | 4.2 KB |
| ecHiInductive.ml | -rw-r--r-- | 12.9 KB |
| ecHiInductive.mli | -rw-r--r-- | 2.3 KB |
| ecHiNotations.ml | -rw-r--r-- | 3.8 KB |
| ecHiNotations.mli | -rw-r--r-- | 1022 bytes |
| ecHiPredicates.ml | -rw-r--r-- | 3.3 KB |
| ecHiPredicates.mli | -rw-r--r-- | 924 bytes |
| ecHiTacticals.ml | -rw-r--r-- | 14.5 KB |
| ecHiTacticals.mli | -rw-r--r-- | 683 bytes |
| ecIdent.ml | -rw-r--r-- | 2.0 KB |
| ecIdent.mli | -rw-r--r-- | 1.5 KB |
| ecInductive.ml | -rw-r--r-- | 9.5 KB |
| ecInductive.mli | -rw-r--r-- | 2.7 KB |
| ecIo.ml | -rw-r--r-- | 6.9 KB |
| ecIo.mli | -rw-r--r-- | 1.3 KB |
| ecLexer.mll | -rw-r--r-- | 18.1 KB |
| ecLoader.ml | -rw-r--r-- | 4.7 KB |
| ecLoader.mli | -rw-r--r-- | 868 bytes |
| ecLocation.ml | -rw-r--r-- | 2.9 KB |
| ecLocation.mli | -rw-r--r-- | 1.6 KB |
| ecLowGoal.ml | -rw-r--r-- | 71.6 KB |
| ecLowGoal.mli | -rw-r--r-- | 10.6 KB |
| ecLowPhlGoal.ml | -rw-r--r-- | 21.6 KB |
| ecMaps.ml | -rw-r--r-- | 4.1 KB |
| ecMatching.ml | -rw-r--r-- | 33.3 KB |
| ecMatching.mli | -rw-r--r-- | 5.9 KB |
| ecMemory.ml | -rw-r--r-- | 3.8 KB |
| ecMemory.mli | -rw-r--r-- | 2.7 KB |
| ecModules.ml | -rw-r--r-- | 20.4 KB |
| ecModules.mli | -rw-r--r-- | 6.8 KB |
| ecOptions.ml | -rw-r--r-- | 13.4 KB |
| ecOptions.mli | -rw-r--r-- | 1.7 KB |
| ecPException.ml | -rw-r--r-- | 1.7 KB |
| ecPException.mli | -rw-r--r-- | 583 bytes |
| ecPV.ml | -rw-r--r-- | 33.4 KB |
| ecPV.mli | -rw-r--r-- | 6.2 KB |
| ecParser.mly | -rw-r--r-- | 82.0 KB |
| ecParsetree.ml | -rw-r--r-- | 29.9 KB |
| ecPath.ml | -rw-r--r-- | 10.9 KB |
| ecPath.mli | -rw-r--r-- | 4.4 KB |
| ecPrinting.ml | -rw-r--r-- | 92.5 KB |
| ecPrinting.mli | -rw-r--r-- | 3.6 KB |
| ecProofTerm.ml | -rw-r--r-- | 29.4 KB |
| ecProofTerm.mli | -rw-r--r-- | 6.2 KB |
| ecProofTyping.ml | -rw-r--r-- | 7.7 KB |
| ecProofTyping.mli | -rw-r--r-- | 3.6 KB |
| ecProvers.ml | -rw-r--r-- | 16.1 KB |
| ecProvers.mli | -rw-r--r-- | 2.1 KB |
| ecReduction.ml | -rw-r--r-- | 27.4 KB |
| ecReduction.mli | -rw-r--r-- | 2.4 KB |
| ecRegexp.ml | -rw-r--r-- | 4.3 KB |
| ecRegexp.mli | -rw-r--r-- | 1.5 KB |
| ecRing.ml | -rw-r--r-- | 13.6 KB |
| ecRing.mli | -rw-r--r-- | 2.4 KB |
| ecScope.ml | -rw-r--r-- | 77.4 KB |
| ecScope.mli | -rw-r--r-- | 7.4 KB |
| ecSearch.ml | -rw-r--r-- | 3.4 KB |
| ecSearch.mli | -rw-r--r-- | 806 bytes |
| ecSection.ml | -rw-r--r-- | 15.0 KB |
| ecSection.mli | -rw-r--r-- | 1.8 KB |
| ecSmt.ml | -rw-r--r-- | 49.2 KB |
| ecSmt.mli | -rw-r--r-- | 1.2 KB |
| ecStrongRing.ml | -rw-r--r-- | 11.0 KB |
| ecSubst.ml | -rw-r--r-- | 20.3 KB |
| ecSubst.mli | -rw-r--r-- | 2.5 KB |
| ecSymbols.ml | -rw-r--r-- | 2.7 KB |
| ecSymbols.mli | -rw-r--r-- | 1.6 KB |
| ecTerminal.ml | -rw-r--r-- | 7.1 KB |
| ecTerminal.mli | -rw-r--r-- | 1.0 KB |
| ecThCloning.ml | -rw-r--r-- | 17.6 KB |
| ecThCloning.mli | -rw-r--r-- | 2.6 KB |
| ecTheory.ml | -rw-r--r-- | 2.9 KB |
| ecTheory.mli | -rw-r--r-- | 2.4 KB |
| ecTheoryReplay.ml | -rw-r--r-- | 21.0 KB |
| ecTheoryReplay.mli | -rw-r--r-- | 2.0 KB |
| ecTransMatching.ml | -rw-r--r-- | 4.1 KB |
| ecTransMatching.mli | -rw-r--r-- | 802 bytes |
| ecTypeClass.ml | -rw-r--r-- | 2.5 KB |
| ecTypeClass.mli | -rw-r--r-- | 841 bytes |
| ecTypes.ml | -rw-r--r-- | 29.1 KB |
| ecTypes.mli | -rw-r--r-- | 8.2 KB |
| ecTyping.ml | -rw-r--r-- | 82.8 KB |
| ecTyping.mli | -rw-r--r-- | 6.8 KB |
| ecUFind.ml | -rw-r--r-- | 5.6 KB |
| ecUFind.mli | -rw-r--r-- | 1.8 KB |
| ecUid.ml | -rw-r--r-- | 2.2 KB |
| ecUid.mli | -rw-r--r-- | 1.2 KB |
| ecUnify.ml | -rw-r--r-- | 14.0 KB |
| ecUnify.mli | -rw-r--r-- | 1.9 KB |
| ecUserMessages.ml | -rw-r--r-- | 24.9 KB |
| ecUserMessages.mli | -rw-r--r-- | 2.5 KB |
| ecUtils.ml | -rw-r--r-- | 20.0 KB |
| ecUtils.mli | -rw-r--r-- | 10.7 KB |
| ecVersion.ml.in | -rw-r--r-- | 801 bytes |
| ecVersion.mli | -rw-r--r-- | 598 bytes |
| ecWhy3Conv.ml | -rw-r--r-- | 6.2 KB |
| ecWhy3Conv.mli | -rw-r--r-- | 645 bytes |
Computing file changes ...
