From 230fd015b5f5424cd0859aa832547a7cf4562eff Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 12 Dec 2022 16:56:18 +0100 Subject: [PATCH] safety-checker: support #copy --- CHANGELOG.md | 4 ++++ compiler/safety/success/copy.jazz | 8 ++++++++ compiler/src/safety/safetyInterpreter.ml | 1 + 3 files changed, 13 insertions(+) create mode 100644 compiler/safety/success/copy.jazz diff --git a/CHANGELOG.md b/CHANGELOG.md index 14c9e8032..dca90694f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -32,6 +32,10 @@ ([PR #303](https://github.com/jasmin-lang/jasmin/pull/303); fixes [#301](https://github.com/jasmin-lang/jasmin/issues/301)). +- Safety checker handles the `#copy` operator + ([PR #312](https://github.com/jasmin-lang/jasmin/pull/312); + fixes [#308](https://github.com/jasmin-lang/jasmin/issues/308)). + ## Other changes - Explicit if-then-else in flag combinations is no longer supported diff --git a/compiler/safety/success/copy.jazz b/compiler/safety/success/copy.jazz new file mode 100644 index 000000000..23f9f8d9a --- /dev/null +++ b/compiler/safety/success/copy.jazz @@ -0,0 +1,8 @@ +export fn test(reg u64 x) -> reg u64 { + reg u64[1] r; + stack u64[1] s; + r[0] = x; + s = #copy(r); + x = s[0]; + return x; +} diff --git a/compiler/src/safety/safetyInterpreter.ml b/compiler/src/safety/safetyInterpreter.ml index f2eae06b0..02c93c71a 100644 --- a/compiler/src/safety/safetyInterpreter.ml +++ b/compiler/src/safety/safetyInterpreter.ml @@ -1577,6 +1577,7 @@ end = struct let cr = { ginstr with i_desc = Cassgn (lv, tag, Bty (U sz), er) } in aeval_if asmOp ginstr c [cl] [cr] state + | Copn ([ lv ], _, Ocopy _, [ e ]) | Cassgn (lv, _, _, e) -> let abs = AbsExpr.abs_assign state.abs