summaryrefslogtreecommitdiff
path: root/mips
AgeCommit message (Collapse)Author
2018-07-09Simplify treating of undefined_bool in Lem libraryThomas Bauereiss
Use nondeterministic choice by default instead of a deterministic bitstream generator in the state, which is slightly awkward to reason about, because every use of undefined_boolS changes the state. The previous behaviour can be implemented as Sail code, if desired. Also add a default implementation of internal_pick that nondeterministically chooses an element from a list.
2018-07-07Coq: bbv have reorganised their repositoryBrian Campbell
2018-07-07Coq: precise generic vectorsBrian Campbell
(probably still some pattern matching to do, but I don't think the models use that)
2018-07-06changes to increase MIPS coverage -- remove optional/unused PREF instruction ↵Robert Norton
and unused cases in ll/sc match
2018-07-05mips: ignore unused functions warnings caused by making some functions static.Robert Norton
2018-07-04mips: move rmem integration instructions into separate file (disabled for ↵Robert Norton
now) to avoid coverage noise.
2018-07-03cheri: refine lwl/lwr cap length checks to be exact. They were previously a ↵Robert Norton
bit loose, but conservative.
2018-07-03mips: just whitespace.Robert Norton
2018-07-03Fill in a few Coq functions for CHERI from the MIPS preludeBrian Campbell
2018-07-02Coq modulus operation that fits the typeBrian Campbell
2018-07-02Coq building rule in MIPS makefileBrian Campbell
2018-06-28Add tagged memory to C rts to cheri can be compiled to CAlasdair Armstrong
2018-06-27Add a mips_c_gcov target that builds mips_c model with coverage reporting.Robert Norton
2018-06-27Add a new function cycle_limit_reached that returns bool, allowing for ↵Robert Norton
graceful exit on reaching cycle limit. This aids coverage and valgrind instrumentation.
2018-06-26mips: fix duplication of cycle_count call that arose due to git merge.Robert Norton
2018-06-26mips: comment out printing of EXCEPTION on every ISA exception.Robert Norton
2018-06-26turn on warnings when compiling mips c then dial back ones that are ↵Robert Norton
triggered by generated code (probably false positives). Fix some warnings in rts.c
2018-06-25Support bitlist representation in Sail2_stringThomas Bauereiss
2018-06-25Coq: add typeclass based comparison, and instantiate for enumsBrian Campbell
2018-06-25Use getopt rather than argp for Mac compatibility in C runtimeAlasdair Armstrong
Also further tweaks to Sail library for C and include sail lib files for tracing
2018-06-25add device tree file for mips.Robert Norton
2018-06-25mips: add optional tracing of register writes (commented out).Robert Norton
2018-06-25Fix bugs in mips ldl/ldr that were probably introduced in porting to sail2.Robert Norton
2018-06-22Fix Lem build of MIPS/CHERIThomas Bauereiss
2018-06-22Add current state of mips_extras.vBrian Campbell
2018-06-22Add bitvector size constraints in MIPSBrian Campbell
2018-06-22Add coq builtins for MIPSBrian Campbell
2018-06-22Add coq generation rule for mipsBrian Campbell
2018-06-22add support for new cycle_limit feature in mips.Robert Norton
2018-06-21Remove loading kernel from mips mainAlasdair Armstrong
2018-06-21Merge branch 'tracing' into sail2Alasdair Armstrong
2018-06-21Fix MIPS wrt changes to C runtimeAlasdair Armstrong
This plus changes to bitfield internals is enough to run some MIPS tests at 1Mhz.
2018-06-18Add bitvector length constraints to mips inequalitiesBrian Campbell
to match new constraints in prelude
2018-06-11More efficient bitfield implementationAlasdair Armstrong
2018-06-08add sail as dependency of mips targets.Robert Norton
2018-06-07Refactor mips main a little to work around apparent bug in c generation. ↵Robert Norton
Generated c Works with no gcc optimisation but fails when optimisation is on, implying undefined behaviour. Probably due to control reaching end of non-void function in exception case.
2018-06-07Use the vector_dec standard library for mips. This means we get all the c ↵Robert Norton
functions ready to go.
2018-06-07add mips_c target.Robert Norton
2018-06-04Add mips.c target in Makefile. Currently triggers assertion failure in ↵Robert Norton
c_backend. still need to merge changes to prelude.sail.
2018-06-04cheri: print debug trace info to stderr to keep it separate from uart output.Robert Norton
2018-05-18mips: add support for CP0 Config0.K0 field because a test has appeared for ↵Robert Norton
it. This concerns cache behaviour of kernel segment k0 but since we dont have a cache we just store the value. It could be relevant to RMEM if we ever want to support kernel mode there.
2018-05-17build fixes: add back tag effect skips required for mips. Move UART check in ↵Robert Norton
to correct place in main.sail. Remove add_atom and sub_atom from prelude as we get them from arith.sail.
2018-05-17changes to for testing FreeBSD boot on MIPS: allowing loading raw file in ↵Robert Norton
ocaml main so that we can have simboot + kernel. Support UART output only.
2018-05-17Refactor main.sailThomas Bauereiss
2018-05-17Remove sequential code againBrian Campbell
2018-05-17Clean up MIPS for HOL4 a littleBrian Campbell
Move mono_rewrites into lib
2018-05-11Add Isabelle code generation for sequential CHERI modelThomas Bauereiss
2018-05-11Merge branch 'sail2' into cheri-monoThomas Bauereiss
In order to use up-to-date sequential CHERI model for test suite
2018-05-11Remove buggy bit list comparison functions from Lem libraryThomas Bauereiss
Found bugs by running CHERI test suite on Isabelle-exported model: signed less-than for bit lists was missing negations for the two's complement, and unsigned less-than compared the reverse lists. Since all other backends implement this in Sail, it seems best to just remove this code. Also add support for infix operators to Lem backend, by z-encoding their identifiers like the other backends do.
2018-05-09remove redundant cloc targets.Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 06:30:47 +0000