fix offline generation after vectoriser and add ci

.github/workflows/test.yml

@@ -12,14 +12,15 @@ permissions:
   contents: read
   packages: read
 
+defaults:
+  run:
+    # https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#jobsjob_idstepsshell
+    # XXX using multi-line string will fail since \n is stuck to the end of the argument.
+    shell: "nix develop github:katrinafyi/pac-nix#ocamlPackages_pac.asli --impure --accept-flake-config --command bash --noprofile --norc -eo pipefail {0}"
+
 jobs:
   test:
     runs-on: ubuntu-latest
-    defaults:
-      run:
-        # https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#jobsjob_idstepsshell
-        # XXX using multi-line string will fail since \n is stuck to the end of the argument.
-        shell: "nix develop github:katrinafyi/pac-nix#ocamlPackages_pac.asli --impure --accept-flake-config --command bash --noprofile --norc -eo pipefail {0}"
 
     steps:
     - uses: actions/checkout@v4
@@ -28,16 +29,32 @@ jobs:
     - run: echo 'preparing nix shell environment'
 
     - run: dune build --profile release
+
     - run: dune runtest -j4
     - run: dune build '@coverage' -j4
-    - run: |
-        echo "OUTPUT=$(pwd)/_build/default/tests/coverage" >> $GITHUB_OUTPUT
-        rm -rf _build/default/tests/coverage/encodings
-      id: coverage
+    - run: rm -rf _build/default/tests/coverage/encodings
 
     - name: Upload new coverage results
       if: always()
       uses: actions/upload-artifact@v4
       with:
         name: coverage-output-${{ github.run_id }}
-        path: ${{ steps.coverage.outputs.OUTPUT }}
+        path: |
+          _build/default/tests/coverage
+          _build/.promotion-staging
+
+  offline:
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v4
+
+    - uses: cachix/install-nix-action@v25
+    - run: echo 'preparing nix shell environment'
+
+    - run: dune build --profile release -j4
+    - run: echo ':gen A64 aarch64_* ocaml offlineASL' | OCAMLRUNPARAM=b dune exec asli
+
+    - run: dune build offlineASL -j4
+
+    - run: dune build @offline-coverage -j4

.gitignore

@@ -19,3 +19,5 @@ scripts/result.txt
 scripts/output.txt
 scripts/cntlm.bir
 scripts/total.txt
+
+offlineASL/aarch64_*

libASL/dis.ml

@@ -23,8 +23,6 @@ module StringCmp = struct
 end
 module StringMap = Map.Make(StringCmp)
 
-let use_vectoriser = ref false
-
 let debug_level_none = -1
 let debug_level = ref debug_level_none
 let debug_show_trace = ref false
@@ -110,15 +108,18 @@ let no_inline = [
   "AArch64.MemTag.set",0;
 ]
 
-let no_inline_pure = [
+let no_inline_pure () = [
   "LSL",0;
   "LSR",0;
   "ASR",0;
   "SignExtend",0;
   "ZeroExtend",0;
+] @ (if !Symbolic.use_vectoriser then [
   "Elem.set",0;
   "Elem.read",0;
-]
+] else [])
+
+
 
 (** A variable's stack level and original identifier name.
     The "stack level" is how many scopes deep it is.
@@ -941,15 +942,15 @@ and dis_expr' (loc: l) (x: AST.expr): sym rws =
     | Expr_LitString(s) -> DisEnv.pure (Val (from_stringLit s))
     )
 
-and no_inline_pure_ids = List.map (fun (x,y) -> FIdent(x,y))
-  no_inline_pure
+and no_inline_pure_ids () = List.map (fun (x,y) -> FIdent(x,y))
+  (no_inline_pure ())
 
 and no_inline_ids = List.map (fun (x,y) -> FIdent (x,y))
   no_inline
 
 (** Disassemble call to function *)
 and dis_funcall (loc: l) (f: ident) (tvs: sym list) (vs: sym list): sym rws =
