Code

Aggregated RISCV64 + CI work#8

Code

Draft

mbrcknl wants to merge 206 commits intomasterseL4/graph-refine:masterfrom mbrcknl/ciseL4/graph-refine:mbrcknl/ciCopy head branch name to clipboard

+21,933-13,477

Commits

Commits on Mar 31, 2021

• apply autopep8 E1,W1,W2

  Show description for 1ba08a7
  mbrcknl

  committed
  1ba08a7

• trivial: Use tab for indents in graph-refine.py

  Show description for e21ab29
  

  yyshen

  authored and

  mbrcknl

  committed
  e21ab29

• A checkpoint for adding 64-bit support

  Show description for 6242ab0
  

  yyshen

  authored and

  mbrcknl

  committed
  6242ab0

• A checkpoint for adding 64-bit support

  Show description for ba21539
  

  yyshen

  authored and

  mbrcknl

  committed
  ba21539

• A checkpoint for adding 64-bit support

  Show description for 4d45f05
  

  yyshen

  authored and

  mbrcknl

  committed
  4d45f05

• A checkpoint for adding 64-bit support

  Show description for d9b35dc
  

  yyshen

  authored and

  mbrcknl

  committed
  d9b35dc

• A checkpoint for adding 64-bit support

  Show description for 138f4d0
  

  yyshen

  authored and

  mbrcknl

  committed
  138f4d0

• trivial: Use tab for indents in chronos parser

  Show description for e97f1dc
  

  yyshen

  authored and

  mbrcknl

  committed
  e97f1dc

• Add arch option as input parameter

  Show description for 2189f25
  

  yyshen

  authored and

  mbrcknl

  committed
  2189f25

• Start a parser for RISC-V

  Show description for fa693ec
  

  yyshen

  authored and

  mbrcknl

  committed
  fa693ec

• A checkpoint for RISCV Chronos

  Show description for 5843527
  

  yyshen

  authored and

  mbrcknl

  committed
  5843527

• A checkpoint

  Show description for 04afb61
  

  yyshen

  authored and

  mbrcknl

  committed
  04afb61

• A checkpoint

  Show description for 3628145
  

  yyshen

  authored and

  mbrcknl

  committed
  3628145

• A checkpoint

  Show description for 473606f
  

  yyshen

  authored and

  mbrcknl

  committed
  473606f

• A checkpoint

  Show description for 23a2ad9
  

  yyshen

  authored and

  mbrcknl

  committed
  23a2ad9

• A checkpoint

  Show description for 2f00247
  

  yyshen

  authored and

  mbrcknl

  committed
  2f00247

• Add arch option to elf_parser.py

  Show description for 5c1efc4
  

  yyshen

  authored and

  mbrcknl

  committed
  5c1efc4

• Set the bench_arch early

  Show description for 836cfda
  

  yyshen

  authored and

  mbrcknl

  committed
  836cfda

• Add rv64 elf match string and debug info

  Show description for 3881941
  

  yyshen

  authored and

  mbrcknl

  committed
  3881941

• A checkpoint for rv64 parser

  Show description for 4034401
  

  yyshen

  authored and

  mbrcknl

  committed
  4034401

• Add rv64 emitter

  Show description for 27d7bd8
  

  yyshen

  authored and

  mbrcknl

  committed
  27d7bd8

• Add missing import

  Show description for 6edf034
  

  yyshen

  authored and

  mbrcknl

  committed
  6edf034

• Add more instruction handling

  Show description for 1b4325b
  

  yyshen

  authored and

  mbrcknl

  committed
  1b4325b

• Add test directory for RISCV64

  Show description for 500bd02
  

  yyshen

  authored and

  mbrcknl

  committed
  500bd02

• UPdate test files

  Show description for 7025bd0
  

  yyshen

  authored and

  mbrcknl

  committed
  7025bd0

• A checkpoint for testing code

  Show description for aa895a7
  

  yyshen

  authored and

  mbrcknl

  committed
  aa895a7

• Add more optimisation levels

  Show description for 0ec69b5
  

  yyshen

  authored and

  mbrcknl

  committed
  0ec69b5

• Change test code

  Show description for a19acb8
  

  yyshen

  authored and

  mbrcknl

  committed
  a19acb8

