diff options
| author | Alasdair | 2018-11-28 00:29:10 +0000 |
|---|---|---|
| committer | Alasdair | 2018-11-28 00:36:13 +0000 |
| commit | 3a0bcd6e7f1dd565fb41574285c9c09bbbe14697 (patch) | |
| tree | f6fc3f0720eea07fe376c28ebad8d23b86e008c2 /test | |
| parent | 134ceff00b6a4837b133cb49b6d775161420dc62 (diff) | |
Allow folding constant expressions into single register reads
Essentially all we have to do to make this work is introduce a member of
the Value type, V_attempted_read <reg>, which is returned whenever we
try to read a register value with allow_registers disabled. This defers
the failure from reading the register to the point where the register
value is used (simply because nothing knows how to deal with
V_attempted_read). However, if V_attempted_read is returned directly as
the result of evaluating an expression, then we can replace the
expression with a single direct register read. This optimises some
indirection in the ARM specification.
Diffstat (limited to 'test')
| -rw-r--r-- | test/c/cfold_reg.expect | 1 | ||||
| -rw-r--r-- | test/c/cfold_reg.sail | 30 |
2 files changed, 31 insertions, 0 deletions
diff --git a/test/c/cfold_reg.expect b/test/c/cfold_reg.expect new file mode 100644 index 00000000..27ba77dd --- /dev/null +++ b/test/c/cfold_reg.expect @@ -0,0 +1 @@ +true diff --git a/test/c/cfold_reg.sail b/test/c/cfold_reg.sail new file mode 100644 index 00000000..a5090e91 --- /dev/null +++ b/test/c/cfold_reg.sail @@ -0,0 +1,30 @@ +default Order dec + +$include <prelude.sail> + +val "eq_string" : (string, string) -> bool + +overload operator == = {eq_string} + +register R : bool + +val "print_endline" : string -> unit + +function IMPDEF(str : string) -> bool = { + if str == "A" then { + return(R) + } else if str == "B" then { + true + } else { + false + } +} + +function main(() : unit) -> unit = { + R = true; + if IMPDEF("A") then { + print_endline("true") + } else { + print_endline("false") + } +}
\ No newline at end of file |
