summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAlasdair2018-11-28 00:29:10 +0000
committerAlasdair2018-11-28 00:36:13 +0000
commit3a0bcd6e7f1dd565fb41574285c9c09bbbe14697 (patch)
treef6fc3f0720eea07fe376c28ebad8d23b86e008c2 /test
parent134ceff00b6a4837b133cb49b6d775161420dc62 (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.expect1
-rw-r--r--test/c/cfold_reg.sail30
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