aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
ModeNameSize
-rw-r--r--Archi.v2938logstatsplain
-rw-r--r--Asm.v38743logstatsplain
-rw-r--r--AsmToJSON.ml1028logstatsplain
-rw-r--r--Asmaux.v1051logstatsplain
-rw-r--r--Asmblock.v13460logstatsplain
-rw-r--r--Asmblockdeps.v68367logstatsplain
-rw-r--r--Asmblockgen.v46418logstatsplain
-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.v66719logstatsplain
l---------BTL_SEsimplify.v27logstatsplain
-rw-r--r--Builtins1.v3435logstatsplain
-rw-r--r--CBuiltins.ml8859logstatsplain
-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.v2025logstatsplain
-rw-r--r--ExtIEEE754.v239logstatsplain
-rw-r--r--ExtValues.v23234logstatsplain
-rw-r--r--ExtZ.v239logstatsplain
-rw-r--r--FPDivision32.v20244logstatsplain
-rw-r--r--FPDivision64.v76480logstatsplain
-rw-r--r--Machregs.v9812logstatsplain
-rw-r--r--Machregsaux.ml1388logstatsplain
-rw-r--r--Machregsaux.mli1004logstatsplain
-rw-r--r--NeedOp.v14293logstatsplain
-rw-r--r--Op.v77480logstatsplain
-rw-r--r--OpWeights.ml3858logstatsplain
-rw-r--r--Peephole.v6415logstatsplain
-rw-r--r--PostpassScheduling.v17871logstatsplain
-rw-r--r--PostpassSchedulingOracle.ml40034logstatsplain
-rw-r--r--PostpassSchedulingproof.v24077logstatsplain
l---------PrepassSchedulingOracle.ml37logstatsplain
l---------PrepassSchedulingOracleDeps.ml41logstatsplain
-rw-r--r--PrintOp.ml13210logstatsplain
-rw-r--r--SelectLong.vp17259logstatsplain
-rw-r--r--SelectLongproof.v38556logstatsplain
-rw-r--r--SelectOp.vp27730logstatsplain
-rw-r--r--SelectOpproof.v64969logstatsplain
-rw-r--r--Stacklayout.v6247logstatsplain
-rw-r--r--TargetPrinter.ml36839logstatsplain
-rw-r--r--ValueAOp.v21885logstatsplain
-rwxr-xr-xbitmasks.py314logstatsplain
-rw-r--r--extractionMachdep.v1459logstatsplain
d---------unittest80logstatsplain