Merge pull request #71 from UQ-PAC/rt_branch

Offline Improvements

dune

@@ -24,4 +24,4 @@
 
 (alias
  (name default)
- (deps (package asli)))
+ (deps (package asli) (alias install)))

libASL/offline_opt.ml

@@ -23,6 +23,9 @@ let is_lit f =
 let is_slice f =
   f = FIdent ("gen_slice", 0)
 
+let is_merge_target f2 =
+  f2 = Offline_transform.rt_merge_branch
+
 let is_gen_call f =
   let prefix = "gen_" in
   match f with
@@ -228,15 +231,15 @@ module CopyProp = struct
         merge_st tst fst
 
     (* RunTime branch *)
-    | Stmt_Assign(LExpr_Tuple([LExpr_Var tv; LExpr_Var fv; LExpr_Var mv]), Expr_TApply(f, [], [c]), loc) when is_branch f ->
+    | Stmt_ConstDecl(t, v, Expr_TApply(f, [], [c]), loc) when is_branch f ->
         (* Collect reads and process them all *)
         let deps = get_deps c in
         let st = read_vars deps st in
         (* Push the merge point *)
-        push_context mv st
+        push_context v st
 
     (* Context switch *)
-    | Stmt_TCall(f, [], [Expr_Var i], loc) when is_context_switch f ->
+    | Stmt_TCall(f, [], [Expr_TApply(f2, [], [Expr_Var i])], loc) when is_context_switch f && is_merge_target f2 ->
         let top = peek_context st in
         if i = top then pop_context st else st
 
@@ -286,3 +289,23 @@ module CopyProp = struct
     Asl_visitor.visit_stmts v body
 
 end
