summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-09Add some syntactic sugar for IsabelleThomas Bauereiss
2018-07-09Patch some potential uses of uninitialised variables in AArch64Thomas Bauereiss
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-09add riscv_analysis.sail to SAIL_SRCSJon French
2018-07-09add LOADRES, STORECON, AMO to analysisJon French
2018-07-09Bits for bits of aarch64 in coqBrian Campbell
2018-07-09Support writes to misa.C in riscv.Prashanth Mundkur
2018-07-08Make the riscv fetch-execute loop return instead of exiting when done.Prashanth Mundkur
2018-07-08Move the riscv analysis function into its own file for coverage purposes.Prashanth Mundkur
2018-07-08Add a riscv coverage target using bisect-ppx.Prashanth Mundkur
2018-07-08Add -static flag that controls whether generated C functions are staticAlasdair
By default generated functions are non-static, using the -static flag makes them static which is useful for measuring coverage using generated code. Some utility helper functions will always be static, but the compiled versions of sail functions won't be unless this flag is set.
2018-07-07Add reservation traces to riscv tracecmp tool.Prashanth Mundkur
2018-07-07Cancel riscv reservation before i/o scheduling, tweak reservation tracing.Prashanth Mundkur
2018-07-07Add the lrsc tests from riscv-tests.Prashanth Mundkur
2018-07-07An initial fix to riscv lr/sc, needs a review.Prashanth Mundkur
This uses a stronger model than the version in Sail-1 in order to perform address alignment checks. The reservation is kept on virtual addresses, and maintained in the platform model, but now the lr/sc definitions need calls to externs to update this state. An alternative was to reserve physical addresses, but that appeared to be more complicated without a lot more changes. Ideally, the model should be parameterizable over both options.
2018-07-07Add some tracing to riscv address translation.Prashanth Mundkur
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-07Coq: supply index constraint in for loopsBrian Campbell
2018-07-07Coq: eq_range should take proofsBrian Campbell
2018-07-06Coq: support assertions inside and outside of blocksBrian Campbell
2018-07-06Coq: avoid nexp simplification when deciding whether a cast is neededBrian Campbell
2018-07-06Coq: Avoid clashes with the monad name, MBrian Campbell
2018-07-06Coq: feed assertions into the contextBrian Campbell
2018-07-06Coq: use List.In predicates in constraint solving; make other bits robustBrian Campbell
2018-07-06Coq: reduce use of sumbool_of_bool to relevant constraintsBrian Campbell
2018-07-06Coq: missing existential building for rangesBrian Campbell
2018-07-06Coq: turn off partial support for dropping true constraints, fix stringsBrian Campbell
2018-07-06Change HighestSetBit into a form that can be handled by c backend. There are ↵Robert Norton
still a few builtins missing before cheri128 will work.
2018-07-06add gcov option for cheri_c. Add cheri128_c target.Robert Norton
2018-07-06changes to increase MIPS coverage -- remove optional/unused PREF instruction ↵Robert Norton
and unused cases in ll/sc match
2018-07-05Fix printing of aq/rl flags in risc-v lr/sc.Prashanth Mundkur
2018-07-05Fix equality comparisons for variants in CAlasdair
Makes sure equality comparisons for variants are compiled correctly. Needed for CHERI and mips, which have structs containing variants. Also make sure that struct equality works for structs containing other structs.
2018-07-05Coq: get index_list rightBrian Campbell
2018-07-05Fix equality comparisons for structsAlasdair
Add a test case in test/c/eq_struct.sail. Ensure that the macro EQUAL(type) will always give a valid equality function for any builtin type in sail.h.
2018-07-05Fix CHERI test that was failing when compiled to CAlasdair Armstrong
Non bitvector literals for decreasing vectors were not being reversed correctly, so the list of capability registers was effectively in reverse order. Added a test case to test/c/ based on this aspect of CHERI
2018-07-05mips: ignore unused functions warnings caused by making some functions static.Robert Norton
2018-07-05make many generated c functions static -- this gives the compiler a chance ↵Robert Norton
to notice if they are dead or inline them if appropriate, cleaning up coverage reports and potentially improving execution speed.
2018-07-05support acquire/release loads/stores in RISCV initial_analysisJon French
2018-07-05print to stdout not stderr to stop upsetting rmem regression testsJon French
2018-07-05restore missing RISC-V fence types in sail2; ignore io bits in fences more ↵Jon French
cleanly
2018-07-04mips: move rmem integration instructions into separate file (disabled for ↵Robert Norton
now) to avoid coverage noise.
2018-07-04AArch64 Prelude: Move cycle count primop to preludeAlastair Reid
2018-07-03Add htif tohost to the riscv tracecmp tool.Prashanth Mundkur
2018-07-03Allow the riscv htif_tohost mmio port to be readable, and ack writes to that ↵Prashanth Mundkur
port.
2018-07-03Fix a bug in foreach loopsAlasdair Armstrong
We should test before the first iteration in case 'to' starts out as less than 'from'.
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-03Fix letbind_effects on LEXP_deref with an effectful subexpressionBrian Campbell
2018-07-03Fill in a few Coq functions for CHERI from the MIPS preludeBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 20:22:01 +0000