aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
ModeNameSize
-rw-r--r--Archi.v2938logstatsplain
-rw-r--r--Asm.v37969logstatsplain
-rw-r--r--AsmToJSON.ml1028logstatsplain
-rw-r--r--Asmaux.v1051logstatsplain
-rw-r--r--Asmblock.v13460logstatsplain
-rw-r--r--Asmblockdeps.v68239logstatsplain
-rw-r--r--Asmblockgen.v45946logstatsplain
-rw-r--r--Asmblockgenproof.v74469logstatsplain
-rw-r--r--Asmblockgenproof0.v31316logstatsplain
-rw-r--r--Asmblockgenproof1.v104270logstatsplain
-rw-r--r--Asmblockprops.v14352logstatsplain
-rw-r--r--Asmexpand.ml24581logstatsplain
-rw-r--r--Asmgen.v2028logstatsplain
-rw-r--r--Asmgenproof.v3920logstatsplain
-rw-r--r--Asmvliw.v66085logstatsplain
l---------BTL_SEsimplify.v27logstatsplain
-rw-r--r--Builtins1.v2475logstatsplain
-rw-r--r--CBuiltins.ml8506logstatsplain
-rw-r--r--CSE2deps.v1626logstatsplain
-rw-r--r--CSE2depsproof.v5049logstatsplain
-rw-r--r--Chunks.v1365logstatsplain
-rw-r--r--CombineOp.v4811logstatsplain
-rw-r--r--CombineOpproof.v6839logstatsplain
-rw-r--r--ConstpropOp.vp12895logstatsplain
-rw-r--r--ConstpropOpproof.v29884logstatsplain
-rw-r--r--Conventions1.v15893logstatsplain
-rw-r--r--DecBoolOps.v1224logstatsplain
-rw-r--r--DuplicateOpcodeHeuristic.ml1613logstatsplain
l---------ExpansionOracle.ml29logstatsplain
-rw-r--r--ExtFloats.v1860logstatsplain
-rw-r--r--ExtValues.v21171logstatsplain
-rw-r--r--FPExtra.v2027logstatsplain
-rw-r--r--Machregs.v9812logstatsplain
-rw-r--r--Machregsaux.ml1388logstatsplain
-rw-r--r--Machregsaux.mli1004logstatsplain
-rw-r--r--NeedOp.v14175logstatsplain
-rw-r--r--Op.v75918logstatsplain
-rw-r--r--OpWeights.ml3858logstatsplain
-rw-r--r--Peephole.v6415logstatsplain
-rw-r--r--PostpassScheduling.v17871logstatsplain
-rw-r--r--PostpassSchedulingOracle.ml40008logstatsplain
-rw-r--r--PostpassSchedulingproof.v24077logstatsplain
l---------PrepassSchedulingOracle.ml37logstatsplain
l---------PrepassSchedulingOracleDeps.ml41logstatsplain
-rw-r--r--PrintOp.ml13210logstatsplain
-rw-r--r--SelectLong.vp17207logstatsplain
-rw-r--r--SelectLongproof.v38256logstatsplain
-rw-r--r--SelectOp.vp27250logstatsplain
-rw-r--r--SelectOpproof.v63486logstatsplain
-rw-r--r--Stacklayout.v6247logstatsplain
-rw-r--r--TargetPrinter.ml36467logstatsplain
-rw-r--r--ValueAOp.v21657logstatsplain
-rwxr-xr-xbitmasks.py314logstatsplain
-rw-r--r--extractionMachdep.v1459logstatsplain
d---------unittest80logstatsplain