-    if List.mem f no_inline_pure_ids &&
+    if List.mem f (no_inline_pure_ids ()) &&
       ((List.exists (function Exp _ -> true | _ -> false) tvs) ||
         (List.exists (function Exp _ -> true | _ -> false) vs)) then
       let expr = Exp (Expr_TApply (f, List.map sym_expr tvs, List.map sym_expr vs)) in
@@ -1595,7 +1596,7 @@ let dis_core (env: Eval.Env.t) (unroll_bound) ((lenv,globals): env) (decode: dec
  *)
 let dis_decode_entry_with_inst (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): string * stmt list =
   let max_upper_bound = Z.of_int64 Int64.max_int in
-  match !use_vectoriser with
+  match !Symbolic.use_vectoriser with
   | false -> dis_core env max_upper_bound (lenv,globals) decode op
   | true ->
     let enc,stmts' = dis_core env Z.one (lenv,globals) decode op in

libASL/flags.ml

@@ -6,7 +6,7 @@ let flags = StringMap.of_seq @@ List.to_seq [
     ("trace:prim",  Eval.trace_primop);
     ("trace:instr", Eval.trace_instruction);
     ("eval:concrete_unknown", Value.concrete_unknown);
-    ("dis:vectors", Dis.use_vectoriser);
+    ("dis:vectors", Symbolic.use_vectoriser);
 ]
 
 let set_flag s =

libASL/ocaml_backend.ml

@@ -379,7 +379,7 @@ let write_dune_file files dir =
     (:standard -w -27 -w -33 -cclib -lstdc++))
   (modules \n";
   List.iter (fun k ->
-    Printf.fprintf oc "    %s\n" (String.lowercase_ascii k)
+    Printf.fprintf oc "    %s\n" k
   ) files;
   Printf.fprintf oc "  )
   (libraries asli.libASL))";

libASL/offline_transform.ml

@@ -174,7 +174,7 @@ let join_state (a: state) (b: state): state =
 (* Produce a runtime value if any arg is runtime *)
 let pure_prims =
   Value.prims_pure @
