src/native_client/src/trusted/validator_ragel/xadd16_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 xadd is added to the 32 bit DFA."""
   6
   7 import proof_tools
   8 from proof_tools_templates import LockedRegWithRegOrMem16bit
   9
  10
  11 def Validate(trie_diffs, bitness):
  12   """Validate the trie_diffs adds 16 bit xadd to 32bit mode."""
  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 cmpxchg instruction.
  16   if bitness == 32:
  17     expected_adds = LockedRegWithRegOrMem16bit(mnemonic_name='xadd',
  18                                                bitness=bitness)
  19   else:
  20     expected_adds = set()
  21
  22   proof_tools.AssertDiffSetEquals(trie_diffs,
  23                                   expected_adds=expected_adds,
  24                                   expected_removes=set())
  25
  26
  27 if __name__ == '__main__':
  28   proof_tools.RunProof(proof_tools.ParseStandardOpts(), Validate)