isla 0.2.0

Isla is a symbolic execution engine for Sail instruction set architecture specifications.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

default Order dec

$include <prelude.sail>

val "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)

register R : bits(32)

$property
function prop() -> bool = {
  let x = R | 0xFFFF_0000;
  let y = shift_bits_right(x, 0x10);
  let z = shift_bits_right(x, 0x0000_0010);
  let w = shift_bits_right(x, 0x0000_0000_0000_0010);
  y == 0x0000_FFFF & y == z & y == w
}