• Copy kernelO1.elf as kernel.elf

  Show description for 61d977f
  

  yyshen

  authored and

  mbrcknl

  committed
  61d977f

• Add test directory for Armv7

  Show description for 08c17b0
  

  yyshen

  authored and

  mbrcknl

  committed
  08c17b0

• Update Armv7 test code

  Show description for 03ebc9a
  

  yyshen

  authored and

  mbrcknl

  committed
  03ebc9a

• A checkpoint

  Show description for e591e16
  

  yyshen

  authored and

  mbrcknl

  committed
  e591e16

• Comment out debug messages

  Show description for 2d1e659
  

  yyshen

  authored and

  mbrcknl

  committed
  2d1e659

• Tweaks for RV64 kernel

  Show description for dcc7327
  

  yyshen

  authored and

  mbrcknl

  committed
  dcc7327

• Support for rv64 assembly instructions

  Show description for 7bf7502
  

  yyshen

  authored and

  mbrcknl

  committed
  7bf7502

• Support RODATA for rv64

  Show description for 943239d
  

  yyshen

  authored and

  mbrcknl

  committed
  943239d

• Enable loading rodata

  Show description for bfd79f7
  

  yyshen

  authored and

  mbrcknl

  committed
  bfd79f7

• Fix sfence.vma

  Show description for 9aed8ed
  

  yyshen

  authored and

  mbrcknl

  committed
  9aed8ed

• Add inline assembly hack and debug

  Show description for 5f6097a
  

  yyshen

  authored and

  mbrcknl

  committed
  5f6097a

• Enable cache and correct offset for RV64

  Show description for 45b0153
  

  yyshen

  authored and

  mbrcknl

  committed
  45b0153

• Add script to check the branch addesses

  Show description for c541a99
  

  yyshen

  authored and

  mbrcknl

  committed
  c541a99

• check_addr.py: output addresses with upper-case hex digits

  Show description for 4dc184e
  mbrcknl

  committed
  4dc184e

• A hack to avoid recomputing stack bounds

  Show description for 2620c67
  

  yyshen

  authored and

  mbrcknl

  committed
  2620c67

• Revert a hack

  Show description for 6a8650a
  

  yyshen

  authored and

  mbrcknl

  committed
  6a8650a

• Add/remove debug messages

  Show description for 8a7087e
  

  yyshen

  authored and

  mbrcknl

  committed
  8a7087e

• Remove debug messages

  Show description for db1c578
  

  yyshen

  authored and

  mbrcknl

  committed
  db1c578

• Use spaces for indent

  Show description for b176029
  

  yyshen

  authored and

  mbrcknl

  committed
  b176029

• Tabs are replaced with spaces

  Show description for 2da0e12
  

  yyshen

  authored and

  mbrcknl

  committed
  2da0e12

• Fix ecall

  Show description for d7d27e3
  

  yyshen

  authored and

  mbrcknl

  committed
  d7d27e3

• Add sbadaddr (the old name for stval) and ebreak

  Show description for 94b8ffb
  

  yyshen

  authored and

  mbrcknl

  committed
  94b8ffb

• restore the assertion

  Show description for 730b6c6
  

  yyshen

  authored and

  mbrcknl

  committed
  730b6c6

• add mk_word16

  Show description for e1df713
  

  yyshen

  authored and

  mbrcknl

  committed
  e1df713

• Import word16T

  Show description for 13f5316
  

  yyshen

  authored and

  mbrcknl

  committed
  13f5316

• Add debug messages

  Show description for 05232de
  

  yyshen

  authored and

  mbrcknl

  committed
  05232de

• Remove debug message

  Show description for 6bd9760
  

  yyshen

  authored and

  mbrcknl

  committed
  6bd9760

• Format preamble

  Show description for 830fb01
  

  yyshen

  authored and

  mbrcknl

  committed
  830fb01

• Add debug message

  Show description for d46ab40
  

  yyshen

  authored and

  mbrcknl

  committed
  d46ab40

• Add debug message

  Show description for 4c70cff
  

  yyshen

  authored and

  mbrcknl

  committed
  4c70cff

• Fix load-rodata for rv64

  Show description for 834892f
  

  yyshen

  authored and

  mbrcknl

  committed
  834892f

