sail/test/builtins, branch sail2 Formal specification language for ISAs Add isla builtin testing and update coq script 2021-04-23T16:05:13+00:00 Brian Campbell 2021-04-23T16:05:13+00:00 75af862bbbff6797dd4a5dfa38b4bb617b034ac4 (both off by default) 
(both off by default)
Add flooring division in prelude 2020-04-28T17:43:57+00:00 Alasdair 2020-04-28T17:40:01+00:00 1c1db56b7b34e3ff6293e216872939ce73cd37e6 Defined in terms of tdiv so we don't have to add it to backends that don't already have it 
Defined in terms of tdiv so we don't have to add it to backends that
don't already have it
Fix all remaining tests for this branch 2019-07-16T21:12:42+00:00 Alasdair 2019-07-16T21:12:42+00:00 92f50f2564834fcbeda250337c3acce571f7d6f0 






Implement count_leading_zeros in Lem
2019-06-18T13:39:21+00:00

Thomas Bauereiss

2019-06-18T13:39:21+00:00

65a8bd3e771f5c062c96dbc940b024ec513aeeca












Implement a count_leading_zeros builtin for ocaml and c. This may be a slight performance improvement and keeps compatibility with smt backend that already had a builtin for this because it can't handle the loop in the sail version. Will need implementations for prover backends.
2019-06-17T13:25:01+00:00

Robert Norton

2019-06-17T13:25:01+00:00

2dd28164e40241a2117142fbb197c967740f196d












Add arith_shiftr to C and OCaml libraries
2019-06-06T16:57:25+00:00

Thomas Bauereiss

2019-06-06T14:31:00+00:00

1ad5bb9ea7b4462c0ec07b0f6021f6f228834eb5












Fix bug in slice_mask
2019-05-23T15:39:13+00:00

Thomas Bauereiss

2019-05-23T15:38:58+00:00

fd89347fae1a193911b4dc28a25eb184ce8ab392












Code for testing builtins with Coq
2019-04-16T16:47:36+00:00

Brian Campbell

2019-04-16T16:29:13+00:00

0eadefbfecb80cc4ada16a4a7328ba63b32b166a

Disabled by default because it's fairly resource heavy.
Currently two failures: a minor bug affecting divmod.sail, and undefined
values aren't set up for set_slice_bits.sail.





Disabled by default because it's fairly resource heavy.
Currently two failures: a minor bug affecting divmod.sail, and undefined
values aren't set up for set_slice_bits.sail.







Tidy up of div and mod operators (C implementation was previously inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one.
2019-03-22T16:55:23+00:00

Robert Norton

2019-03-22T16:50:48+00:00

f4acbce30be2aecdfc491478a24c5eb551824f24












Fix some small bugs
2018-12-12T22:40:21+00:00

Alasdair

2018-12-12T22:37:04+00:00

b9a051d186593fdd3bbf295e20f7ace78e668580

Now all ARM, RISC-V, and CHERI-MIPS all build successfully with
type-checking changes. All typechecker/c/ocaml/lem/builtin/riscv/arm
tests are now working as well.

Now the python test scripts can run sequentially with TEST_PAR=1 there's
no reason to keep the old shell versions around anymore.





Now all ARM, RISC-V, and CHERI-MIPS all build successfully with
type-checking changes. All typechecker/c/ocaml/lem/builtin/riscv/arm
tests are now working as well.

Now the python test scripts can run sequentially with TEST_PAR=1 there's
no reason to keep the old shell versions around anymore.