From f855b929d1b7afcfb190b5425fba9bb7f36910ae Mon Sep 17 00:00:00 2001
From: rina <k@rina.fyi>
Date: Thu, 21 Mar 2024 17:15:38 +1000
Subject: [PATCH] stashing work to add types rt_expr and rt_label.

---
 libASL/cpp_backend.ml               |   4 +-
 offlineASL-cpp/aslp_lifter_base.cpp |  84 +++++++++++++
 offlineASL-cpp/aslp_lifter_base.hpp | 179 ++++++++++++++++------------
 offlineASL-cpp/build.sh             |   6 +
 4 files changed, 194 insertions(+), 79 deletions(-)
 create mode 100644 offlineASL-cpp/aslp_lifter_base.cpp
 create mode 100755 offlineASL-cpp/build.sh

diff --git a/libASL/cpp_backend.ml b/libASL/cpp_backend.ml
index 9f9ddb15..d6df30c7 100644
--- a/libASL/cpp_backend.ml
+++ b/libASL/cpp_backend.ml
@@ -152,8 +152,8 @@ and default_value t st =
       Printf.sprintf "llvm::APInt::getZero(%s)" (prints_expr w st)
   | Type_Constructor (Ident "boolean") -> "true"
   | Type_Constructor (Ident "integer") -> "0LL"
-  | Type_Constructor (Ident "rt_label") -> "(/*rt_label*/ static_cast<llvm::BasicBlock *>(nullptr))"
-  | Type_Constructor (Ident "rt_expr") -> "(/*rt_expr*/ 0)"
+  | Type_Constructor (Ident "rt_label") -> "rt_label{}"
+  | Type_Constructor (Ident "rt_expr") -> "rt_expr{}"
   | Type_Array(Index_Range(lo, hi),ty) ->
       let lo = prints_expr lo st in
       let hi = prints_expr hi st in
