aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
ModeNameSize
-rw-r--r--Archi.v2938logstatsplain
-rw-r--r--Asm.v39348logstatsplain
-rw-r--r--AsmToJSON.ml1028logstatsplain
-rw-r--r--Asmaux.v1051logstatsplain
-rw-r--r--Asmblock.v13460logstatsplain
-rw-r--r--Asmblockdeps.v68455logstatsplain
-rw-r--r--Asmblockgen.v46929logstatsplain
-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.v67174logstatsplain
l---------BTL_SEsimplify.v27logstatsplain
-rw-r--r--Builtins1.v5643logstatsplain
-rw-r--r--CBuiltins.ml9557logstatsplain
-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.v25563logstatsplain
-rw-r--r--ExtZ.v239logstatsplain
-rw-r--r--FPDivision32.v30645logstatsplain
-rw-r--r--FPDivision64.v85822logstatsplain
-rw-r--r--FPExtra.v4117logstatsplain
-rw-r--r--Machregs.v9812logstatsplain
-rw-r--r--Machregsaux.ml1388logstatsplain
-rw-r--r--Machregsaux.mli1004logstatsplain
-rw-r--r--NeedOp.v14437logstatsplain
-rw-r--r--Op.v78382logstatsplain
-rw-r--r--OpWeights.ml3858logstatsplain
-rw-r--r--Peephole.v6415logstatsplain
-rw-r--r--PostpassScheduling.v17871logstatsplain
-rw-r--r--PostpassSchedulingOracle.ml40186logstatsplain
-rw-r--r--PostpassSchedulingproof.v24077logstatsplain
l---------PrepassSchedulingOracle.ml37logstatsplain
l---------PrepassSchedulingOracleDeps.ml41logstatsplain
-rw-r--r--PrintOp.ml13210logstatsplain
-rw-r--r--SelectLong.vp17280logstatsplain
-rw-r--r--SelectLongproof.v38409logstatsplain
-rw-r--r--SelectOp.vp29182logstatsplain
-rw-r--r--SelectOpproof.v69826logstatsplain
-rw-r--r--Stacklayout.v6247logstatsplain
-rw-r--r--TargetPrinter.ml37256logstatsplain
-rw-r--r--ValueAOp.v22869logstatsplain
-rwxr-xr-xbitmasks.py314logstatsplain
-rw-r--r--extractionMachdep.v1459logstatsplain
d---------unittest80logstatsplain