• Add debug messages

  Show description for d54b62c
  

  yyshen

  authored and

  mbrcknl

  committed
  d54b62c

• Adjust mod and change 32T to 64T

  Show description for d137a08
  

  yyshen

  authored and

  mbrcknl

  committed
  d137a08

• Add r2 (stack pointer) to callee-saved list

  Show description for 58ce7d3
  

  yyshen

  authored and

  mbrcknl

  committed
  58ce7d3

• StackBounds hack for rv64

  Show description for 21e8745
  

  yyshen

  authored and

  mbrcknl

  committed
  21e8745

• word64T -> syntax.word64T

  Show description for 4a1f6b1
  

  yyshen

  authored and

  mbrcknl

  committed
  4a1f6b1

• Add printouts for understanding the code

  Show description for bf43178
  

  yyshen

  authored and

  mbrcknl

  committed
  bf43178

• Copy SMT file with a relative directory

  Show description for a1e97a7
  

  yyshen

  authored and

  mbrcknl

  committed
  a1e97a7

• Hack to use the Slow solver

  Show description for 841c30c
  

  yyshen

  authored and

  mbrcknl

  committed
  841c30c

• Support for rodata in the SMT file

  Show description for a1fa1d1
  

  yyshen

  authored and

  mbrcknl

  committed
  a1fa1d1

• Add printouts to understand the code

  Show description for 98831f8
  

  yyshen

  authored and

  mbrcknl

  committed
  98831f8

• Implement -include-only argument

  Show description for 93387b4
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  93387b4

• r0 is always 0. writes to r0 do not have effects

  Show description for 5189d29
  

  yyshen

  authored and

  mbrcknl

  committed
  5189d29

• ret_addr_input is r10 for rv64

  Show description for 9506c9d
  

  yyshen

  authored and

  mbrcknl

  committed
  9506c9d

• import syntax in solver.py

  Show description for ede0f44
  

  MitchellBuckley

  authored and

  mbrcknl

  committed
  ede0f44

• hard-code flags in syntax.py for RISCV64

  Show description for 0342d32
  

  MitchellBuckley

  authored and

  mbrcknl

  committed
  0342d32

• Add smt2 for copied SMT files

  Show description for 818f5b3
  

  yyshen

  authored and

  mbrcknl

  committed
  818f5b3

• Fix missing len in logic.py

  Show description for cdb5790
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  cdb5790

• create logs directory

  Show description for a206c2e
  mbrcknl

  committed
  a206c2e

• add script to patch ret_addr_input arguments only

  Show description for 74b9955
  mbrcknl

  committed
  74b9955

• Move check_addr.py to tools directory

  Show description for b116038
  

  yyshen

  authored and

  mbrcknl

  committed
  b116038

• x10 and x11 can be used to return a 128-bit value

  Show description for 1782c1b
  

  yyshen

  authored and

  mbrcknl

  committed
  1782c1b

• Add preliminary support for csrw_sie and csrr_sie instructions

  Show description for 0b46f32
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  0b46f32

• Comment out debug code

  Show description for aa5b5cb
  

  yyshen

  authored and

  mbrcknl

  committed
  aa5b5cb

• x10 and x11 can be used to return a 128-bit value

  Show description for 35fecd9
  

  yyshen

  authored and

  mbrcknl

  committed
  35fecd9

• Implement exit on any exception in syscall argument

  Show description for d307699
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  d307699

• Add preconditions for r10 for large return values

  Show description for 7a190e3
  

  yyshen

  authored and

  mbrcknl

  committed
  7a190e3

• Increase recursion limit to 5000

  Show description for 9538a25
  

  yyshen

  authored and

  mbrcknl

  committed
  9538a25

• Add 'r14' as an input register

  Show description for 809539b
  

  yyshen

  authored and

  mbrcknl

  committed
  809539b

• a script to select functions by simple criteria

  Show description for c1d44be
  mbrcknl

  committed
  c1d44be

• Add make_solverlist.sh.

  Show description for c2cb874
  

  MitchellBuckley

  authored and

  mbrcknl

  committed
  c2cb874

• Fix the sfence.vma inconsistency.

  Show description for da94187
  

  yyshen

  authored and

  mbrcknl

  committed
  da94187