-  (List.map fst Dis.no_inline_pure) @ [
+  (List.map fst (Dis.no_inline_pure ())) @ [
     "lsr_bits";
     "sle_bits";
     "lsl_bits";

libASL/symbolic.ml

@@ -5,6 +5,8 @@ open Value
 open Asl_utils
 open Primops
 
+let use_vectoriser = ref false
+
 type sym =
   | Val of value
   | Exp of expr
@@ -617,12 +619,12 @@ let sym_insert_bits loc (old_width: int) (old: sym) (lo: sym) (wd: sym) (v: sym)
       else
         sym_append_bits loc (old_width - up) up (sym_slice loc old up (old_width - up))
           (sym_append_bits loc wd lo v (sym_slice loc old 0 lo))
-  | (_, _, Val wd', _) when Primops.prim_zrem_int (Z.of_int old_width) (to_integer Unknown wd') = Z.zero ->
+  | (_, _, Val wd', _) when Primops.prim_zrem_int (Z.of_int old_width) (to_integer Unknown wd') = Z.zero && !use_vectoriser ->
       (* Elem.set *)
       let pos = zdiv_int lo wd in
       Exp ( Expr_TApply (FIdent("Elem.set", 0), [expr_of_int old_width ; sym_expr wd],
           List.map sym_expr [old ; pos ; wd ; v]) )
-  | (_, Val (VInt l), _, _) when l = Z.zero ->
+  | (_, Val (VInt l), _, _) when l = Z.zero && !use_vectoriser ->
       Exp (Expr_TApply (FIdent ("Elem.set", 0), [expr_of_int old_width ; sym_expr wd],
           List.map sym_expr [old ; lo ; wd ; v]))
 

libASL/symbolic_lifter.ml

@@ -158,7 +158,7 @@ let unsupported f = IdentSet.mem f unsupported_set
 let get_inlining_frontier =
   (* Collect all functions dis will not inline *)
   let l1 = IdentSet.of_list (List.map (fun (f,i) -> FIdent (f,i)) Dis.no_inline) in
-  let l2 = IdentSet.of_list (List.map (fun (f,i) -> FIdent (f,i)) Dis.no_inline_pure) in
+  let l2 = IdentSet.of_list (List.map (fun (f,i) -> FIdent (f,i)) (Dis.no_inline_pure ())) in
   (* Collect all prims *)
   let l3 = IdentSet.of_list (List.map (fun f -> FIdent (f,0)) Value.prims_pure) in
   let l4 = IdentSet.of_list (List.map (fun f -> FIdent (f,0)) Value.prims_impure) in

libASL/transforms.ml

@@ -1097,7 +1097,13 @@ module IntToBits = struct
     method! vstmt s =
       match s with
       | Stmt_ConstDecl(ty, nm, _, _) ->
-        var_types <- Bindings.add nm ty var_types;
+          var_types <- Bindings.add nm ty var_types;
+          DoChildren
+      | Stmt_VarDecl(ty, nm, _, _) ->
+          var_types <- Bindings.add nm ty var_types;
+          DoChildren
+      | Stmt_VarDeclsNoInit(ty, [nm], _) ->
+          var_types <- Bindings.add nm ty var_types;
         DoChildren
       | _ -> DoChildren
 
@@ -1374,9 +1380,9 @@ module RedundantSlice = struct
       (* Last chance to convert dynamic slices into shift & static slice *)
       | Expr_Slices(x, [Slice_LoWd(l,w)]) when non_const l ->
           (match option_or (infer_type x) (self#var_type' x) with
-          (*| Some (Type_Bits xw) ->
+          | Some (Type_Bits xw) ->
               let e = Expr_TApply (FIdent ("LSR", 0), [xw], [x; l]) in
-              Expr_Slices(e, [Slice_LoWd (Expr_LitInt "0", w)])*)
+              Expr_Slices(e, [Slice_LoWd (Expr_LitInt "0", w)])
           | _ -> e)
       | Expr_Slices(e', [Slice_LoWd (Expr_LitInt "0", wd)]) ->
           let try_match (opt: ty option): expr =

offlineASL/offline_utils.ml

@@ -10,6 +10,8 @@ let from_bitsLit x =
 let frem_int     = Primops.prim_frem_int
 let extract_bits = Primops.prim_extract
 
+let f_Elem_set w _w' vec index size x = Primops.prim_insert vec index size x
+
 let f_eq_bits          _ = Primops.prim_eq_bits
 let f_ne_bits          _ = Primops.prim_ne_bits
 let f_add_bits         _ = Primops.prim_add_bits
@@ -36,6 +38,9 @@ let f_lsr_bits       w _ (x : bitvector) (y : bitvector) = mkBits w (Z.shift_rig
 let f_asr_bits       w _ (x : bitvector) (y : bitvector) = mkBits w (Z.shift_right x.v (Z.to_int y.v))
 let f_cvt_bits_uint w bv = Primops.prim_cvt_bits_uint bv
 
+let f_sdiv_int           = Primops.prim_fdiv_int
+let f_shl_int            = Primops.prim_shl_int
+
 (****************************************************************
  * Runtime State
  ****************************************************************)
@@ -157,6 +162,14 @@ let f_gen_array_load a i =
 let f_gen_array_store a i e =
   push_stmt (Stmt_Assign(LExpr_Array(to_lexpr a, expr_of_z i), e, loc))
 
+(* Vector accesses, with runtime values and indices. *)
+let f_gen_Elem_read w w' vec index size =
+  (* w' should always == size *)
+  Expr_TApply (FIdent ("Elem.read", 0), [expr_of_z w; expr_of_z w'], [vec; index; size])
+let f_gen_Elem_set w w' vec index size x =
+  (* w' should always == size *)
+  Expr_TApply (FIdent ("Elem.set", 0), [expr_of_z w; expr_of_z w'], [vec; index; size; x])
+
 (* Memory ops *)
 let f_gen_Mem_set w x _ y z =
   push_stmt (Stmt_TCall (FIdent ("Mem.set", 0), [expr_of_z w], [x; expr_of_z w; y; z], Unknown))