+
+module DeadContextSwitch = struct
+  (* Backwards walk to reduce consecutive context switches.
+     Could be extended to any context switches with no rt gen operations between,
+     but this pattern doesn't seem to show up. *)
+
+  let rec walk_stmts s dead =
+    List.fold_right (fun s (acc,dead) ->
+      match s with
+      | Stmt_TCall (f, _, _, _) when is_context_switch f && dead -> (acc,dead)
+      | Stmt_TCall (f, _, _, _) when is_context_switch f -> (s::acc,true)
+      | Stmt_If(c, t, [], f, loc) ->
+          let (t,dead) = walk_stmts t dead in
+          let (f,dead') = walk_stmts f dead in
+          (Stmt_If(c, t, [], f, loc)::acc, dead && dead')
+      | _ -> (s::acc,false)
+    ) s ([],dead)
+
+  let run fn body = let (s,_) =  walk_stmts body false in s
+end

libASL/offline_transform.ml

@@ -715,23 +715,20 @@ let gen_fresh_var loc ty =
   let+ _ = gen_var_decl loc ty i in
   i
 
+let rt_true_branch = FIdent("true_branch", 0)
+let rt_false_branch = FIdent("false_branch", 0)
+let rt_merge_branch = FIdent("merge_branch", 0)
+
 (* Generate a branch in the runtime program, with some way to refer to its targets and merge point *)
 let gen_branch loc c =
-  let@ tl = get_fresh_name in
-  let@ tf = get_fresh_name in
-  let@ tm = get_fresh_name in
-  let lexpr = LExpr_Tuple ( List.map (fun v -> LExpr_Var v) [tl;tf;tm] ) in
-  let+ _ = write [
-    Stmt_VarDeclsNoInit( rt_label_ty, [tl], loc);
-    Stmt_VarDeclsNoInit( rt_label_ty, [tf], loc);
-    Stmt_VarDeclsNoInit( rt_label_ty, [tm], loc);
-    Stmt_Assign(lexpr, Expr_TApply(rt_gen_branch, [], [c]), loc)
-  ] in
-  (tl,tf,tm)
+  let@ res = get_fresh_name in
+  let v = Expr_Var res in
+  let+ _ = write [Stmt_ConstDecl( rt_label_ty, res, Expr_TApply(rt_gen_branch, [], [c]), loc) ] in
+  (Expr_TApply(rt_true_branch, [], [v]),Expr_TApply(rt_false_branch,[],[v]),Expr_TApply(rt_merge_branch,[],[v]))
 
 (* Switch the implicit context to one produced by gen_branch *)
 let switch_context loc t =
-  write [Stmt_TCall(rt_switch_context, [], [Expr_Var t], loc)]
+  write [Stmt_TCall(rt_switch_context, [], [t], loc)]
 
 (* Generate a variable store/load *)
 let gen_var_store loc v e =

libASL/req_analysis.ml

@@ -68,6 +68,10 @@ let wrap f = fun s ->
   match f s with
   | Either.Left r -> Either.Left (s,[],r)
   | Either.Right e -> Either.Right e
+let wrapl f = fun s ->
+  match f s with
+  | Either.Left (s,w,r) -> Either.Left (s,[],(w,r))
+  | Either.Right e -> Either.Right e
 let write l = fun s ->
   Either.Left (s,[l],())
 let writel l = fun s ->
@@ -391,7 +395,17 @@ let contains_req_assign s : bool wrm =
     | _ -> pure false) s in
   List.mem true search
 
-let fix_stmt fid s =
+let rec process_alts fid v loc alts d =
+  match alts with
+  | (Alt_Alt(p,oc,b))::alts ->
+      let e = Expr_In (v, Pat_Set p) in
+      let e = match oc with Some c -> Expr_TApply (FIdent ("and_bool", 0), [], [e;c]) | _ -> e in
+      let@ (b,_) = wrapl (fix_stmts fid b) in
+      let+ acc = process_alts fid v loc alts d in
+      [Stmt_If(e, b, [], acc, loc)]
+  | _ -> pure d
+
+and fix_stmt fid s =
   match s with
   | Stmt_VarDecl(ty, v, e, loc) 
   | Stmt_ConstDecl(ty, v, e, loc) ->
@@ -403,29 +417,35 @@ let fix_stmt fid s =
       | _, Some vals ->
           Printf.printf "  %s: Splitting %s into %d values\n" (name_of_FIdent fid)(pp_stmt s) (List.length vals);
           let@ _ = write (Stmt_VarDeclsNoInit(ty, [v], loc)) in
+          write (List.fold_right (fun (test,expr) acc ->
+            Stmt_If(test, [Stmt_Assign(LExpr_Var v, expr, loc)], [], [acc], loc)) vals (Stmt_Throw (Ident ("UNREACHABLE"), loc))))
+  | Stmt_Assign(LExpr_Var v, e, loc) ->
+      let@ r = get_req v in
+      let vals = enumerate e in
+      (match r, vals with
+      | NoReq, _
+      | _, None -> write s
+      | _, Some vals ->
+          Printf.printf "  %s: Splitting assign %s into %d values\n" (name_of_FIdent fid)(pp_stmt s) (List.length vals);
           write (List.fold_right (fun (test,expr) acc -> 
             Stmt_If(test, [Stmt_Assign(LExpr_Var v, expr, loc)], [], [acc], loc)) vals (Stmt_Throw (Ident ("UNREACHABLE"), loc))))
   | Stmt_Case(v, alts, None, loc) ->
       let@ b = contains_req_assign (List.flatten (List.map (function Alt_Alt(p,oc,b) -> b) alts)) in
       if not b then write s
       else
         (Printf.printf "  %s: Splitting %s into %d values\n" (name_of_FIdent fid) (pp_stmt s) (List.length alts);
-        write (List.fold_left (fun acc (Alt_Alt(p,oc,b)) ->
-          let e = Expr_In (v, Pat_Set p) in
-          let e = match oc with Some c -> Expr_TApply (FIdent ("and_bool", 0), [], [e;c]) | _ -> e in
-          Stmt_If(e, b, [], [acc], loc)) (Stmt_Throw (Ident ("UNREACHABLE"), loc))  alts))
+        let@ r = process_alts fid v loc alts [Stmt_Throw (Ident ("UNREACHABLE"), loc)] in
+        writel r)
   | Stmt_Case(v, alts, Some d, loc) ->
       let@ b = contains_req_assign (List.flatten (List.map (function Alt_Alt(p,oc,b) -> b) alts)) in
       if not b then write s
       else
         (Printf.printf "  %s: Splitting %s into %d values\n" (name_of_FIdent fid) (pp_stmt s) (List.length alts + 1);
-        writel (List.fold_left (fun acc (Alt_Alt(p,oc,b)) ->
-          let e = Expr_In (v, Pat_Set p) in
-          let e = match oc with Some c -> Expr_TApply (FIdent ("and_bool", 0), [], [e;c]) | _ -> e in
-          [Stmt_If(e, b, [], acc, loc)]) (d)  alts))
+        let@ r = process_alts fid v loc alts d in
+        writel r)
   | _ -> write s
 
