x86/model: Incorrect handling of string operations in the NullInj contract

[OleksiiOleksenko]

String operations can access multiple memory addresses with some of them triggering a fault and some not. Yet the nullinj-fault contract injects zeros into all of the accesses if at least one of them faults. It leads to contract violations, which could be considered a fault positive.

Minimal test case:

.intel_syntax noprefix
MFENCE # instrumentation
.test_case_enter:

AND RDI, 0b1111111111111 # instrumentation
ADD RDI, R14 # instrumentation
AND RSI, 0b1111111111111 # instrumentation
ADD RSI, R14 # instrumentation
AND RCX, 0xff # instrumentation
ADD RCX, 1 # instrumentation
REPNE MOVSW

AND RAX, 0b1111111111111 # instrumentation
MOV rax, qword ptr [R14 + RAX]

.test_case_exit:
MFENCE # instrumentation

Config:

contract_observation_clause: loads+stores+pc
contract_execution_clause:
    - nullinj-fault

input_gen_entropy_bits: 24
memory_access_zeroed_bits: 0
inputs_per_class: 2

permitted_faults:
    - PF-present

logging_modes:
  - info
  - stat
  - dbg_violation