• Add more CSR instructions

  Show description for 25cf9a6
  

  yyshen

  authored and

  mbrcknl

  committed
  25cf9a6

• Add "csrc sstatus"

  Show description for e12cdfc
  

  yyshen

  authored and

  mbrcknl

  committed
  e12cdfc

• 64-bit support for add_pvaild_dom_assertions

  Show description for 12bd7bc
  

  yyshen

  authored and

  mbrcknl

  committed
  12bd7bc

• 64-bit support for loop analysis

  Show description for 27e41be
  

  yyshen

  authored and

  mbrcknl

  committed
  27e41be

• 64-bit for array size limit

  Show description for 126ac01
  

  yyshen

  authored and

  mbrcknl

  committed
  126ac01

• Add r10_input as post eq when ret > 1

  Show description for b8b75f8
  

  yyshen

  authored and

  mbrcknl

  committed
  b8b75f8

• Refactor logging and argument parsing

  Show description for 458b25b
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  458b25b

• Implement report versioning

  Show description for 99ed8e6
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  99ed8e6

• Added excludes.txt

  Show description for 298d887
  

  MitchellBuckley

  authored and

  mbrcknl

  committed
  298d887

• Move 6 functions from excludes.txt to includes.txt

  Show description for e0292bf
  

  MitchellBuckley

  authored and

  mbrcknl

  committed
  e0292bf

• Move excludes.txt so that it sits with includes.txt.

  Show description for 4d0223f
  

  MitchellBuckley

  authored and

  mbrcknl

  committed
  4d0223f

• add a script for generating stack bounds

  Show description for 88f44b7
  mbrcknl

  committed
  88f44b7

• add missing argument to problem.check_no_symbols

  Show description for deb9c17
  mbrcknl

  committed
  deb9c17

• Remove outdated check_addr.py scripts

  Show description for 6b3e97c
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  6b3e97c

• Add submit_report

  Show description for d73988b
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  d73988b

• avoid recomputing stack bounds

  Show description for e1e3153
  mbrcknl

  committed
  e1e3153

• simplify stack_bounds

  Show description for 783edb9
  mbrcknl

  committed
  783edb9

• target-2020-08-10-MCS-jr-fix: find functions with jr

  Show description for 2a4610d
  mbrcknl

  committed
  2a4610d

• riscv: fix ecall instruction spec

  Show description for 342879a
  mbrcknl

  committed
  342879a

• fix riscv64 rodata loader

  Show description for 5636f66
  mbrcknl

  committed
  5636f66

• riscv: add sc.w instruction spec

  Show description for 7978ee9
  mbrcknl

  committed
  7978ee9

• objdump: fix rodata trace messages

  Show description for a6ada8c
  mbrcknl

  committed
  a6ada8c

• riscv: require that gp and tp registers are preserved

  Show description for b2803a7
  mbrcknl

  committed
  b2803a7

• riscv: consolidate some debug tracing

  Show description for a6c2d4f
  mbrcknl

  committed
  a6c2d4f

• riscv fixup: require that gp and tp registers are preserved

  Show description for 52f8595
  mbrcknl

  committed
  52f8595

• riscv: handle 32-bit values in 64-bit registers

  Show description for 64a5d0f
  mbrcknl

  committed
  64a5d0f

• word64: Implement 8-bit config mode for RISC-V

  Show description for 0469824
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  0469824

• word64: Remove hard-coded architecture variables

  Show description for abd9008
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  abd9008

• word64: create Arch class

  Show description for fbcb901
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  fbcb901

• word64: Refactor ghost_assertion_type into Arch

  Show description for 6c7b169
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  6c7b169

• word64: make logic.py architecture-agnostic

  Show description for 9f1f9c9
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  9f1f9c9

• word64: refactor architecture dispatch in stack_logic.py

  Show description for 6bb811f
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  6bb811f

• word64: fix offs_expr_cons default type issue

  Show description for 2e6f5a3
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  2e6f5a3

• word64: make mk_cast part of the architecture specification

  Show description for d10217b
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  d10217b

• word64: remove unused mk_fun_eqs from logic.py

  Show description for 03e2ed3
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  03e2ed3

• word64: Implement architecture-agnostic mk_eqs

  Show description for da6089c
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  da6089c

• word64: make solver.py architecture-agnostic (excl. preambles and rodata)

  Show description for 2703671
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  2703671

