From 9fca4aade48f109ab4b36c179b7f067e04386f74 Mon Sep 17 00:00:00 2001 From: rina Date: Mon, 1 Jul 2024 16:27:50 +1000 Subject: [PATCH 1/5] dis: add function to extract disasm name --- libASL/dis.ml | 37 ++++++++++++++++++++----------------- 1 file changed, 20 insertions(+), 17 deletions(-) diff --git a/libASL/dis.ml b/libASL/dis.ml index f7b9ed1..caea0bf 100644 --- a/libASL/dis.ml +++ b/libASL/dis.ml @@ -1386,11 +1386,11 @@ let dis_decode_slice (loc: l) (x: decode_slice) (op: Primops.bigint): value rws ) (* Duplicate of eval_decode_case modified to print rather than eval *) -let rec dis_decode_case (loc: AST.l) (x: decode_case) (op: Primops.bigint): unit rws = +let rec dis_decode_case (loc: AST.l) (x: decode_case) (op: Primops.bigint): string rws = let body = dis_decode_case' loc x op in if no_debug() then body - else DisEnv.scope loc "dis_decode_case" (pp_decode_case x) Utils.pp_unit body -and dis_decode_case' (loc: AST.l) (x: decode_case) (op: Primops.bigint): unit rws = + else DisEnv.scope loc "dis_decode_case" (pp_decode_case x) Fun.id body +and dis_decode_case' (loc: AST.l) (x: decode_case) (op: Primops.bigint): string rws = (match x with | DecoderCase_Case (ss, alts, loc) -> let@ vs = DisEnv.traverse (fun s -> dis_decode_slice loc s op) ss in @@ -1399,8 +1399,8 @@ and dis_decode_case' (loc: AST.l) (x: decode_case) (op: Primops.bigint): unit rw | (alt :: alts') -> let@ alt' = dis_decode_alt loc alt vs op in (match alt' with - | true -> DisEnv.unit - | false -> dis alts') + | Some x -> DisEnv.pure x + | None -> dis alts') | [] -> raise (DisInternalError (loc, "unmatched decode pattern")) ) @@ -1409,16 +1409,16 @@ and dis_decode_case' (loc: AST.l) (x: decode_case) (op: Primops.bigint): unit rw ) (* Duplicate of eval_decode_alt modified to print rather than eval *) -and dis_decode_alt (loc: l) (x: decode_alt) (vs: value list) (op: Primops.bigint): bool rws = +and dis_decode_alt (loc: l) (x: decode_alt) (vs: value list) (op: Primops.bigint): string option rws = let body = dis_decode_alt' loc x vs op in if no_debug() then body - else DisEnv.scope loc "dis_decode_alt" (pp_decode_alt x) string_of_bool body -and dis_decode_alt' (loc: AST.l) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: Primops.bigint): bool rws = + else DisEnv.scope loc "dis_decode_alt" (pp_decode_alt x) Option.(fold ~none:"(unmatched)" ~some:Fun.id) body +and dis_decode_alt' (loc: AST.l) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: Primops.bigint): string option rws = if List.for_all2 (Eval.eval_decode_pattern loc) ps vs then (match b with | DecoderBody_UNPRED loc -> raise (Throw (loc, Exc_Unpredictable)) | DecoderBody_UNALLOC loc -> raise (Throw (loc, Exc_Undefined)) - | DecoderBody_NOP loc -> DisEnv.pure true + | DecoderBody_NOP loc -> DisEnv.pure (Some "(NOP)") | DecoderBody_Encoding (inst, l) -> let@ (enc, opost, cond, exec) = DisEnv.reads (fun env -> Eval.Env.getInstruction loc env inst) in let@ enc_match = dis_encoding enc op in @@ -1450,9 +1450,9 @@ and dis_decode_alt' (loc: AST.l) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: end; let@ () = DisEnv.write stmts in - DisEnv.pure true + DisEnv.pure (Some (pprint_ident inst)) end else begin - DisEnv.pure false + DisEnv.pure None end | DecoderBody_Decoder (fs, c, loc) -> let@ () = DisEnv.modify (LocalEnv.addLevel) in @@ -1462,12 +1462,12 @@ and dis_decode_alt' (loc: AST.l) (DecoderAlt_Alt (ps, b)) (vs: value list) (op: declare_assign_var loc (val_type v) f (Val v) ) fs in - let@ () = dis_decode_case loc c op in + let@ result = dis_decode_case loc c op in let@ () = DisEnv.modify (LocalEnv.popLevel) in - DisEnv.pure true + DisEnv.pure (Some result) ) else - DisEnv.pure false + DisEnv.pure None type env = (LocalEnv.t * IdentSet.t) @@ -1480,9 +1480,9 @@ let enum_types env i = | Some l -> Some (Z.log2up (Z.of_int (List.length l))) | _ -> None -let dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): stmt list = +let dis_decode_entry_with_inst (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): string * stmt list = let DecoderCase_Case (_,_,loc) = decode in - let ((),lenv',stmts) = (dis_decode_case loc decode op) env lenv in + let (inst,lenv',stmts) = (dis_decode_case loc decode op) env lenv in let varentries = List.(concat @@ map (fun vars -> StringMap.(bindings (map fst vars))) lenv.locals) in let bindings = Asl_utils.Bindings.of_seq @@ List.to_seq @@ List.map (fun (x,y) -> (Ident x,y)) varentries in (* List.iter (fun (v,t) -> Printf.printf ("%s:%s\n") v (pp_type t)) varentries; *) @@ -1505,7 +1505,10 @@ let dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_cas List.iter (fun s -> Printf.printf "%s\n" (pp_stmt s)) stmts'; Printf.printf "===========\n"; end; - stmts' + inst, stmts' + +let dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: Primops.bigint): stmt list = + snd @@ dis_decode_entry_with_inst env (lenv, globals) decode op let build_env (env: Eval.Env.t): env = let env = Eval.Env.freeze env in From 8ce869fd877130f61ebb8679705dc78b77e74e58 Mon Sep 17 00:00:00 2001 From: rina Date: Mon, 1 Jul 2024 16:34:33 +1000 Subject: [PATCH 2/5] server: return 'encoding' field to store the instruction encoding name --- bin/server.ml | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/bin/server.ml b/bin/server.ml index 77a14ba..ae8e250 100644 --- a/bin/server.ml +++ b/bin/server.ml @@ -17,24 +17,28 @@ open Lwt let persistent_env = lazy (Option.get (Arm_env.aarch64_evaluation_environment ())) -let eval_instr (opcode: string) : string = +let eval_instr (opcode: string) : string * string = let pp_raw stmt : string = Utils.to_string (Asl_parser_pp.pp_raw_stmt stmt) |> String.trim in - let address = None in - let env' = Lazy.force persistent_env in - let stmts : Asl_ast.stmt list = Dis.retrieveDisassembly ?address env' (Dis.build_env env') opcode in - let stmts' = List.map pp_raw stmts in - String.concat "\n" stmts' + let _address = None in + + let env' = Lazy.force persistent_env in + let lenv = Dis.build_env env' in + let decoder = Eval.Env.getDecoder env' (Ident "A64") in + let (enc, stmts) = Dis.dis_decode_entry_with_inst env' lenv decoder (Z.of_string opcode) in + + let stmts' = List.map pp_raw stmts in + enc, String.concat "\n" stmts' let get_reply (jsonin: string) : Cohttp.Code.status_code * string = (*let json = Yojson.Safe.from_string jsonin in *) let make_reply code tail = - (code, Yojson.Safe.to_string (`Assoc [("instruction", `String jsonin); tail])) in + (code, Yojson.Safe.to_string (`Assoc (["instruction", `String jsonin] @ tail))) in Printf.printf "Disassembling '%s'\n" jsonin; flush stdout; match (eval_instr jsonin) with - | exception e -> make_reply `Internal_server_error ("error", `String (Printexc.to_string e)) - | x -> make_reply `OK ("semantics", `String x) + | exception e -> make_reply `Internal_server_error ["error", `String (Printexc.to_string e)] + | enc, x -> make_reply `OK [ "encoding", `String enc; "semantics", `String x; ] let unsupp_method_resp : Cohttp.Code.status_code * string = From 2a4bb833b022a85db81f04423f4a744667b90fad Mon Sep 17 00:00:00 2001 From: rina Date: Tue, 2 Jul 2024 10:43:03 +1000 Subject: [PATCH 3/5] aslp-cpp: also return encoding name --- aslp-cpp/include/aslp-cpp/aslp-cpp.hpp | 7 +++++-- aslp-cpp/source/aslp-cpp.cpp | 9 ++++++--- aslp-cpp/test/source/aslp-cpp_test.cpp | 3 ++- 3 files changed, 13 insertions(+), 6 deletions(-) diff --git a/aslp-cpp/include/aslp-cpp/aslp-cpp.hpp b/aslp-cpp/include/aslp-cpp/aslp-cpp.hpp index 08feb23..485e334 100644 --- a/aslp-cpp/include/aslp-cpp/aslp-cpp.hpp +++ b/aslp-cpp/include/aslp-cpp/aslp-cpp.hpp @@ -7,6 +7,9 @@ namespace httplib { class Client; } // namespace httplib; +// tuple of encoding and semantics +using aslp_opcode_result_t = std::tuple; + class aslp_connection { std::unique_ptr client {nullptr}; @@ -14,7 +17,7 @@ class aslp_connection public: aslp_connection(const std::string& server_addr, int server_port); aslp_connection(aslp_connection&&) noexcept; - auto get_opcode(uint32_t opcode) -> std::string; + auto get_opcode(uint32_t opcode) -> aslp_opcode_result_t; void wait_active(); ~aslp_connection(); }; @@ -54,7 +57,7 @@ class aslp_client { auto static start(const std::string& addr, int server_port) -> std::unique_ptr; /** Returns the semantics for the given opcode, as a newline-separated string. */ - auto get_opcode(uint32_t opcode) -> std::string; + auto get_opcode(uint32_t opcode) -> aslp_opcode_result_t; /** Destroys the aslp_client and terminates the managed server as well. */ virtual ~aslp_client() { diff --git a/aslp-cpp/source/aslp-cpp.cpp b/aslp-cpp/source/aslp-cpp.cpp index 57cf5e7..598d504 100644 --- a/aslp-cpp/source/aslp-cpp.cpp +++ b/aslp-cpp/source/aslp-cpp.cpp @@ -147,7 +147,7 @@ void aslp_connection::wait_active() std::cout << "\n"; } -std::string aslp_connection::get_opcode(uint32_t opcode) +aslp_opcode_result_t aslp_connection::get_opcode(uint32_t opcode) { auto codestr = std::format("{:#x}", opcode); std::cout << codestr << "\n"; @@ -167,7 +167,10 @@ std::string aslp_connection::get_opcode(uint32_t opcode) if (!result.contains("semantics")) { throw std::runtime_error("semantics missing"); } - return result["semantics"]; + if (!result.contains("encoding")) { + throw std::runtime_error("encoding name missing"); + } + return {result["encoding"], result["semantics"]}; } aslp_connection::aslp_connection(const std::string& server_addr, @@ -179,7 +182,7 @@ aslp_connection::aslp_connection(const std::string& server_addr, aslp_connection::aslp_connection(aslp_connection&&) noexcept = default; aslp_connection::~aslp_connection() = default; -std::string aslp_client::get_opcode(uint32_t opcode) +aslp_opcode_result_t aslp_client::get_opcode(uint32_t opcode) { aslp_connection conn {server_addr, server_port}; conn.wait_active(); diff --git a/aslp-cpp/test/source/aslp-cpp_test.cpp b/aslp-cpp/test/source/aslp-cpp_test.cpp index ed1e825..2bf6877 100644 --- a/aslp-cpp/test/source/aslp-cpp_test.cpp +++ b/aslp-cpp/test/source/aslp-cpp_test.cpp @@ -8,7 +8,8 @@ auto main() -> int auto s = aslp_client::start(); try { - auto c = s->get_opcode(0xFD430091); + std::string c; + std::tie(std::ignore, c) = s->get_opcode(0xFD430091); std::cout << c << "\n"; } catch (std::runtime_error &e) { std::cout << " error " << e.what() << "\n"; From 91693e085df4725e158616a66db7a92b8538d321 Mon Sep 17 00:00:00 2001 From: Kait Lam Date: Wed, 3 Jul 2024 14:03:06 +1000 Subject: [PATCH 4/5] avoid regex for debug indentation (#97) this should speed up performance in javascript. --- libASL/dis.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/libASL/dis.ml b/libASL/dis.ml index f7b9ed1..a47f4c8 100644 --- a/libASL/dis.ml +++ b/libASL/dis.ml @@ -385,20 +385,19 @@ module DisEnv = struct let num, s = LocalEnv.incNumSymbols s in (Ident (prefix ^ string_of_int num),s,empty) - let indent: string rws = + let indent: string list rws = let+ i = gets (fun l -> l.indent) in - let h = i / 2 in - let s = String.concat "" (List.init h (fun _ -> "\u{2502} \u{250a} ")) in - if i mod 2 == 0 then - s ^ "" - else - s ^ "\u{2502} " + (* when concatenated, produces a string of the form: + "| I | I | ..." where | and I are + alternating unicode box-drawing lines *) + List.init i (fun i -> if i mod 2 == 0 then "\u{2502} " else "\u{250a} ") let debug (minLevel: int) (s: string): unit rws = if !debug_level >= minLevel then let+ i = indent in - let s' = Str.global_replace (Str.regexp "\n") ("\n"^i) s in - Printf.printf "%s%s\n" i s'; + List.iter + (fun l -> List.iter print_string i; print_endline l) + (String.split_on_char '\n' s); () else unit From 66ba70b5aa3bf085077d71b9091926f4283591de Mon Sep 17 00:00:00 2001 From: Kait Lam Date: Wed, 3 Jul 2024 14:29:17 +1000 Subject: [PATCH 5/5] grammar: fix TypeBoolean (#96) * grammar: fix TypeBoolean was previously missing quotation marks. * tests: add opcode with emitting boolean variable --- libASL/Semantics.g4 | 2 +- tests/aslt/ops.txt | 3 + tests/aslt/test_antlr.t | 156 ++++++++++++++++++++- tests/aslt/test_dis.t | 297 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 456 insertions(+), 2 deletions(-) diff --git a/libASL/Semantics.g4 b/libASL/Semantics.g4 index c72cca8..0bcf24f 100644 --- a/libASL/Semantics.g4 +++ b/libASL/Semantics.g4 @@ -46,7 +46,7 @@ type_register_slices: type: 'Type_Bits' OPEN_PAREN expr CLOSE_PAREN # TypeBits - | 'Type_Constructor(boolean)' # TypeBoolean + | 'Type_Constructor("boolean")' # TypeBoolean | 'Type_Constructor(' ident ')' # TypeConstructor | 'Type_Register' OPEN_PAREN QUOTE width=integer QUOTE type_register_slices CLOSE_PAREN # TypeRegister ; diff --git a/tests/aslt/ops.txt b/tests/aslt/ops.txt index c7abcec..49712f6 100644 --- a/tests/aslt/ops.txt +++ b/tests/aslt/ops.txt @@ -24,3 +24,6 @@ // cnt v0.8b, v0.8b https://github.com/UQ-PAC/aslp/issues/43 0x0e205800 + +// sqrdmulh v0.8h, v0.8h, v1.h[3] https://github.com/UQ-PAC/aslp/pull/96 +0x4f71d000 diff --git a/tests/aslt/test_antlr.t b/tests/aslt/test_antlr.t index ff90d7f..6a5f0b6 100644 --- a/tests/aslt/test_antlr.t +++ b/tests/aslt/test_antlr.t @@ -358,6 +358,160 @@ tests building and running of the antlr grammar. requires java (stmts [ (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " result__5_7 ") )) , (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 4))) ] , [ (expr Expr_Var ( (ident " result__5_7 ") )) ; (expr (bits '0001')) ] )) ))) ]) , [ ] , (stmts [ ]) ))) - (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Array ( (lexpr LExpr_Var ( (ident " _Z ") )) , (expr (integer 0)) )) , (expr Expr_TApply ( (ident " ZeroExtend.0 ") , [ (targs (expr (integer 64))) ; (targs (expr (integer 128))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 56))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " result__5_7 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 48))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp81__5 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 40))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp70__5 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 32))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp59__5 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 24))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp48__5 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 16))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp37__5 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 8))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp26__5 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp14__5 ") )) ] )) ] )) ] )) ] )) ] )) ] )) ] )) ] )) ; (expr (integer 128)) ] )) ))) ) + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Array ( (lexpr LExpr_Var ( (ident " _Z ") )) , (expr (integer 0)) )) , (expr Expr_TApply ( (ident " ZeroExtend.0 ") , [ (targs (expr (integer 64))) ; (targs (expr (integer 128))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 56))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " result__5_7 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 48))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp81__5 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 40))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp70__5 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 32))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp59__5 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 24))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp48__5 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 16))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp37__5 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 8))) ; (targs (expr (integer 8))) ] , [ (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp26__5 ") )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 4))) ] , [ (expr (bits '0000')) ; (expr Expr_Var ( (ident " Exp14__5 ") )) ] )) ] )) ] )) ] )) ] )) ] )) ] )) ] )) ; (expr (integer 128)) ] )) ))) + (stmt (assignment_stmt Stmt_ConstDecl ( (type Type_Bits ( (expr (integer 17)) )) , (ident " Cse43__5 ") , (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 17))) ] , [ (expr Expr_Slices ( (expr Expr_Array ( (expr Expr_Var ( (ident " _Z ") )) , (expr (integer 0)) )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 16)) )) ] )) ; (expr (integer 17)) ] )) ))) + (stmt (assignment_stmt Stmt_ConstDecl ( (type Type_Bits ( (expr (integer 17)) )) , (ident " Cse36__5 ") , (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 17))) ] , [ (expr Expr_Slices ( (expr Expr_Array ( (expr Expr_Var ( (ident " _Z ") )) , (expr (integer 0)) )) , [ (slice Slice_LoWd ( (expr (integer 16)) , (expr (integer 16)) )) ] )) ; (expr (integer 17)) ] )) ))) + (stmt (assignment_stmt Stmt_ConstDecl ( (type Type_Bits ( (expr (integer 17)) )) , (ident " Cse30__5 ") , (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 17))) ] , [ (expr Expr_Slices ( (expr Expr_Array ( (expr Expr_Var ( (ident " _Z ") )) , (expr (integer 0)) )) , [ (slice Slice_LoWd ( (expr (integer 32)) , (expr (integer 16)) )) ] )) ; (expr (integer 17)) ] )) ))) + (stmt (assignment_stmt Stmt_ConstDecl ( (type Type_Bits ( (expr (integer 17)) )) , (ident " Cse24__5 ") , (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 17))) ] , [ (expr Expr_Slices ( (expr Expr_Array ( (expr Expr_Var ( (ident " _Z ") )) , (expr (integer 0)) )) , [ (slice Slice_LoWd ( (expr (integer 48)) , (expr (integer 16)) )) ] )) ; (expr (integer 17)) ] )) ))) + (stmt (assignment_stmt Stmt_ConstDecl ( (type Type_Bits ( (expr (integer 17)) )) , (ident " Cse18__5 ") , (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 17))) ] , [ (expr Expr_Slices ( (expr Expr_Array ( (expr Expr_Var ( (ident " _Z ") )) , (expr (integer 0)) )) , [ (slice Slice_LoWd ( (expr (integer 64)) , (expr (integer 16)) )) ] )) ; (expr (integer 17)) ] )) ))) + (stmt (assignment_stmt Stmt_ConstDecl ( (type Type_Bits ( (expr (integer 17)) )) , (ident " Cse12__5 ") , (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 17))) ] , [ (expr Expr_Slices ( (expr Expr_Array ( (expr Expr_Var ( (ident " _Z ") )) , (expr (integer 0)) )) , [ (slice Slice_LoWd ( (expr (integer 80)) , (expr (integer 16)) )) ] )) ; (expr (integer 17)) ] )) ))) + (stmt (assignment_stmt Stmt_ConstDecl ( (type Type_Bits ( (expr (integer 17)) )) , (ident " Cse6__5 ") , (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 17))) ] , [ (expr Expr_Slices ( (expr Expr_Array ( (expr Expr_Var ( (ident " _Z ") )) , (expr (integer 0)) )) , [ (slice Slice_LoWd ( (expr (integer 96)) , (expr (integer 16)) )) ] )) ; (expr (integer 17)) ] )) ))) + (stmt (assignment_stmt Stmt_ConstDecl ( (type Type_Bits ( (expr (integer 17)) )) , (ident " Cse0__5 ") , (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 17))) ] , [ (expr Expr_Slices ( (expr Expr_Array ( (expr Expr_Var ( (ident " _Z ") )) , (expr (integer 0)) )) , [ (slice Slice_LoWd ( (expr (integer 112)) , (expr (integer 16)) )) ] )) ; (expr (integer 17)) ] )) ))) + (stmt (assignment_stmt Stmt_ConstDecl ( (type Type_Bits ( (expr (integer 33)) )) , (ident " Cse42__5 ") , (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 33))) ] , [ (expr Expr_Slices ( (expr Expr_Array ( (expr Expr_Var ( (ident " _Z ") )) , (expr (integer 1)) )) , [ (slice Slice_LoWd ( (expr (integer 48)) , (expr (integer 16)) )) ] )) ; (expr (integer 33)) ] )) ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Bits ( (expr (integer 16)) )) , [ (ident " SignedSatQ17__5 ") ] ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Constructor("boolean")) , [ (ident " SignedSatQ18__5 ") ] ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr (bits '000000000000000000111111111111111')) ; (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse43__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ17__5 ") )) , (expr (bits '0111111111111111')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ18__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse43__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ; (expr (bits '111111111111111111000000000000000')) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ17__5 ") )) , (expr (bits '1000000000000000')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ18__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ17__5 ") )) , (expr Expr_Slices ( (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse43__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 16)) )) ] )) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ18__5 ") )) , (expr Expr_Var ( (ident " FALSE ") )) ))) ]) ))) ]) ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_Var ( (ident " SignedSatQ18__5 ") )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " FPSR ") )) , (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 28))) ] , [ (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 28)) , (expr (integer 4)) )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 1))) ; (targs (expr (integer 27))) ] , [ (expr (bits '1')) ; (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 27)) )) ] )) ] )) ] )) ))) ]) , [ ] , + (stmts [ ]) ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Bits ( (expr (integer 16)) )) , [ (ident " SignedSatQ31__5 ") ] ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Constructor("boolean")) , [ (ident " SignedSatQ32__5 ") ] ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr (bits '000000000000000000111111111111111')) ; (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse36__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ31__5 ") )) , (expr (bits '0111111111111111')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ32__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse36__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ; (expr (bits '111111111111111111000000000000000')) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ31__5 ") )) , (expr (bits '1000000000000000')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ32__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ31__5 ") )) , (expr Expr_Slices ( (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse36__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 16)) )) ] )) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ32__5 ") )) , (expr Expr_Var ( (ident " FALSE ") )) ))) ]) ))) ]) ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_Var ( (ident " SignedSatQ32__5 ") )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " FPSR ") )) , (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 28))) ] , [ (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 28)) , (expr (integer 4)) )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 1))) ; (targs (expr (integer 27))) ] , [ (expr (bits '1')) ; (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 27)) )) ] )) ] )) ] )) ))) ]) , [ ] , + (stmts [ ]) ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Bits ( (expr (integer 16)) )) , [ (ident " SignedSatQ44__5 ") ] ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Constructor("boolean")) , [ (ident " SignedSatQ45__5 ") ] ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr (bits '000000000000000000111111111111111')) ; (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse30__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ44__5 ") )) , (expr (bits '0111111111111111')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ45__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse30__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ; (expr (bits '111111111111111111000000000000000')) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ44__5 ") )) , (expr (bits '1000000000000000')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ45__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ44__5 ") )) , (expr Expr_Slices ( (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse30__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 16)) )) ] )) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ45__5 ") )) , (expr Expr_Var ( (ident " FALSE ") )) ))) ]) ))) ]) ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_Var ( (ident " SignedSatQ45__5 ") )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " FPSR ") )) , (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 28))) ] , [ (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 28)) , (expr (integer 4)) )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 1))) ; (targs (expr (integer 27))) ] , [ (expr (bits '1')) ; (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 27)) )) ] )) ] )) ] )) ))) ]) , [ ] , + (stmts [ ]) ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Bits ( (expr (integer 16)) )) , [ (ident " SignedSatQ57__5 ") ] ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Constructor("boolean")) , [ (ident " SignedSatQ58__5 ") ] ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr (bits '000000000000000000111111111111111')) ; (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse24__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ57__5 ") )) , (expr (bits '0111111111111111')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ58__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse24__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ; (expr (bits '111111111111111111000000000000000')) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ57__5 ") )) , (expr (bits '1000000000000000')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ58__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ57__5 ") )) , (expr Expr_Slices ( (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse24__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 16)) )) ] )) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ58__5 ") )) , (expr Expr_Var ( (ident " FALSE ") )) ))) ]) ))) ]) ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_Var ( (ident " SignedSatQ58__5 ") )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " FPSR ") )) , (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 28))) ] , [ (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 28)) , (expr (integer 4)) )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 1))) ; (targs (expr (integer 27))) ] , [ (expr (bits '1')) ; (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 27)) )) ] )) ] )) ] )) ))) ]) , [ ] , + (stmts [ ]) ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Bits ( (expr (integer 16)) )) , [ (ident " SignedSatQ70__5 ") ] ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Constructor("boolean")) , [ (ident " SignedSatQ71__5 ") ] ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr (bits '000000000000000000111111111111111')) ; (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse18__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ70__5 ") )) , (expr (bits '0111111111111111')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ71__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse18__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ; (expr (bits '111111111111111111000000000000000')) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ70__5 ") )) , (expr (bits '1000000000000000')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ71__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ70__5 ") )) , (expr Expr_Slices ( (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse18__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 16)) )) ] )) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ71__5 ") )) , (expr Expr_Var ( (ident " FALSE ") )) ))) ]) ))) ]) ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_Var ( (ident " SignedSatQ71__5 ") )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " FPSR ") )) , (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 28))) ] , [ (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 28)) , (expr (integer 4)) )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 1))) ; (targs (expr (integer 27))) ] , [ (expr (bits '1')) ; (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 27)) )) ] )) ] )) ] )) ))) ]) , [ ] , + (stmts [ ]) ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Bits ( (expr (integer 16)) )) , [ (ident " SignedSatQ83__5 ") ] ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Constructor("boolean")) , [ (ident " SignedSatQ84__5 ") ] ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr (bits '000000000000000000111111111111111')) ; (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse12__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ83__5 ") )) , (expr (bits '0111111111111111')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ84__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse12__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ; (expr (bits '111111111111111111000000000000000')) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ83__5 ") )) , (expr (bits '1000000000000000')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ84__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ83__5 ") )) , (expr Expr_Slices ( (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse12__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 16)) )) ] )) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ84__5 ") )) , (expr Expr_Var ( (ident " FALSE ") )) ))) ]) ))) ]) ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_Var ( (ident " SignedSatQ84__5 ") )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " FPSR ") )) , (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 28))) ] , [ (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 28)) , (expr (integer 4)) )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 1))) ; (targs (expr (integer 27))) ] , [ (expr (bits '1')) ; (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 27)) )) ] )) ] )) ] )) ))) ]) , [ ] , + (stmts [ ]) ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Bits ( (expr (integer 16)) )) , [ (ident " SignedSatQ96__5 ") ] ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Constructor("boolean")) , [ (ident " SignedSatQ97__5 ") ] ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr (bits '000000000000000000111111111111111')) ; (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse6__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ96__5 ") )) , (expr (bits '0111111111111111')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ97__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse6__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ; (expr (bits '111111111111111111000000000000000')) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ96__5 ") )) , (expr (bits '1000000000000000')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ97__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ96__5 ") )) , (expr Expr_Slices ( (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse6__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 16)) )) ] )) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ97__5 ") )) , (expr Expr_Var ( (ident " FALSE ") )) ))) ]) ))) ]) ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_Var ( (ident " SignedSatQ97__5 ") )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " FPSR ") )) , (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 28))) ] , [ (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 28)) , (expr (integer 4)) )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 1))) ; (targs (expr (integer 27))) ] , [ (expr (bits '1')) ; (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 27)) )) ] )) ] )) ] )) ))) ]) , [ ] , + (stmts [ ]) ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Bits ( (expr (integer 16)) )) , [ (ident " SignedSatQ109__5 ") ] ))) + (stmt (assignment_stmt Stmt_VarDeclsNoInit ( (type Type_Constructor("boolean")) , [ (ident " SignedSatQ110__5 ") ] ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr (bits '000000000000000000111111111111111')) ; (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse0__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ109__5 ") )) , (expr (bits '0111111111111111')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ110__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (conditional_stmt Stmt_If ( (expr Expr_TApply ( (ident " slt_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse0__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) ; (expr (bits '111111111111111111000000000000000')) ] )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ109__5 ") )) , (expr (bits '1000000000000000')) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ110__5 ") )) , (expr Expr_Var ( (ident " TRUE ") )) ))) ]) , [ ] , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ109__5 ") )) , (expr Expr_Slices ( (expr Expr_TApply ( (ident " asr_bits.0 ") , [ (targs (expr (integer 33))) ; (targs (expr (integer 6))) ] , [ (expr Expr_TApply ( (ident " add_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " SignExtend.0 ") , [ (targs (expr (integer 17))) ; (targs (expr (integer 33))) ] , [ (expr Expr_TApply ( (ident " mul_bits.0 ") , [ (targs (expr (integer 17))) ] , [ (expr (bits '00000000000000010')) ; (expr Expr_Var ( (ident " Cse0__5 ") )) ] )) ; (expr (integer 33)) ] )) ; (expr Expr_Var ( (ident " Cse42__5 ") )) ] )) ; (expr (bits '000000000000000001000000000000000')) ] )) ; (expr (bits '010000')) ] )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 16)) )) ] )) ))) ; + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " SignedSatQ110__5 ") )) , (expr Expr_Var ( (ident " FALSE ") )) ))) ]) ))) ]) ))) + (stmt (conditional_stmt Stmt_If ( (expr Expr_Var ( (ident " SignedSatQ110__5 ") )) , + (stmts [ + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Var ( (ident " FPSR ") )) , (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 4))) ; (targs (expr (integer 28))) ] , [ (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 28)) , (expr (integer 4)) )) ] )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 1))) ; (targs (expr (integer 27))) ] , [ (expr (bits '1')) ; (expr Expr_Slices ( (expr Expr_Var ( (ident " FPSR ") )) , [ (slice Slice_LoWd ( (expr (integer 0)) , (expr (integer 27)) )) ] )) ] )) ] )) ))) ]) , [ ] , + (stmts [ ]) ))) + (stmt (assignment_stmt Stmt_Assign ( (lexpr LExpr_Array ( (lexpr LExpr_Var ( (ident " _Z ") )) , (expr (integer 0)) )) , (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 112))) ] , [ (expr Expr_Var ( (ident " SignedSatQ109__5 ") )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 96))) ] , [ (expr Expr_Var ( (ident " SignedSatQ96__5 ") )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 80))) ] , [ (expr Expr_Var ( (ident " SignedSatQ83__5 ") )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 64))) ] , [ (expr Expr_Var ( (ident " SignedSatQ70__5 ") )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 48))) ] , [ (expr Expr_Var ( (ident " SignedSatQ57__5 ") )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 32))) ] , [ (expr Expr_Var ( (ident " SignedSatQ44__5 ") )) ; (expr Expr_TApply ( (ident " append_bits.0 ") , [ (targs (expr (integer 16))) ; (targs (expr (integer 16))) ] , [ (expr Expr_Var ( (ident " SignedSatQ31__5 ") )) ; (expr Expr_Var ( (ident " SignedSatQ17__5 ") )) ] )) ] )) ] )) ] )) ] )) ] )) ] )) ))) ) $ cat antlr_err diff --git a/tests/aslt/test_dis.t b/tests/aslt/test_dis.t index 3bf9339..1f61fa0 100644 --- a/tests/aslt/test_dis.t +++ b/tests/aslt/test_dis.t @@ -597,4 +597,301 @@ run asli with these commands Stmt_Assign(LExpr_Var("result__5_7"),Expr_TApply("add_bits.0",[4],[Expr_Var("result__5_7");'0001'])) ],[],[]) Stmt_Assign(LExpr_Array(LExpr_Var("_Z"),0),Expr_TApply("ZeroExtend.0",[64;128],[Expr_TApply("append_bits.0",[8;56],[Expr_TApply("append_bits.0",[4;4],['0000';Expr_Var("result__5_7")]);Expr_TApply("append_bits.0",[8;48],[Expr_TApply("append_bits.0",[4;4],['0000';Expr_Var("Exp81__5")]);Expr_TApply("append_bits.0",[8;40],[Expr_TApply("append_bits.0",[4;4],['0000';Expr_Var("Exp70__5")]);Expr_TApply("append_bits.0",[8;32],[Expr_TApply("append_bits.0",[4;4],['0000';Expr_Var("Exp59__5")]);Expr_TApply("append_bits.0",[8;24],[Expr_TApply("append_bits.0",[4;4],['0000';Expr_Var("Exp48__5")]);Expr_TApply("append_bits.0",[8;16],[Expr_TApply("append_bits.0",[4;4],['0000';Expr_Var("Exp37__5")]);Expr_TApply("append_bits.0",[8;8],[Expr_TApply("append_bits.0",[4;4],['0000';Expr_Var("Exp26__5")]);Expr_TApply("append_bits.0",[4;4],['0000';Expr_Var("Exp14__5")])])])])])])])]);128])) + " + 0x4f71d000 + " + Decoding instruction A64 4f71d000 + constant bits ( 17 ) Cse43__5 = SignExtend.0 {{ 16,17 }} ( __array _Z [ 0 ] [ 0 +: 16 ],17 ) ; + constant bits ( 17 ) Cse36__5 = SignExtend.0 {{ 16,17 }} ( __array _Z [ 0 ] [ 16 +: 16 ],17 ) ; + constant bits ( 17 ) Cse30__5 = SignExtend.0 {{ 16,17 }} ( __array _Z [ 0 ] [ 32 +: 16 ],17 ) ; + constant bits ( 17 ) Cse24__5 = SignExtend.0 {{ 16,17 }} ( __array _Z [ 0 ] [ 48 +: 16 ],17 ) ; + constant bits ( 17 ) Cse18__5 = SignExtend.0 {{ 16,17 }} ( __array _Z [ 0 ] [ 64 +: 16 ],17 ) ; + constant bits ( 17 ) Cse12__5 = SignExtend.0 {{ 16,17 }} ( __array _Z [ 0 ] [ 80 +: 16 ],17 ) ; + constant bits ( 17 ) Cse6__5 = SignExtend.0 {{ 16,17 }} ( __array _Z [ 0 ] [ 96 +: 16 ],17 ) ; + constant bits ( 17 ) Cse0__5 = SignExtend.0 {{ 16,17 }} ( __array _Z [ 0 ] [ 112 +: 16 ],17 ) ; + constant bits ( 33 ) Cse42__5 = SignExtend.0 {{ 16,33 }} ( __array _Z [ 1 ] [ 48 +: 16 ],33 ) ; + bits ( 16 ) SignedSatQ17__5 ; + boolean SignedSatQ18__5 ; + if slt_bits.0 {{ 33 }} ( '000000000000000000111111111111111',asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse43__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) ) then { + SignedSatQ17__5 = '0111111111111111' ; + SignedSatQ18__5 = TRUE ; + } else { + if slt_bits.0 {{ 33 }} ( asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse43__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ),'111111111111111111000000000000000' ) then { + SignedSatQ17__5 = '1000000000000000' ; + SignedSatQ18__5 = TRUE ; + } else { + SignedSatQ17__5 = asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse43__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) [ 0 +: 16 ] ; + SignedSatQ18__5 = FALSE ; + } + } + if SignedSatQ18__5 then { + FPSR = append_bits.0 {{ 4,28 }} ( FPSR [ 28 +: 4 ],append_bits.0 {{ 1,27 }} ( '1',FPSR [ 0 +: 27 ] ) ) ; + } + bits ( 16 ) SignedSatQ31__5 ; + boolean SignedSatQ32__5 ; + if slt_bits.0 {{ 33 }} ( '000000000000000000111111111111111',asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse36__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) ) then { + SignedSatQ31__5 = '0111111111111111' ; + SignedSatQ32__5 = TRUE ; + } else { + if slt_bits.0 {{ 33 }} ( asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse36__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ),'111111111111111111000000000000000' ) then { + SignedSatQ31__5 = '1000000000000000' ; + SignedSatQ32__5 = TRUE ; + } else { + SignedSatQ31__5 = asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse36__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) [ 0 +: 16 ] ; + SignedSatQ32__5 = FALSE ; + } + } + if SignedSatQ32__5 then { + FPSR = append_bits.0 {{ 4,28 }} ( FPSR [ 28 +: 4 ],append_bits.0 {{ 1,27 }} ( '1',FPSR [ 0 +: 27 ] ) ) ; + } + bits ( 16 ) SignedSatQ44__5 ; + boolean SignedSatQ45__5 ; + if slt_bits.0 {{ 33 }} ( '000000000000000000111111111111111',asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse30__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) ) then { + SignedSatQ44__5 = '0111111111111111' ; + SignedSatQ45__5 = TRUE ; + } else { + if slt_bits.0 {{ 33 }} ( asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse30__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ),'111111111111111111000000000000000' ) then { + SignedSatQ44__5 = '1000000000000000' ; + SignedSatQ45__5 = TRUE ; + } else { + SignedSatQ44__5 = asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse30__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) [ 0 +: 16 ] ; + SignedSatQ45__5 = FALSE ; + } + } + if SignedSatQ45__5 then { + FPSR = append_bits.0 {{ 4,28 }} ( FPSR [ 28 +: 4 ],append_bits.0 {{ 1,27 }} ( '1',FPSR [ 0 +: 27 ] ) ) ; + } + bits ( 16 ) SignedSatQ57__5 ; + boolean SignedSatQ58__5 ; + if slt_bits.0 {{ 33 }} ( '000000000000000000111111111111111',asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse24__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) ) then { + SignedSatQ57__5 = '0111111111111111' ; + SignedSatQ58__5 = TRUE ; + } else { + if slt_bits.0 {{ 33 }} ( asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse24__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ),'111111111111111111000000000000000' ) then { + SignedSatQ57__5 = '1000000000000000' ; + SignedSatQ58__5 = TRUE ; + } else { + SignedSatQ57__5 = asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse24__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) [ 0 +: 16 ] ; + SignedSatQ58__5 = FALSE ; + } + } + if SignedSatQ58__5 then { + FPSR = append_bits.0 {{ 4,28 }} ( FPSR [ 28 +: 4 ],append_bits.0 {{ 1,27 }} ( '1',FPSR [ 0 +: 27 ] ) ) ; + } + bits ( 16 ) SignedSatQ70__5 ; + boolean SignedSatQ71__5 ; + if slt_bits.0 {{ 33 }} ( '000000000000000000111111111111111',asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse18__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) ) then { + SignedSatQ70__5 = '0111111111111111' ; + SignedSatQ71__5 = TRUE ; + } else { + if slt_bits.0 {{ 33 }} ( asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse18__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ),'111111111111111111000000000000000' ) then { + SignedSatQ70__5 = '1000000000000000' ; + SignedSatQ71__5 = TRUE ; + } else { + SignedSatQ70__5 = asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse18__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) [ 0 +: 16 ] ; + SignedSatQ71__5 = FALSE ; + } + } + if SignedSatQ71__5 then { + FPSR = append_bits.0 {{ 4,28 }} ( FPSR [ 28 +: 4 ],append_bits.0 {{ 1,27 }} ( '1',FPSR [ 0 +: 27 ] ) ) ; + } + bits ( 16 ) SignedSatQ83__5 ; + boolean SignedSatQ84__5 ; + if slt_bits.0 {{ 33 }} ( '000000000000000000111111111111111',asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse12__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) ) then { + SignedSatQ83__5 = '0111111111111111' ; + SignedSatQ84__5 = TRUE ; + } else { + if slt_bits.0 {{ 33 }} ( asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse12__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ),'111111111111111111000000000000000' ) then { + SignedSatQ83__5 = '1000000000000000' ; + SignedSatQ84__5 = TRUE ; + } else { + SignedSatQ83__5 = asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse12__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) [ 0 +: 16 ] ; + SignedSatQ84__5 = FALSE ; + } + } + if SignedSatQ84__5 then { + FPSR = append_bits.0 {{ 4,28 }} ( FPSR [ 28 +: 4 ],append_bits.0 {{ 1,27 }} ( '1',FPSR [ 0 +: 27 ] ) ) ; + } + bits ( 16 ) SignedSatQ96__5 ; + boolean SignedSatQ97__5 ; + if slt_bits.0 {{ 33 }} ( '000000000000000000111111111111111',asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse6__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) ) then { + SignedSatQ96__5 = '0111111111111111' ; + SignedSatQ97__5 = TRUE ; + } else { + if slt_bits.0 {{ 33 }} ( asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse6__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ),'111111111111111111000000000000000' ) then { + SignedSatQ96__5 = '1000000000000000' ; + SignedSatQ97__5 = TRUE ; + } else { + SignedSatQ96__5 = asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse6__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) [ 0 +: 16 ] ; + SignedSatQ97__5 = FALSE ; + } + } + if SignedSatQ97__5 then { + FPSR = append_bits.0 {{ 4,28 }} ( FPSR [ 28 +: 4 ],append_bits.0 {{ 1,27 }} ( '1',FPSR [ 0 +: 27 ] ) ) ; + } + bits ( 16 ) SignedSatQ109__5 ; + boolean SignedSatQ110__5 ; + if slt_bits.0 {{ 33 }} ( '000000000000000000111111111111111',asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse0__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) ) then { + SignedSatQ109__5 = '0111111111111111' ; + SignedSatQ110__5 = TRUE ; + } else { + if slt_bits.0 {{ 33 }} ( asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse0__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ),'111111111111111111000000000000000' ) then { + SignedSatQ109__5 = '1000000000000000' ; + SignedSatQ110__5 = TRUE ; + } else { + SignedSatQ109__5 = asr_bits.0 {{ 33,6 }} ( add_bits.0 {{ 33 }} ( mul_bits.0 {{ 33 }} ( SignExtend.0 {{ 17,33 }} ( mul_bits.0 {{ 17 }} ( '00000000000000010',Cse0__5 ),33 ),Cse42__5 ),'000000000000000001000000000000000' ),'010000' ) [ 0 +: 16 ] ; + SignedSatQ110__5 = FALSE ; + } + } + if SignedSatQ110__5 then { + FPSR = append_bits.0 {{ 4,28 }} ( FPSR [ 28 +: 4 ],append_bits.0 {{ 1,27 }} ( '1',FPSR [ 0 +: 27 ] ) ) ; + } + __array _Z [ 0 ] = append_bits.0 {{ 16,112 }} ( SignedSatQ109__5,append_bits.0 {{ 16,96 }} ( SignedSatQ96__5,append_bits.0 {{ 16,80 }} ( SignedSatQ83__5,append_bits.0 {{ 16,64 }} ( SignedSatQ70__5,append_bits.0 {{ 16,48 }} ( SignedSatQ57__5,append_bits.0 {{ 16,32 }} ( SignedSatQ44__5,append_bits.0 {{ 16,16 }} ( SignedSatQ31__5,SignedSatQ17__5 ) ) ) ) ) ) ) ; + "" + Stmt_ConstDecl(Type_Bits(17),"Cse43__5",Expr_TApply("SignExtend.0",[16;17],[Expr_Slices(Expr_Array(Expr_Var("_Z"),0),[Slice_LoWd(0,16)]);17])) + Stmt_ConstDecl(Type_Bits(17),"Cse36__5",Expr_TApply("SignExtend.0",[16;17],[Expr_Slices(Expr_Array(Expr_Var("_Z"),0),[Slice_LoWd(16,16)]);17])) + Stmt_ConstDecl(Type_Bits(17),"Cse30__5",Expr_TApply("SignExtend.0",[16;17],[Expr_Slices(Expr_Array(Expr_Var("_Z"),0),[Slice_LoWd(32,16)]);17])) + Stmt_ConstDecl(Type_Bits(17),"Cse24__5",Expr_TApply("SignExtend.0",[16;17],[Expr_Slices(Expr_Array(Expr_Var("_Z"),0),[Slice_LoWd(48,16)]);17])) + Stmt_ConstDecl(Type_Bits(17),"Cse18__5",Expr_TApply("SignExtend.0",[16;17],[Expr_Slices(Expr_Array(Expr_Var("_Z"),0),[Slice_LoWd(64,16)]);17])) + Stmt_ConstDecl(Type_Bits(17),"Cse12__5",Expr_TApply("SignExtend.0",[16;17],[Expr_Slices(Expr_Array(Expr_Var("_Z"),0),[Slice_LoWd(80,16)]);17])) + Stmt_ConstDecl(Type_Bits(17),"Cse6__5",Expr_TApply("SignExtend.0",[16;17],[Expr_Slices(Expr_Array(Expr_Var("_Z"),0),[Slice_LoWd(96,16)]);17])) + Stmt_ConstDecl(Type_Bits(17),"Cse0__5",Expr_TApply("SignExtend.0",[16;17],[Expr_Slices(Expr_Array(Expr_Var("_Z"),0),[Slice_LoWd(112,16)]);17])) + Stmt_ConstDecl(Type_Bits(33),"Cse42__5",Expr_TApply("SignExtend.0",[16;33],[Expr_Slices(Expr_Array(Expr_Var("_Z"),1),[Slice_LoWd(48,16)]);33])) + Stmt_VarDeclsNoInit(Type_Bits(16),["SignedSatQ17__5"]) + Stmt_VarDeclsNoInit(Type_Constructor("boolean"),["SignedSatQ18__5"]) + Stmt_If(Expr_TApply("slt_bits.0",[33],['000000000000000000111111111111111';Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse43__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000'])]),[ + Stmt_Assign(LExpr_Var("SignedSatQ17__5"),'0111111111111111'); + Stmt_Assign(LExpr_Var("SignedSatQ18__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_If(Expr_TApply("slt_bits.0",[33],[Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse43__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']);'111111111111111111000000000000000']),[ + Stmt_Assign(LExpr_Var("SignedSatQ17__5"),'1000000000000000'); + Stmt_Assign(LExpr_Var("SignedSatQ18__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_Assign(LExpr_Var("SignedSatQ17__5"),Expr_Slices(Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse43__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']),[Slice_LoWd(0,16)])); + Stmt_Assign(LExpr_Var("SignedSatQ18__5"),Expr_Var("FALSE")) + ]) + ]) + Stmt_If(Expr_Var("SignedSatQ18__5"),[ + Stmt_Assign(LExpr_Var("FPSR"),Expr_TApply("append_bits.0",[4;28],[Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(28,4)]);Expr_TApply("append_bits.0",[1;27],['1';Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(0,27)])])])) + ],[],[]) + Stmt_VarDeclsNoInit(Type_Bits(16),["SignedSatQ31__5"]) + Stmt_VarDeclsNoInit(Type_Constructor("boolean"),["SignedSatQ32__5"]) + Stmt_If(Expr_TApply("slt_bits.0",[33],['000000000000000000111111111111111';Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse36__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000'])]),[ + Stmt_Assign(LExpr_Var("SignedSatQ31__5"),'0111111111111111'); + Stmt_Assign(LExpr_Var("SignedSatQ32__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_If(Expr_TApply("slt_bits.0",[33],[Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse36__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']);'111111111111111111000000000000000']),[ + Stmt_Assign(LExpr_Var("SignedSatQ31__5"),'1000000000000000'); + Stmt_Assign(LExpr_Var("SignedSatQ32__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_Assign(LExpr_Var("SignedSatQ31__5"),Expr_Slices(Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse36__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']),[Slice_LoWd(0,16)])); + Stmt_Assign(LExpr_Var("SignedSatQ32__5"),Expr_Var("FALSE")) + ]) + ]) + Stmt_If(Expr_Var("SignedSatQ32__5"),[ + Stmt_Assign(LExpr_Var("FPSR"),Expr_TApply("append_bits.0",[4;28],[Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(28,4)]);Expr_TApply("append_bits.0",[1;27],['1';Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(0,27)])])])) + ],[],[]) + Stmt_VarDeclsNoInit(Type_Bits(16),["SignedSatQ44__5"]) + Stmt_VarDeclsNoInit(Type_Constructor("boolean"),["SignedSatQ45__5"]) + Stmt_If(Expr_TApply("slt_bits.0",[33],['000000000000000000111111111111111';Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse30__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000'])]),[ + Stmt_Assign(LExpr_Var("SignedSatQ44__5"),'0111111111111111'); + Stmt_Assign(LExpr_Var("SignedSatQ45__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_If(Expr_TApply("slt_bits.0",[33],[Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse30__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']);'111111111111111111000000000000000']),[ + Stmt_Assign(LExpr_Var("SignedSatQ44__5"),'1000000000000000'); + Stmt_Assign(LExpr_Var("SignedSatQ45__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_Assign(LExpr_Var("SignedSatQ44__5"),Expr_Slices(Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse30__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']),[Slice_LoWd(0,16)])); + Stmt_Assign(LExpr_Var("SignedSatQ45__5"),Expr_Var("FALSE")) + ]) + ]) + Stmt_If(Expr_Var("SignedSatQ45__5"),[ + Stmt_Assign(LExpr_Var("FPSR"),Expr_TApply("append_bits.0",[4;28],[Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(28,4)]);Expr_TApply("append_bits.0",[1;27],['1';Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(0,27)])])])) + ],[],[]) + Stmt_VarDeclsNoInit(Type_Bits(16),["SignedSatQ57__5"]) + Stmt_VarDeclsNoInit(Type_Constructor("boolean"),["SignedSatQ58__5"]) + Stmt_If(Expr_TApply("slt_bits.0",[33],['000000000000000000111111111111111';Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse24__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000'])]),[ + Stmt_Assign(LExpr_Var("SignedSatQ57__5"),'0111111111111111'); + Stmt_Assign(LExpr_Var("SignedSatQ58__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_If(Expr_TApply("slt_bits.0",[33],[Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse24__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']);'111111111111111111000000000000000']),[ + Stmt_Assign(LExpr_Var("SignedSatQ57__5"),'1000000000000000'); + Stmt_Assign(LExpr_Var("SignedSatQ58__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_Assign(LExpr_Var("SignedSatQ57__5"),Expr_Slices(Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse24__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']),[Slice_LoWd(0,16)])); + Stmt_Assign(LExpr_Var("SignedSatQ58__5"),Expr_Var("FALSE")) + ]) + ]) + Stmt_If(Expr_Var("SignedSatQ58__5"),[ + Stmt_Assign(LExpr_Var("FPSR"),Expr_TApply("append_bits.0",[4;28],[Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(28,4)]);Expr_TApply("append_bits.0",[1;27],['1';Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(0,27)])])])) + ],[],[]) + Stmt_VarDeclsNoInit(Type_Bits(16),["SignedSatQ70__5"]) + Stmt_VarDeclsNoInit(Type_Constructor("boolean"),["SignedSatQ71__5"]) + Stmt_If(Expr_TApply("slt_bits.0",[33],['000000000000000000111111111111111';Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse18__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000'])]),[ + Stmt_Assign(LExpr_Var("SignedSatQ70__5"),'0111111111111111'); + Stmt_Assign(LExpr_Var("SignedSatQ71__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_If(Expr_TApply("slt_bits.0",[33],[Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse18__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']);'111111111111111111000000000000000']),[ + Stmt_Assign(LExpr_Var("SignedSatQ70__5"),'1000000000000000'); + Stmt_Assign(LExpr_Var("SignedSatQ71__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_Assign(LExpr_Var("SignedSatQ70__5"),Expr_Slices(Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse18__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']),[Slice_LoWd(0,16)])); + Stmt_Assign(LExpr_Var("SignedSatQ71__5"),Expr_Var("FALSE")) + ]) + ]) + Stmt_If(Expr_Var("SignedSatQ71__5"),[ + Stmt_Assign(LExpr_Var("FPSR"),Expr_TApply("append_bits.0",[4;28],[Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(28,4)]);Expr_TApply("append_bits.0",[1;27],['1';Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(0,27)])])])) + ],[],[]) + Stmt_VarDeclsNoInit(Type_Bits(16),["SignedSatQ83__5"]) + Stmt_VarDeclsNoInit(Type_Constructor("boolean"),["SignedSatQ84__5"]) + Stmt_If(Expr_TApply("slt_bits.0",[33],['000000000000000000111111111111111';Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse12__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000'])]),[ + Stmt_Assign(LExpr_Var("SignedSatQ83__5"),'0111111111111111'); + Stmt_Assign(LExpr_Var("SignedSatQ84__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_If(Expr_TApply("slt_bits.0",[33],[Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse12__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']);'111111111111111111000000000000000']),[ + Stmt_Assign(LExpr_Var("SignedSatQ83__5"),'1000000000000000'); + Stmt_Assign(LExpr_Var("SignedSatQ84__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_Assign(LExpr_Var("SignedSatQ83__5"),Expr_Slices(Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse12__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']),[Slice_LoWd(0,16)])); + Stmt_Assign(LExpr_Var("SignedSatQ84__5"),Expr_Var("FALSE")) + ]) + ]) + Stmt_If(Expr_Var("SignedSatQ84__5"),[ + Stmt_Assign(LExpr_Var("FPSR"),Expr_TApply("append_bits.0",[4;28],[Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(28,4)]);Expr_TApply("append_bits.0",[1;27],['1';Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(0,27)])])])) + ],[],[]) + Stmt_VarDeclsNoInit(Type_Bits(16),["SignedSatQ96__5"]) + Stmt_VarDeclsNoInit(Type_Constructor("boolean"),["SignedSatQ97__5"]) + Stmt_If(Expr_TApply("slt_bits.0",[33],['000000000000000000111111111111111';Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse6__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000'])]),[ + Stmt_Assign(LExpr_Var("SignedSatQ96__5"),'0111111111111111'); + Stmt_Assign(LExpr_Var("SignedSatQ97__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_If(Expr_TApply("slt_bits.0",[33],[Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse6__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']);'111111111111111111000000000000000']),[ + Stmt_Assign(LExpr_Var("SignedSatQ96__5"),'1000000000000000'); + Stmt_Assign(LExpr_Var("SignedSatQ97__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_Assign(LExpr_Var("SignedSatQ96__5"),Expr_Slices(Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse6__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']),[Slice_LoWd(0,16)])); + Stmt_Assign(LExpr_Var("SignedSatQ97__5"),Expr_Var("FALSE")) + ]) + ]) + Stmt_If(Expr_Var("SignedSatQ97__5"),[ + Stmt_Assign(LExpr_Var("FPSR"),Expr_TApply("append_bits.0",[4;28],[Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(28,4)]);Expr_TApply("append_bits.0",[1;27],['1';Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(0,27)])])])) + ],[],[]) + Stmt_VarDeclsNoInit(Type_Bits(16),["SignedSatQ109__5"]) + Stmt_VarDeclsNoInit(Type_Constructor("boolean"),["SignedSatQ110__5"]) + Stmt_If(Expr_TApply("slt_bits.0",[33],['000000000000000000111111111111111';Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse0__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000'])]),[ + Stmt_Assign(LExpr_Var("SignedSatQ109__5"),'0111111111111111'); + Stmt_Assign(LExpr_Var("SignedSatQ110__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_If(Expr_TApply("slt_bits.0",[33],[Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse0__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']);'111111111111111111000000000000000']),[ + Stmt_Assign(LExpr_Var("SignedSatQ109__5"),'1000000000000000'); + Stmt_Assign(LExpr_Var("SignedSatQ110__5"),Expr_Var("TRUE")) + ],[],[ + Stmt_Assign(LExpr_Var("SignedSatQ109__5"),Expr_Slices(Expr_TApply("asr_bits.0",[33;6],[Expr_TApply("add_bits.0",[33],[Expr_TApply("mul_bits.0",[33],[Expr_TApply("SignExtend.0",[17;33],[Expr_TApply("mul_bits.0",[17],['00000000000000010';Expr_Var("Cse0__5")]);33]);Expr_Var("Cse42__5")]);'000000000000000001000000000000000']);'010000']),[Slice_LoWd(0,16)])); + Stmt_Assign(LExpr_Var("SignedSatQ110__5"),Expr_Var("FALSE")) + ]) + ]) + Stmt_If(Expr_Var("SignedSatQ110__5"),[ + Stmt_Assign(LExpr_Var("FPSR"),Expr_TApply("append_bits.0",[4;28],[Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(28,4)]);Expr_TApply("append_bits.0",[1;27],['1';Expr_Slices(Expr_Var("FPSR"),[Slice_LoWd(0,27)])])])) + ],[],[]) + Stmt_Assign(LExpr_Array(LExpr_Var("_Z"),0),Expr_TApply("append_bits.0",[16;112],[Expr_Var("SignedSatQ109__5");Expr_TApply("append_bits.0",[16;96],[Expr_Var("SignedSatQ96__5");Expr_TApply("append_bits.0",[16;80],[Expr_Var("SignedSatQ83__5");Expr_TApply("append_bits.0",[16;64],[Expr_Var("SignedSatQ70__5");Expr_TApply("append_bits.0",[16;48],[Expr_Var("SignedSatQ57__5");Expr_TApply("append_bits.0",[16;32],[Expr_Var("SignedSatQ44__5");Expr_TApply("append_bits.0",[16;16],[Expr_Var("SignedSatQ31__5");Expr_Var("SignedSatQ17__5")])])])])])])]))