Enable testing of instructions with memory operands in x86_64 simulator

[pennyannn]

Description of changes:
This is a PR following what is done in #186 for enabling testing of instructions with memory operands in x86_64 simulator.

Specifically, cosimulation tests with memory operands are added for the following instructions:

ADD, ADC, OR, SBB, SUB, XOR, MOV, CMOVA, CMOVB, MUL, PUSH and POP

They are tested for two addressing modes: base + scale * index + displacement and base + displacement. The tested operand size is 64 and displacement is disp8. One additional test is added when base register is rsp. They are represented as the following calls in the code:

cosimulate_mem_full_harness([opcode]); (* base + scale * index + displacement *)
cosimulate_mem_base_disp_harness([opcode]); (* base + displacement *)
cosimulate_mem_rsp_harness([opcode]); (* rsp_base + scale * index + displacement *)

To simplify the problem, the register usage is mostly fixed, however the parameters (base, scale, index, and displacement) are randomized. For PUSH and POP, the register usage is also randomized.
These instructions and their respective addressing modes are chosen because they appear in existing s2n-bignum assembly.
The cosimulate_xxx_harness functions are added in file x86-mem-insns.ml for convenience of adding tests for future x86 instruction modeling.

Unlike in Arm, many of the instructions can take memory operands in x86. Therefore I set the cosimulation fraction to be 50% for both non memory-accessing instruction and memory-accessing instruction. The number of tests run in a 40min run is reduced from 2000 to 200, meaning it is now 10 times slower. Reducing the percentage to 10% and around 800 instructions are tested. Some analysis for why this slowdown:

1. The tactics used for the simulation proof is slightly more complex than the ARM version. Specifically, we repeated the use of READ_MEMORY_MERGE_CONV and ASM_REWRITE_TAC[] as in

(if memop then CONV_TAC(ONCE_DEPTH_CONV READ_MEMORY_MERGE_CONV)
   else ALL_TAC) THEN
  ASM_REWRITE_TAC[] THEN extra_simp_tac THEN
  (if memop then CONV_TAC(ONCE_DEPTH_CONV READ_MEMORY_MERGE_CONV)
   else ALL_TAC) THEN
  ASM_REWRITE_TAC[] THEN extra_simp_tac

2. While running conversion over these tests, terms like val (word xxx)) appear in expressions causing proofs to fail. To fix this problem, John (@jargh) proposes adding a tactic EPTH_CONV WORD_NUM_RED_CONV THENC in x86_conv. This change has an impact on all tests
3. Auxiliary instructions are slightly more. For example cosimulate_mem_full_harness function takes five instructions to simulate one

One minor thing, I often find myself having to test if an instruction could be decoded by s2n-bignum, so I wrote this function that currently resides in simulator.ml:

(* A function that decodes a list of bytes into an x86 instruction.
 Could be used for figuring out if an instruction exist in s2n-bignum. *)
let decode_inst ibytes =
  let ibyteterm =
     mk_flist(map (curry mk_comb `word:num->byte` o mk_small_numeral) ibytes) in
  let execth = X86_MK_EXEC_RULE(REFL ibyteterm) in
  let decoded = mk_flist
     (map (rand o rand o snd o strip_forall o concl o Option.get)
       (filter Option.is_some (Array.to_list (snd execth)))) in
  let _ = print_term decoded in
  decoded

I find it really helpful in times, but I'm not sure where to put it. Let me know if it should be moved to somewhere else.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[aqjune-aws]

Hi Yan, in the x86-sematests log the proof states are being printed when ~undefined remains in the conclusion. Do you want to remove this logging? This is useful when wants to briefly look at the Codebuild output and see the checkd instructions trace.