• word64: make rodata handling architecture-agnostic

  Show description for f4c70fb
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  f4c70fb

• word64: Move Arch section to end of syntax.py (logical dependency order)

  Show description for b3c7ca6
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  b3c7ca6

• word64: make search.py architecture-agnostic

  Show description for a0adf88
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  a0adf88

• word64: make check.py architecture-agnostic

  Show description for 03dda0c
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  03dda0c

• word64: refactor mem_mode dispatch

  Show description for f99996f
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  f99996f

• word64: remove majority of rv64-specific hacks

  Show description for 63c720e
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  63c720e

• word64: partially implement rv64_native prelude

  Show description for f6351a6
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  f6351a6

• word64: implement rv64_native prelude

  Show description for 597065a
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  597065a

• word64: fix cancelAllIPCs regression

  Show description for 313ce24
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  313ce24

• word64: sanitize import mechanism

  Show description for 9ea9ca6
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  9ea9ca6

• word64: make parts of syntax.py architecture-agnostic

  Show description for e9d9b12
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  e9d9b12

• word64: remove print statements from solver.py

  Show description for b9e83d9
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  b9e83d9

• word64: future-proof zero-wired register check

  Show description for 9803743
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  9803743

• word64: Implement native word16 loads in rv64 SMT prelude

  Show description for c7b9d0b
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  c7b9d0b

• word64: optimize word16-shift implementation

  Show description for feb749d
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  feb749d

• word64: make stack_logic.py architecture-agnostic

  Show description for a1a0840
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  a1a0840

• word64: make cast_pair arch-specific, restore orig. mk_cast behavior

  Show description for 8c90963
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  8c90963

• word64: remove outdated comments about rodata_chunk_type

  Show description for 9b8eee4
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  9b8eee4

• word64: remove hack paving over a long-since-fixed decompiler bug

  Show description for e7f8713
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  e7f8713

• word64: restore uniform token_smt_typ across architectures

  Show description for 74d8e0b
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  74d8e0b

• word64: remove redundant conditional in logic.py

  Show description for 1b7c1a6
  

  Zoltan A. Kocsis

  authored and

  mbrcknl

  committed
  1b7c1a6

• riscv: add rdcycle instruction spec

  Show description for 62e0ce9
  mbrcknl

  committed
  62e0ce9

• riscv: add load-word32 and store-word32 to SMT preamble

  Show description for 8cbf2cf
  mbrcknl

  committed
  8cbf2cf

• solverlist configuration format updates

  Show description for 45c9bca
  mbrcknl

  committed
  45c9bca

• riscv: remove redundant debug trace

  Show description for eb93c14
  mbrcknl

  committed
  eb93c14

• Remove orphan print statements from solver.py and inst_logic.py

  Show description for 18f243a
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  18f243a

• Turn off destructive printing of output in solver.py

  Show description for 3ab7cb6
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  3ab7cb6

• riscv: remove redundant context_trace calls

  Show description for b293392
  mbrcknl

  committed
  b293392

• add solverlist offline-solver configuration option

  Show description for 5c0db72
  mbrcknl

  committed
  5c0db72

• Use hash instead of random temp file names

  Show description for 573b413
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  573b413

• Add filenames to non-parallel outputs

  Show description for 3fe399c
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  3fe399c

• Remove slow_solver_multisat

  Show description for 4903149
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  4903149

• Add filenames to parallel output

  Show description for ebd549e
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  ebd549e

• Make exec_slow_solver writes atomic

  Show description for 83b6e08
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  83b6e08

• Remove saving of SMT examples

  Show description for c20f101
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  c20f101

• Refactor write_solv_script

  Show description for c1d5a77
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  c1d5a77

• remove some unused default arguments

  Show description for 53df601
  mbrcknl

  committed
  53df601

• Add invariant check to VisitCount

  Show description for dab9413
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  dab9413

• Implement __cmp__ for VisitCount

  Show description for 4b283b0
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  4b283b0

• Ensure group keys in proof_check_groups have deterministic order

  Show description for c8f17a8
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  c8f17a8

• riscv: remove some unused default arguments

  Show description for 5007946
  mbrcknl

  committed
  5007946

• Remove dead code from solver.py

  Show description for 6afde59
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  6afde59

