sail/aarch64, branch sail2 Formal specification language for ISAs Update 8.3 readme to point to 8.5 sail-arm 2020-07-31T12:38:10+00:00 Alasdair Armstrong 2020-07-31T12:38:10+00:00 8f64b7b5aaa411d2866b78e6e9b0cf504d2043ec 






Fix all remaining tests for this branch
2019-07-16T21:12:42+00:00

Alasdair

2019-07-16T21:12:42+00:00

92f50f2564834fcbeda250337c3acce571f7d6f0












Fix some broken interpreter tests
2019-04-26T16:20:20+00:00

Alasdair Armstrong

2019-04-26T16:20:20+00:00

094c8e254abde44d45097aca7a36203704fe2ef4












AArch64: Update write_mem_val to write_mem
2019-04-04T22:53:32+00:00

Alasdair

2019-04-04T22:52:17+00:00

8dca40d218b5fbc0956b29887d9c1065b1c1757f












Tidy up of div and mod operators (C implementation was previously inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one.
2019-03-22T16:55:23+00:00

Robert Norton

2019-03-22T16:50:48+00:00

f4acbce30be2aecdfc491478a24c5eb551824f24












Fix implicits in v8.2 public ARM spec
2019-02-07T15:06:05+00:00

Alasdair Armstrong

2019-02-07T15:06:05+00:00

a0798a777d800f6255a1370806435a51d418a249












Avoid unification on ambiguous return types
2019-02-02T01:31:20+00:00

Alasdair

2019-02-02T01:22:39+00:00

ebfed17b57993f034d1a334014a8b9c9a542c0d5

Usually we want to unify on return types, but in the case of
constraint unification (especially during rewriting) we can find
ourselves in the situation where unifying too eagerly on a return
type like bool('p & 'q) can cause us to instantiate 'p and 'q in the
wrong order (as & should really respect commutativity and
associativity during typechecking to avoid being overly brittle).

Originally I simply avoided adding cases for unify on NC_and/NC_or
and similar to avoid these cases, but this lead to the undesirable
situation where identical types wouldn't unify with each other for
an empty set of goals, which should be a trivial property of the
unification functions.

The solution is therefore to identify type variables in ambiguous
positions, and remove them from the list of goals during
unification. All type variables still have to be resolved by the
time we finish checking each application, but this has the added
bonus of making order much less important when it comes to
instantiating type variables.

Currently I am overly conservative about what qualifies as
ambigious, but this set should be expanded





Usually we want to unify on return types, but in the case of
constraint unification (especially during rewriting) we can find
ourselves in the situation where unifying too eagerly on a return
type like bool('p & 'q) can cause us to instantiate 'p and 'q in the
wrong order (as & should really respect commutativity and
associativity during typechecking to avoid being overly brittle).

Originally I simply avoided adding cases for unify on NC_and/NC_or
and similar to avoid these cases, but this lead to the undesirable
situation where identical types wouldn't unify with each other for
an empty set of goals, which should be a trivial property of the
unification functions.

The solution is therefore to identify type variables in ambiguous
positions, and remove them from the list of goals during
unification. All type variables still have to be resolved by the
time we finish checking each application, but this has the added
bonus of making order much less important when it comes to
instantiating type variables.

Currently I am overly conservative about what qualifies as
ambigious, but this set should be expanded







Arm ElfMain: fix minor type errors
2019-01-04T10:54:41+00:00

Alastair Reid

2019-01-04T10:54:41+00:00

ed4ed7e7e0373d33c6aa3ed6566d0eee28ff0c91

I guess that Sail became a bit more strict about typechecking variables in
the last few months.





I guess that Sail became a bit more strict about typechecking variables in
the last few months.







Fix monomorpisation tests with typechecker changes
2018-12-20T22:00:40+00:00

Alasdair Armstrong

2018-12-20T22:00:40+00:00

0a9200153430f5e727b3ebe1fa272d4842069530

Add an extra argument for Type_check.prove for the location of the prove
call (as prove __POS__) to help debug SMT related issues





Add an extra argument for Type_check.prove for the location of the prove
call (as prove __POS__) to help debug SMT related issues







Various changes:
2018-12-10T20:45:05+00:00

Alasdair Armstrong

2018-12-10T20:39:16+00:00

5bc5f5dee8921f8d24260dae54177e00c291fcb1

* Improve type inference for numeric if statements (if_infer test)

* Correctly handle constraints for existentially quantified constructors (constraint_ctor test)

* Canonicalise all numeric types in function arguments, which
  triggers some weird edge cases between parametric polymorphism and
  subtyping of numeric arguments

* Because of this eq_int, eq_range, and eq_atom etc become identical

* Avoid duplicating destruct_exist in Env

* Handle some odd subtyping cases better





* Improve type inference for numeric if statements (if_infer test)

* Correctly handle constraints for existentially quantified constructors (constraint_ctor test)

* Canonicalise all numeric types in function arguments, which
  triggers some weird edge cases between parametric polymorphism and
  subtyping of numeric arguments

* Because of this eq_int, eq_range, and eq_atom etc become identical

* Avoid duplicating destruct_exist in Env

* Handle some odd subtyping cases better