<feed xmlns='http://www.w3.org/2005/Atom'>
<title>sail/test/ocaml/bitfield, branch sail2</title>
<subtitle>Formal specification language for ISAs</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/'/>
<entry>
<title>Interactive: Refactor sail.ml</title>
<updated>2019-03-27T16:32:08+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2019-03-27T16:21:05+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=790de19f73f1c164aba2259a6fe3f1a50eeff70c'/>
<id>790de19f73f1c164aba2259a6fe3f1a50eeff70c</id>
<content type='text'>
Rather than having a separate variable for each backend X,
opt_print_X, just have a single variable opt_print_target, where
target contains a string option, such as `Some "lem"` or `Some
"ocaml"`, then we have a function target that takes that string and
invokes the appropriate backend, so the main function in sail.ml goes
from being a giant if-then-else block to a single call to

target !opt_target ast env

This allows us to implement a :compile &lt;target&gt; command in the
interactive toplevel

Also implement a :rewrites &lt;target&gt; command which performs all the
rewrites for a specific target, so rather than doing e.g.

&gt; sail -c -O -o out $FILES

one could instead interactively do

&gt; sail -i
:option -undefined_gen
:load $FILES
:option -O
:option -o out
:rewrites c
:compile c
:quit

for the same result.

To support this the behavior of the interactive mode has changed
slightly. It no longer performs any rewrites at all, so a :rewrites
interpreter is currently needed to interpret functions in the
interactive toplevel, nor does it automatically set any other flags,
so -undefined_gen is needed in this case, which is usually implied by
the -c flag.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Rather than having a separate variable for each backend X,
opt_print_X, just have a single variable opt_print_target, where
target contains a string option, such as `Some "lem"` or `Some
"ocaml"`, then we have a function target that takes that string and
invokes the appropriate backend, so the main function in sail.ml goes
from being a giant if-then-else block to a single call to

target !opt_target ast env

This allows us to implement a :compile &lt;target&gt; command in the
interactive toplevel

Also implement a :rewrites &lt;target&gt; command which performs all the
rewrites for a specific target, so rather than doing e.g.

&gt; sail -c -O -o out $FILES

one could instead interactively do

&gt; sail -i
:option -undefined_gen
:load $FILES
:option -O
:option -o out
:rewrites c
:compile c
:quit

for the same result.

To support this the behavior of the interactive mode has changed
slightly. It no longer performs any rewrites at all, so a :rewrites
interpreter is currently needed to interpret functions in the
interactive toplevel, nor does it automatically set any other flags,
so -undefined_gen is needed in this case, which is usually implied by
the -c flag.
</pre>
</div>
</content>
</entry>
<entry>
<title>Flow typing and l-expression changes for ASL parser</title>
<updated>2018-05-03T19:08:20+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2018-05-03T14:30:55+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=3f93ecbc6dbdc315b79de4ee69bf6bc6a6420d57'/>
<id>3f93ecbc6dbdc315b79de4ee69bf6bc6a6420d57</id>
<content type='text'>
1. Experiment with allowing some flow typing on mutable variables for
translating ASL in a more idiomatic way. I realise after updating some
of the test cases that this could have some problematic side effects
for lem translation, where mutable variables are translated into
monadic code. We'd need to ensure that whatever flow typing happens
for mutable variables also works for monadic code, including within
transformed loops. If this doesn't work out some of these changes may
need to be reverted.

2. Make the type inference for l-expressions a bit smarter. Splits the
type checking rules for l-expressions into a inference part and a
checking part like the other bi-directional rules. Should not be able
to type check slightly more l-expresions, such as nested vector slices
that may not have checked previously.

The l-expression rules for vector patterns should be simpler now, but
they are also more strict about bounds checking. Previously the bounds
checks were derived from the corresponding operations that would
appear on the RHS (i.e. LEXP_vector would get it's check from
vector_access). This meant that the l-expression bounds checks could
be weakend by weakening the checks on those operations. Now this is no
longer possible, there is a -no_lexp_bounds_check option which turns
of bounds checking in l-expressions. Currently this is on for the
generated ARM spec, but this should only be temporary.