-let fix_stmts fid s =
+and fix_stmts fid s =
   let+ _ = traverse (fix_stmt fid) s in
   () 
 

libASL/symbolic_lifter.ml

@@ -34,10 +34,6 @@ let unsupported_set = IdentSet.of_list [
 
 (* Problematic instruction encoding names, due to various disassembly issues *)
 let problematic_enc = [
-  (* >10k lines due to unrolling/splitting *)
-  "aarch64_memory_vector_multiple_no_wb";
-  "aarch64_memory_vector_multiple_post_inc";
-
   (* Need to extend RemoveUnsupported to remove all undesirable global variables & fields *)
   "aarch64_system_register_system";
   "aarch64_system_register_cpsr";
@@ -372,6 +368,7 @@ let run iset pat env =
   Printf.printf "Stages 7-8: Offline Transform\n";
   let offline_fns = Offline_transform.run fns env in
   let offline_fns = Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.CopyProp.run k)) offline_fns in
+  let offline_fns = Bindings.mapi (fun k -> fnsig_upd_body (Offline_opt.DeadContextSwitch.run k)) offline_fns in
   let dsig = fnsig_upd_body (DecoderCleanup.run (unsupported_inst tests offline_fns)) dsig in
   let dsig = fnsig_upd_body (Transforms.RemoveUnused.remove_unused IdentSet.empty) dsig in
   Printf.printf "\n";

libASL/transforms.ml

@@ -121,13 +121,14 @@ let infer_type (e: expr): ty option =
 
 (** Remove variables which are unused at the end of the statement list. *)
 module RemoveUnused = struct
