src/native_client/src/trusted/validator_ragel/movbe_proof.py

   1 # Copyright (c) 2014 The Native Client Authors. All rights reserved.
   2 # Use of this source code is governed by a BSD-style license that can be
   3 # found in the LICENSE file.
   4
   5 """Proof for verifying that 16bit movbe is added to the 32 bit DFA."""
   6
   7 import proof_tools
   8
   9
  10 def Validate(trie_diffs, bitness):
  11   """Validate the trie_diffs adds 16 bit movbe is added in 32bit mode."""
  12
  13   # No instructions should be removed for 32/64 bit DFAs.
  14   # No instructions should be added for 64 bit DFA because it already
  15   # contains 16 bit movbe instructions.
  16   # in 32-bit mode, 16 bit movbe should be added.
  17   # This is of two forms:
  18   #   movbe mem, reg16
  19   #      or
  20   #   movbe reg16, mem
  21   if bitness == 32:
  22     mnemonic = proof_tools.MnemonicOp('movbe')
  23     reg16 = proof_tools.GprOperands(bitness=bitness, operand_size=16)
  24     mem = proof_tools.AllMemoryOperands(bitness=bitness)
  25
  26     expected_adds = (proof_tools.OpsProd(mnemonic, mem, reg16) |
  27                      proof_tools.OpsProd(mnemonic, reg16, mem))
  28   else:
  29     expected_adds = set()
  30
  31   proof_tools.AssertDiffSetEquals(trie_diffs,
  32                                   expected_adds=expected_adds,
  33                                   expected_removes=set())
  34
  35
  36 if __name__ == '__main__':
  37   proof_tools.RunProof(proof_tools.ParseStandardOpts(), Validate)