3. Add a LEXP_vector_concat which mirrors P_vector_concat except in
l-expressions. Previously there was a hack that overloaded LEXP_tup
for this to translate some ASL patterns, but that was fairly
ugly. Adapt the rewriter and other parts of the code to handle
this. The rewriter for lexp tuple vector assignments is now a rewriter
for vector concat assignments.

4. Include a newly generated version of aarch64_no_vector

5. Update the Ocaml test suite to use builtins in lib/
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
1. Experiment with allowing some flow typing on mutable variables for
translating ASL in a more idiomatic way. I realise after updating some
of the test cases that this could have some problematic side effects
for lem translation, where mutable variables are translated into
monadic code. We'd need to ensure that whatever flow typing happens
for mutable variables also works for monadic code, including within
transformed loops. If this doesn't work out some of these changes may
need to be reverted.

2. Make the type inference for l-expressions a bit smarter. Splits the
type checking rules for l-expressions into a inference part and a
checking part like the other bi-directional rules. Should not be able
to type check slightly more l-expresions, such as nested vector slices
that may not have checked previously.

The l-expression rules for vector patterns should be simpler now, but
they are also more strict about bounds checking. Previously the bounds
checks were derived from the corresponding operations that would
appear on the RHS (i.e. LEXP_vector would get it's check from
vector_access). This meant that the l-expression bounds checks could
be weakend by weakening the checks on those operations. Now this is no
longer possible, there is a -no_lexp_bounds_check option which turns
of bounds checking in l-expressions. Currently this is on for the
generated ARM spec, but this should only be temporary.

3. Add a LEXP_vector_concat which mirrors P_vector_concat except in
l-expressions. Previously there was a hack that overloaded LEXP_tup
for this to translate some ASL patterns, but that was fairly
ugly. Adapt the rewriter and other parts of the code to handle
this. The rewriter for lexp tuple vector assignments is now a rewriter
for vector concat assignments.

4. Include a newly generated version of aarch64_no_vector

5. Update the Ocaml test suite to use builtins in lib/
</pre>
</div>
</content>
</entry>
<entry>
<title>Create an update_field function for each field in a bitfield definition</title>
<updated>2018-02-21T14:48:36+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2018-02-21T14:47:37+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=0c9960e4efb510bea03906a528ac4cf57263dbf5'/>
<id>0c9960e4efb510bea03906a528ac4cf57263dbf5</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Allow overlapping bitfield field names</title>
<updated>2018-02-20T17:52:35+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2018-02-20T16:07:49+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=7f5f06adda7074e55708290d56fccb786a8df8f4'/>
<id>7f5f06adda7074e55708290d56fccb786a8df8f4</id>
<content type='text'>
Allows bitfields to share field names by generating accessors as

_get/set_name_field where name is the type name and field is the field
name rather than _get/set_field. They are still accessed and set using
just register.field() and register.field() = value.

Fixes #1
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Allows bitfields to share field names by generating accessors as

_get/set_name_field where name is the type name and field is the field
name rather than _get/set_field. They are still accessed and set using
just register.field() and register.field() = value.

Fixes #1
</pre>
</div>
</content>
</entry>
<entry>
<title>Update and fix test suite</title>
<updated>2018-01-22T13:41:35+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2018-01-22T13:41:35+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=1f8ac16d110e2b964a482c083e3782f406e94b69'/>
<id>1f8ac16d110e2b964a482c083e3782f406e94b69</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Ocaml semantics can now run aarch64 hello world example using octapod</title>
<updated>2018-01-11T20:42:07+00:00</updated>
<author>
<name>Alasdair Armstrong</name>
</author>
<published>2018-01-08T16:59:27+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/sail/commit/?id=f12a3b5ea9d541163f277ad5e40a005b8b955512'/>
<id>f12a3b5ea9d541163f277ad5e40a005b8b955512</id>
<content type='text'>
New testcase for bitfield syntax

Updated to work with latest lem and linksem
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
New testcase for bitfield syntax

Updated to work with latest lem and linksem
</pre>
</div>
</content>
</entry>
</feed>