• Improve error message on SMT conversation problems

  Show description for 61d06c3
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  61d06c3

• remove reference to undeclared variable

  Show description for c575be0
  mbrcknl

  committed
  c575be0

• Update Makefile to be in line w/ master

  Show description for 1f8ac82
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  1f8ac82

• Update seL4 target Makefile (cleanup, automate manual fix-ups)

  Show description for 5d1c2a0
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  5d1c2a0

• Implement new parallel solver (ParallelTaskManager)

  Show description for 125b161
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  125b161

• Fix comment typos in parallel_solver.py

  Show description for 5169d2f
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  5169d2f

• Improve log messages in parallel_solver.py

  Show description for 2ff9fd2
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  2ff9fd2

• Fix docstring arg list naming in parallel_solver.py

  Show description for 03621f3
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  03621f3

• Remove legacy (unused) classes from parallel task manager

  Show description for 7cbca4e
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  7cbca4e

• Improve model behavior in start_prove_task_with_solver

  Show description for be48977
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  be48977

• Switch to idiomatic return in functions of type (..)->None

  Show description for e8f7037
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  e8f7037

• Apply PEP8 formatting (fixes redundant whitespace)

  Show description for b1029bb
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  b1029bb

• riscv: add stack usage configuration for O2

  Show description for a80fff0
  

  mbrcknl

  and

  Zoltan Kocsis

  committed
  a80fff0

• seL4-example: add arch-specific target.py configurations

  Show description for abc7d43
  mbrcknl

  committed
  abc7d43

• seL4-example: move obsolete scripts

  Show description for e943b0c
  mbrcknl

  committed
  e943b0c

• Implement "run all proofs" shell script

  Show description for 1529b47
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  1529b47

• Add template solverlists for seL4 binary verification

  Show description for c211fbf
  

  Zoltan Kocsis

  authored and

  mbrcknl

  committed
  c211fbf

Commits on Mar 25, 2022

• cleanup: remove obsolete code, rename misc scripts

  Show description for 8b0f482
  mbrcknl

  committed
  8b0f482

• trivial: add missing license headers

  Show description for 0a521a7
  mbrcknl

  committed
  0a521a7

• trivial: fix broken link in README

  Show description for 996ab89
  mbrcknl

  committed
  996ab89

• trivial: fix undefined var

  Show description for 7d760fe
  mbrcknl

  committed
  7d760fe

• add GRAPH_REFINE_SOLVERLIST_DIR env var

  Show description for e553dcb
  mbrcknl

  committed
  e553dcb

• add GRAPH_REFINE_VERSION_INFO env var

  Show description for e25ba2a
  mbrcknl

  committed
  e25ba2a

• log smt problems under specified directory

  Show description for d833f2d
  mbrcknl

  committed
  d833f2d

• add tools for obtaining a decompiler

  Show description for cf83b22
  mbrcknl

  committed
  cf83b22

• add Nix deriviation for graph-refine

  Show description for f91aa1d
  mbrcknl

  committed
  f91aa1d

• ci: build Docker images

  Show description for 7b07fab
  mbrcknl

  committed
  7b07fab

• add shell.nix

  Show description for 342fa75
  mbrcknl

  committed
  342fa75

• stack_bounds: add support more configurations

  Show description for 5159a86
  mbrcknl

  committed
  5159a86

• seL4-example: refresh Makefile

  Show description for af9960c
  mbrcknl

  committed
  af9960c

• add a script for hashing a directory tree

  Show description for 754f0da
  mbrcknl

  committed
  754f0da

• add a script to list functions to be tested

  Show description for a6a5353
  mbrcknl

  committed
  a6a5353

• ci: add scripts to submit graph-refine job

  Show description for 945334a
  mbrcknl

  committed
  945334a

• add a simple parallel job runner

  Show description for da0d97f
  mbrcknl

  committed
  da0d97f

• queue: add basic HTML renderer

  Show description for dfbac8d
  mbrcknl

  committed
  dfbac8d

Commits on Mar 29, 2023

• ci: Various improvements to support scripts

  Show description for 1056cdc
  mbrcknl

  committed
  1056cdc

• ci: Add a web-based view of results

  Show description for d0b2916
  mbrcknl

  committed
  d0b2916