summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-09-28Use (K)Bindings from ast_util rather than making new onesBrian Campbell
2017-09-28Add loops to monomorphisationBrian Campbell
2017-09-28Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-09-28Refine constructors during monomorphisationBrian Campbell
2017-09-27Add while-loops to Lem backendThomas Bauereiss
2017-09-26Remove obsolete existential removal codeBrian Campbell
2017-09-26Added while-do and repeat-until loops to sail for translating ASLAlasdair Armstrong
2017-09-26Remove debugging statements included accidentallyBrian Campbell
2017-09-26Add propagation of local assignments to monomorphisationBrian Campbell
2017-09-21Support more functions and vector construction in mono for hexapodBrian Campbell
2017-09-21Substitute into constraints to make assert work with monoBrian Campbell
2017-09-21Disable existential removal for nowBrian Campbell
2017-09-20Handle let (exists 't...[:'t:]) 't = lit in monoBrian Campbell
2017-09-20Remove obsolete nexp refinementBrian Campbell
2017-09-20Support splitting on multiple variables in monoBrian Campbell
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-18Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-09-14Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-09-14Two thirds of monomorphising union types with an existentialBrian Campbell
Still need some way of picking the appropriate constructor
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-04Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵Brian Campbell
mono-experiments
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-28Eta expand lem for OCaml generationBrian Campbell
2017-08-28Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-08-28Correct indexing and equality for bitvectorsBrian Campbell
2017-08-28Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵Brian Campbell
mono-experiments # Conflicts: # src/gen_lib/sail_values.lem
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 03:14:34 +0000