summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-10-04Merge branch 'cleanup' into experimentsAlasdair Armstrong
2017-10-04Add pretty printing for while loopsAlasdair Armstrong
2017-10-04Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-10-03Fixes to new parserAlasdair Armstrong
2017-10-03Fixed some loop bugs for ASL parserAlasdair Armstrong
2017-09-29Support vector registers (other than bitvectors)Thomas Bauereiss
2017-09-29Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
2017-09-29Some more refactoring of Sail libraryThomas Bauereiss
- Remove start indices and indexing order from bitvector types. Instead add them as arguments to functions accessing/updating bitvectors. These arguments are effectively implicit, thanks to wrappers in prelude_wrappers.sail and a "sizeof" rewriting pass. - Add a typeclass for bitvectors with a few basic functions (converting to/from bitlists, converting to an integer, getting and setting bits). Make both monads use this interface, so that they work with both the bitlist and the machine word representation of bitvectors.
2017-09-29Add MIPS->Isabelle target to MakefileThomas Bauereiss
2017-09-27Add while-loops to Lem backendThomas Bauereiss
2017-09-27Fixed command line flag namingAlasdair Armstrong
2017-09-26Added while-do and repeat-until loops to sail for translating ASLAlasdair Armstrong
2017-09-21Refactored AST valspecs into single constructorAlasdair Armstrong
2017-09-21Remove unused kind_def (KD_) nodes from ASTAlasdair Armstrong
2017-09-21Change NC_fixed to NC_equal to match NC_not_equalAlasdair Armstrong
also rename NC_nat_set_bounded to NC_set (it was an int set not a nat set anyway)
2017-09-21Simplify AST by removing LB_val_explicit and replace LB_val_implicit with ↵Alasdair Armstrong
just LB_val in AST also rename functions in rewriter.ml appropriately.
2017-09-21Cleaning up the AST and removing redundant and/or unused nodesAlasdair Armstrong
2017-09-19Added additional case for tuple l-expressions to increase compatability for ASL.Alasdair Armstrong
2017-09-18Added additional utility functions in ast_utilAlasdair Armstrong
Also fixed basic ocaml test suite
2017-09-14Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-09-14Fix bug in topological sortingThomas Bauereiss
2017-09-14Fix some more test casesThomas Bauereiss
2017-09-14Fix a regression when writing to a register via a reference in a vector such ↵Thomas Bauereiss
as GPR This was wrongly translated as an update of the vector of references.
2017-09-13Fixed code display in error messages that span multiple linesAlasdair Armstrong
2017-09-13Work on improving Sail error messagesAlasdair Armstrong
- Modified how sail type error messages are displayed. The typechecker, rather than immediately outputing a string has a datatype for error types, which are the pretty-printed using a PPrint pretty-printer. Needs more work for all the error messages. - Error messages now attempt to highlight the part of the file where the error occurred, by printing the line the error is on and highlighting where the error message is in red. Again, this needs to be made more robust, especially when the error messages span multiple lines. Other things - Improved new parser and lexer. Made the lexer & parser handling of colons simpler and more intuitive. - Added some more typechecking test cases
2017-09-08Fixed bug when printing Typ_args in Lem AST outputAlasdair Armstrong
2017-09-07Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-09-07Add ocaml run-time and updates to sail for ocaml backendAlasdair Armstrong
2017-09-05Fix printing of negative numbersAlastair Reid
2017-09-02Various fixes for HexapodThomas Bauereiss
- Support tuples in lexps - Rewrite trivial sizeofs - Rewrite early returns more aggressively - Support let bindings with ticked variables (binding both a type-level and term-level variable at the same time)
2017-09-02Remove dependency of state.lem on bitvector operationsThomas Bauereiss
2017-09-02Add command line flags to toggle sequential monad and native machine wordsThomas Bauereiss
2017-09-01Testing typedef generation for ocamlAlasdair Armstrong
2017-09-01Started work on test suite for ocaml backendAlasdair Armstrong
2017-08-30Remove debug print statement from rewriterAlasdair Armstrong
2017-08-30Improved ocaml backend to the point where the hexapod spec produces ↵Alasdair Armstrong
syntactically correct ocaml
2017-08-30Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-08-30Ocaml backend can now run ocamlbuild automatically to build ocamlAlasdair Armstrong
files into runable executable.
2017-08-30Fix another bug in local variable update rewritingThomas Bauereiss
E_internal_let is only used for introducing local variables, not updating existing ones.
2017-08-29Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-08-29More work on ocaml backend.Alasdair Armstrong
Works for basic examples with arbitrary register types, so for example we can compile: val extern string -> unit effect pure print = "print_endline" val unit -> string effect pure hello_world function hello_world () = { return "Hello, World!"; "Unreachable" } val unit -> unit effect {wreg, rreg} main register string REG function main () = { REG := "Hello, Sail!"; print(REG); REG := hello_world (); print(REG); return () } into open Sail_lib;; let zhello_world () = with_return (fun r -> begin r.return "Hello, World!"; "Unreachable" end);; let zREG : (string) ref = ref (undefined_string ());; let zmain () = with_return (fun r -> begin zREG := "Hello, Sail!"; print_endline !zREG; zREG := zhello_world (); print_endline !zREG; r.return () end);; let initialize_registers () = with_return (fun r -> zREG := undefined_string ());; with the arbitrary register types and early returns being handled appropriately, given a suitable implementation for Sail_lib
2017-08-29Make Lem export of CHERI(-256) typecheckThomas Bauereiss
Note: The effect annotations of the execute function differ between CHERI and MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the initial declarations of ast, decode, and execute (with the right effects for MIPS).
2017-08-29Fix bug in rewriting local variable updatesThomas Bauereiss
Don't pull out local variables that are introduced inside a sub-block.
2017-08-29Expand Nexp_id's in sizeof rewriting (e.g. cap_size_t in CHERI)Thomas Bauereiss
Also, rewrite expressions in global let bindings (not only function bodies)
2017-08-29Improve flow typingThomas Bauereiss
Can now handle nexps such as (2**65 - 1). Uses big_ints for comparisons, and keeps original nexps in the AST.
2017-08-28Correct indexing and equality for bitvectorsBrian Campbell
2017-08-24Use relative path in MakefileThomas Bauereiss
2017-08-24Fix some bugs related to the CHERI specThomas Bauereiss
- Correctly pass exponentials to Z3 - Infer types of functional record updates - Support "def Nat"
2017-08-24More work on undefined elimination pass.Alasdair Armstrong
Also generate a function which initializes all the registers in a spec to undefined. This gives us the information we need post-rewriting to generate registers of any arbitrary type.
2017-08-24Add Num identifiers to type environmentThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 20:33:21 +0000