diff --git a/offlineASL-cpp/aslp_lifter_base.cpp b/offlineASL-cpp/aslp_lifter_base.cpp
new file mode 100644
index 00000000..2171bbd7
--- /dev/null
+++ b/offlineASL-cpp/aslp_lifter_base.cpp
@@ -0,0 +1,84 @@
+#include "aslp_lifter_base.hpp"
+
+namespace aslp {
+
+bits extract_bits(const bits &val, bigint lo, bigint wd) {
+  return val.extractBits(wd, lo);
+}
+
+bool f_eq_bits(bits x, bits y) {
+  return x == y;
+}
+bool f_ne_bits(bits x, bits y) {
+  return x != y;
+}
+bits f_add_bits(bits x, bits y) {
+  return x + y;
+}
+bits f_sub_bits(bits x, bits y) {
+  return x - y;
+}
+bits f_mul_bits(bits x, bits y) {
+  return x * y;
+}
+bits f_and_bits(bits x, bits y) {
+  return x & y;
+}
+bits f_or_bits(bits x, bits y) {
+  return x | y;
+}
+bits f_eor_bits(bits x, bits y) {
+  return x ^ y;
+}
+bits f_not_bits(bits x) {
+  return ~x;
+}
+bool f_slt_bits(bits x, bits y) {
+  return x.slt(y);
+}
+bool f_sle_bits(bits x, bits y) {
+  return x.sle(y);
+}
+bits f_zeros_bits(bigint n) {
+  return llvm::APInt::getZero(n);
+}
+bits f_ones_bits(bigint n) {
+  return llvm::APInt::getAllOnes(n);
+}
+bits f_replicate_bits(bits x, bigint n) {
+  assert(n >= 1);
+  bits original = x;
+  unsigned wd = x.getBitWidth();
+  x = x.zextOrTrunc(wd * n);
+  for (unsigned i = 1; i < n; i++) {
+    x <<= wd;
+    x |= original;
+  }
+  return x;
+}
+bits f_append_bits(bits x, bits y) {
+  x = x.zext(x.getBitWidth() + y.getBitWidth());
+  x <<= y.getBitWidth();
+  x |= y;
+  return x;
+}
+bits f_ZeroExtend(bits x, bigint wd) {
+  return x.zextOrTrunc(wd);
+}
+bits f_SignExtend(bits x, bigint wd) {
+  return x.sextOrTrunc(wd);
+}
+bits f_lsl_bits(bits x, bits y) {
+  return x << y;
+}
+bits f_lsr_bits(bits x, bits y) {
+  return x.lshr(y);
+}
+bits f_asr_bits(bits x, bits y) {
+  return x.ashr(y);
+}
+bigint f_cvt_bits_uint(bits x) {
+  return x.getZExtValue();
+}
+
+} // namespace aslp
\ No newline at end of file
diff --git a/offlineASL-cpp/aslp_lifter_base.hpp b/offlineASL-cpp/aslp_lifter_base.hpp
index 4982ceb2..5c44be24 100644
--- a/offlineASL-cpp/aslp_lifter_base.hpp
+++ b/offlineASL-cpp/aslp_lifter_base.hpp
@@ -9,91 +9,116 @@
 
 namespace aslp {
 
+// bits which are known at lift-time
 using bits = llvm::APInt;
+// bigints which are known at lift-time
 using bigint = long long;
 
-bits extract_bits(const bits &val, bigint lo, bigint wd) {
-  return val.extractBits(wd, lo);
-}
+// runtime-expression type, i.e. the type of values produced by the semantics
+using rt_expr = llvm::Value *;
+// runtime-label, supports switching blocks during semantics generation
+using rt_label = llvm::BasicBlock *;
 
-bool f_eq_bits(bits x, bits y) {
-  return x == y;
-}
-bool f_ne_bits(bits x, bits y) {
-  return x != y;
-}
-bits f_add_bits(bits x, bits y) {
-  return x + y;
-}
-bits f_sub_bits(bits x, bits y) {
-  return x - y;
-}
-bits f_mul_bits(bits x, bits y) {
-  return x * y;
-}
-bits f_and_bits(bits x, bits y) {
-  return x & y;
-}
-bits f_or_bits(bits x, bits y) {
-  return x | y;
-}
-bits f_eor_bits(bits x, bits y) {
-  return x ^ y;
-}
-bits f_not_bits(bits x) {
-  return ~x;
-}
-bool f_slt_bits(bits x, bits y) {
-  return x.slt(y);
-}
-bool f_sle_bits(bits x, bits y) {
-  return x.sle(y);
-}
-bits f_zeros_bits(bigint n) {
-  return llvm::APInt::getZero(n);
-}
-bits f_ones_bits(bigint n) {
-  return llvm::APInt::getAllOnes(n);
-}
-bits f_replicate_bits(bits x, bigint n) {
-  assert(n >= 1);
-  bits original = x;
-  unsigned wd = x.getBitWidth();
-  x = x.zextOrTrunc(wd * n);
-  for (unsigned i = 1; i < n; i++) {
-    x <<= wd;
-    x |= original;
-  }
-  return x;
-}
-bits f_append_bits(bits x, bits y) {
-  x = x.zext(x.getBitWidth() + y.getBitWidth());
-  x <<= y.getBitWidth();
-  x |= y;
-  return x;
-}
-bits f_ZeroExtend(bits x, bigint wd) {
-  return x.zextOrTrunc(wd);
-}
-bits f_SignExtend(bits x, bigint wd) {
-  return x.sextOrTrunc(wd);
-}
-bits f_lsl_bits(bits x, bits y) {
-  return x << y;
-}
-bits f_lsr_bits(bits x, bits y) {
-  return x.lshr(y);
-}
-bits f_asr_bits(bits x, bits y) {
-  return x.ashr(y);
-}
-bigint f_cvt_bits_uint(bits x) {
-  return x.getZExtValue();
-}
+bits extract_bits(const bits &val, bigint lo, bigint wd);
 
+bool f_eq_bits(bits x, bits y);
+bool f_ne_bits(bits x, bits y);
+bits f_add_bits(bits x, bits y);
+bits f_sub_bits(bits x, bits y);
+bits f_mul_bits(bits x, bits y);
+bits f_and_bits(bits x, bits y);
+bits f_or_bits(bits x, bits y);
+bits f_eor_bits(bits x, bits y);
+bits f_not_bits(bits x);
+bool f_slt_bits(bits x, bits y);
+bool f_sle_bits(bits x, bits y);
+bits f_zeros_bits(bigint n);
+bits f_ones_bits(bigint n);
+bits f_replicate_bits(bits x, bigint n);
+bits f_append_bits(bits x, bits y);
+bits f_ZeroExtend(bits x, bigint wd);
+bits f_SignExtend(bits x, bigint wd);
+bits f_lsl_bits(bits x, bits y);
+bits f_lsr_bits(bits x, bits y);
+bits f_asr_bits(bits x, bits y);
+bigint f_cvt_bits_uint(bits x);
 
 class aslp_lifter_base {
 
+virtual rt_expr f_decl_bv(const std::string_view& name, bigint width) = 0;
+let f_decl_bool name =
+
+let f_switch_context ctx =
+
+let f_gen_branch cond =
+let f_gen_assert b =
+let f_gen_bit_lit w (bv: bitvector) =
+let f_gen_bool_lit b =
+let f_gen_int_lit i =
+let f_gen_load v = v
+let f_gen_store v e = push_stmt (Stmt_Assign(to_lexpr v, e, loc))
+let f_gen_array_load a i =
+let f_gen_array_store a i e =
+let f_gen_Mem_set w x _ y z =
+let f_gen_Mem_read w x _ y =
+let f_gen_AArch64_MemTag_set x y z: unit =
+let f_gen_and_bool e1 e2 =
+let f_gen_or_bool e1 e2 =
+let f_gen_not_bool e1 =
+let f_gen_eq_enum e1 e2 =
+let f_gen_cvt_bits_uint w x =
+let f_gen_eq_bits w e1 e2 =
+let f_gen_ne_bits w e1 e2 =
+let f_gen_not_bits w e1 =
+let f_gen_cvt_bool_bv e =
+let f_gen_or_bits w e1 e2 =
+let f_gen_eor_bits w e1 e2 =
+let f_gen_and_bits w e1 e2 =
+let f_gen_add_bits w e1 e2 =
+let f_gen_sub_bits w e1 e2 =
+let f_gen_sdiv_bits w e1 e2 =
+let f_gen_sle_bits w e1 e2 =
+let f_gen_slt_bits w e1 e2 =
+let f_gen_mul_bits w e1 e2 =
+let f_gen_append_bits xw yw x y =
+let f_gen_lsr_bits xw yw x y =
+let f_gen_lsl_bits xw yw x y =
+let f_gen_asr_bits xw yw x y =
+let f_gen_replicate_bits xw yw x y =
+let f_gen_ZeroExtend xw yw x y =
+let f_gen_SignExtend xw yw x y =
+let f_gen_slice e lo wd =
+let f_gen_FPCompare w x y s t =
+let f_gen_FPCompareEQ w x y r =
+let f_gen_FPCompareGE w x y r =
+let f_gen_FPCompareGT w x y r =
+let f_gen_FPAdd w x y r =
+let f_gen_FPSub w x y r =
+let f_gen_FPMulAdd w a x y r =
+let f_gen_FPMulAddH w a x y r =
+let f_gen_FPMulX w x y r =
+let f_gen_FPMul w x y r =
+let f_gen_FPDiv w x y r =
+let f_gen_FPMin w x y r =
+let f_gen_FPMinNum w x y r =
+let f_gen_FPMax w x y r =
+let f_gen_FPMaxNum w x y r =
+let f_gen_FPRecpX w x t =
+let f_gen_FPSqrt w x t =
+let f_gen_FPRecipEstimate w x r =
+let f_gen_BFAdd x y =
+let f_gen_BFMul x y =
+let f_gen_FPConvertBF x t r =
+let f_gen_FPRecipStepFused w x y =
+let f_gen_FPRSqrtStepFused w x y =
+let f_gen_FPToFixed w w' x b u t r =
+let f_gen_FixedToFP w w' x b u t r =
+let f_gen_FPConvert w w' x t r =
+let f_gen_FPRoundInt w x t r e =
+let f_gen_FPRoundIntN w x t r e =
+let f_gen_FPToFixedJS_impl w w' x t s =
+
+
 };
 
 };
\ No newline at end of file
diff --git a/offlineASL-cpp/build.sh b/offlineASL-cpp/build.sh
new file mode 100755
index 00000000..890f9765
--- /dev/null
+++ b/offlineASL-cpp/build.sh
@@ -0,0 +1,6 @@
+#!/bin/bash -e
+
+set -o pipefail
+
+echo ":gen A64 aarch64_integer_arithmetic.+ cpp $(pwd)" | dune exec asli
+# dune build