-  let rec remove_unused (globals: IdentSet.t) xs = (remove_unused' globals xs)
+  let rec remove_unused (globals: IdentSet.t) xs = fst (remove_unused' globals IdentSet.empty xs)
 
-  and remove_unused' (used: IdentSet.t) (xs: stmt list): (stmt list) =
-    fst @@ List.fold_right (fun stmt (acc, used) ->
+  and remove_unused' globals (used: IdentSet.t) (xs: stmt list): (stmt list * IdentSet.t) =
+    List.fold_right (fun stmt (acc, used) ->
 
       let pass = (acc, used)
       and emit (s: stmt) = (s::acc, IdentSet.union used (fv_stmt s))
+      and halt (s: stmt) = ([stmt], IdentSet.empty)
       in
 
       match stmt with
@@ -146,19 +147,34 @@ module RemoveUnused = struct
           else pass
       | Stmt_Assign(le, r, loc) ->
         let lvs = assigned_vars_of_stmts [stmt] in
-        if not (IdentSet.disjoint lvs used)
+        if not (IdentSet.disjoint lvs used) || not (IdentSet.disjoint lvs globals)
           then emit stmt
           else pass
+
+      (* Skip if structure if possible - often seen in decode tests *)
+      | Stmt_If(Expr_Var (Ident "TRUE"), tstmts, elsif, fstmts, loc) ->
+          let (tstmts',tused) = remove_unused' globals used tstmts in
+          (tstmts'@acc,tused)
+
       | Stmt_If(c, tstmts, elsif, fstmts, loc) ->
-        let tstmts' = remove_unused' used tstmts in
-        let fstmts' = remove_unused' used fstmts in
+        let (tstmts',tused) = remove_unused' globals used tstmts in
+        let (fstmts',fused) = remove_unused' globals used fstmts in
         let elsif' = List.map
           (fun (S_Elsif_Cond (c,ss)) ->
-            S_Elsif_Cond (c, remove_unused' used ss))
+            let (b, bused) = remove_unused' globals used ss in
+            let bused = IdentSet.union bused (fv_expr c) in
+            (S_Elsif_Cond (c,b), bused))
           elsif in
+        let used = List.fold_right (fun (_,u) -> IdentSet.union u) elsif' (IdentSet.union tused fused) in
+        let used = IdentSet.union used (fv_expr c) in
         (match (tstmts',fstmts',elsif') with
         | [], [], [] -> pass
-        | _, _, _ -> emit (Stmt_If(c, tstmts', elsif', fstmts', loc)))
+        | _, _, _ -> (Stmt_If(c, tstmts', List.map fst elsif', fstmts', loc)::acc,used))
+
+      (* Unreachable points *)
+      | Stmt_Assert (Expr_Var (Ident "FALSE"), _)
+      | Stmt_Throw _ -> halt stmt
+
       | x -> emit x
 
     ) xs ([], used)

offlineASL/utils.ml

@@ -121,6 +121,10 @@ let f_gen_branch cond =
             Expr_LitInt (string_of_int merge)], loc));
   (true_branch, false_branch, merge)
 
+let f_true_branch (a,_,_) = a
+let f_false_branch (_,b,_) = b
+let f_merge_branch (_,_,c) = c
+
 let undefined () = Expr_Tuple []
 
 (* Runtime assert *)

tests/coverage/dune

@@ -12,6 +12,10 @@
  (deps (package asli) ./encodings)
  (action (copy ./run.sh ./run)))
 
+(rule
+ (deps (package asli) ./encodings)
+ (action (copy ./off_run.sh ./off_run)))
+
 (rule (with-stdout-to cov_integer (run ./run "aarch64_integer.+")))
 (rule (with-stdout-to cov_branch  (run ./run "aarch64_branch.+")))
 (rule (with-stdout-to cov_float   (run ./run "aarch64_float_.+")))
@@ -25,4 +29,17 @@
 (rule (alias coverage) (action (diff ./aarch64_vector1 cov_vector1)))
 (rule (alias coverage) (action (diff ./aarch64_vector2 cov_vector2)))
 (rule (alias coverage) (action (diff ./aarch64_memory cov_memory)))
-
+
+(rule (with-stdout-to off_cov_integer (run ./off_run "aarch64_integer.+")))
+(rule (with-stdout-to off_cov_branch  (run ./off_run "aarch64_branch.+")))
+(rule (with-stdout-to off_cov_float   (run ./off_run "aarch64_float_.+")))
+(rule (with-stdout-to off_cov_vector1 (run ./off_run "aarch64_vector_arithmetic_binary.+")))
+(rule (with-stdout-to off_cov_vector2 (run ./off_run "aarch64_vector_(?!arithmetic_binary).+")))
+(rule (with-stdout-to off_cov_memory  (run ./off_run "aarch64_memory_.+")))
+
+(rule (alias offline-coverage) (action (diff ./aarch64_integer off_cov_integer)))
+(rule (alias offline-coverage) (action (diff ./aarch64_branch  off_cov_branch)))
+(rule (alias offline-coverage) (action (diff ./aarch64_float   off_cov_float)))
+(rule (alias offline-coverage) (action (diff ./aarch64_vector1 off_cov_vector1)))
+(rule (alias offline-coverage) (action (diff ./aarch64_vector2 off_cov_vector2)))
+(rule (alias offline-coverage) (action (diff ./aarch64_memory  off_cov_memory)))

tests/coverage/off_run.sh

@@ -0,0 +1,8 @@
+#!/bin/bash -e
+
+pattern="${1:?requires regex pattern as first argument}"
+
+asl_dir="$(asli --aarch64-dir)"
+output="$(asloff-coverage "$pattern")"
+
+echo "$output" | sed "s#$asl_dir#.#g"