From 9fb83cc3d4adfee4b12b5ee8b755c765221ed8be Mon Sep 17 00:00:00 2001 From: rina Date: Tue, 12 Mar 2024 16:19:35 +1000 Subject: [PATCH] aslt: quote ident names --- libASL/asl.ott | 2 +- tests/aslt/test_dis.t | 94 +++++++++++++++++++++---------------------- 2 files changed, 48 insertions(+), 48 deletions(-) diff --git a/libASL/asl.ott b/libASL/asl.ott index 75d2d729..0e530849 100644 --- a/libASL/asl.ott +++ b/libASL/asl.ott @@ -175,7 +175,7 @@ ident :: '' ::= {{ phantom }} {{ ocaml ident }} {{ com Identifier }} {{ pp l = PPrint.string (pprint_ident l) }} - {{ pp-raw l = PPrint.string (pprint_ident l) }} + {{ pp-raw l = PPrint.string ("\"" ^ pprint_ident l ^ "\"") }} | id :: :: Ident {{ ocaml Ident [[id]] }} typeident :: '' ::= {{ phantom }} diff --git a/tests/aslt/test_dis.t b/tests/aslt/test_dis.t index 53b3afaa..9291049e 100644 --- a/tests/aslt/test_dis.t +++ b/tests/aslt/test_dis.t @@ -28,19 +28,19 @@ note: concatenate all commands to avoid aslp startup overhead PSTATE . N = Cse0__5 [ 63 +: 1 ] ; __array _R [ 1 ] = Cse0__5 ; "" - Stmt_ConstDecl(Type_Bits(Expr_LitInt("64")),Cse0__5,Expr_TApply(add_bits.0,[(Expr_LitInt("64"))],[(Expr_Array(Expr_Var(_R),Expr_LitInt("2")));(Expr_Array(Expr_Var(_R),Expr_LitInt("3")))])) - Stmt_Assign(LExpr_Field(LExpr_Var(PSTATE),V),Expr_TApply(not_bits.0,[(Expr_LitInt("1"))],[(Expr_TApply(cvt_bool_bv.0,[],[(Expr_TApply(eq_bits.0,[(Expr_LitInt("65"))],[(Expr_TApply(SignExtend.0,[(Expr_LitInt("64"));(Expr_LitInt("65"))],[(Expr_Var(Cse0__5));(Expr_LitInt("65"))]));(Expr_TApply(add_bits.0,[(Expr_LitInt("65"))],[(Expr_TApply(SignExtend.0,[(Expr_LitInt("64"));(Expr_LitInt("65"))],[(Expr_Array(Expr_Var(_R),Expr_LitInt("2")));(Expr_LitInt("65"))]));(Expr_TApply(SignExtend.0,[(Expr_LitInt("64"));(Expr_LitInt("65"))],[(Expr_Array(Expr_Var(_R),Expr_LitInt("3")));(Expr_LitInt("65"))]))]))]))]))])) - Stmt_Assign(LExpr_Field(LExpr_Var(PSTATE),C),Expr_TApply(not_bits.0,[(Expr_LitInt("1"))],[(Expr_TApply(cvt_bool_bv.0,[],[(Expr_TApply(eq_bits.0,[(Expr_LitInt("65"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("64"));(Expr_LitInt("65"))],[(Expr_Var(Cse0__5));(Expr_LitInt("65"))]));(Expr_TApply(add_bits.0,[(Expr_LitInt("65"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("64"));(Expr_LitInt("65"))],[(Expr_Array(Expr_Var(_R),Expr_LitInt("2")));(Expr_LitInt("65"))]));(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("64"));(Expr_LitInt("65"))],[(Expr_Array(Expr_Var(_R),Expr_LitInt("3")));(Expr_LitInt("65"))]))]))]))]))])) - Stmt_Assign(LExpr_Field(LExpr_Var(PSTATE),Z),Expr_TApply(cvt_bool_bv.0,[],[(Expr_TApply(eq_bits.0,[(Expr_LitInt("64"))],[(Expr_Var(Cse0__5));(Expr_LitBits("0000000000000000000000000000000000000000000000000000000000000000"))]))])) - Stmt_Assign(LExpr_Field(LExpr_Var(PSTATE),N),Expr_Slices(Expr_Var(Cse0__5),[(Slice_LoWd(Expr_LitInt("63"),Expr_LitInt("1")))])) - Stmt_Assign(LExpr_Array(LExpr_Var(_R),Expr_LitInt("1")),Expr_Var(Cse0__5)) + Stmt_ConstDecl(Type_Bits(Expr_LitInt("64")),"Cse0__5",Expr_TApply("add_bits.0",[(Expr_LitInt("64"))],[(Expr_Array(Expr_Var("_R"),Expr_LitInt("2")));(Expr_Array(Expr_Var("_R"),Expr_LitInt("3")))])) + Stmt_Assign(LExpr_Field(LExpr_Var("PSTATE"),V),Expr_TApply("not_bits.0",[(Expr_LitInt("1"))],[(Expr_TApply("cvt_bool_bv.0",[],[(Expr_TApply("eq_bits.0",[(Expr_LitInt("65"))],[(Expr_TApply("SignExtend.0",[(Expr_LitInt("64"));(Expr_LitInt("65"))],[(Expr_Var("Cse0__5"));(Expr_LitInt("65"))]));(Expr_TApply("add_bits.0",[(Expr_LitInt("65"))],[(Expr_TApply("SignExtend.0",[(Expr_LitInt("64"));(Expr_LitInt("65"))],[(Expr_Array(Expr_Var("_R"),Expr_LitInt("2")));(Expr_LitInt("65"))]));(Expr_TApply("SignExtend.0",[(Expr_LitInt("64"));(Expr_LitInt("65"))],[(Expr_Array(Expr_Var("_R"),Expr_LitInt("3")));(Expr_LitInt("65"))]))]))]))]))])) + Stmt_Assign(LExpr_Field(LExpr_Var("PSTATE"),C),Expr_TApply("not_bits.0",[(Expr_LitInt("1"))],[(Expr_TApply("cvt_bool_bv.0",[],[(Expr_TApply("eq_bits.0",[(Expr_LitInt("65"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("64"));(Expr_LitInt("65"))],[(Expr_Var("Cse0__5"));(Expr_LitInt("65"))]));(Expr_TApply("add_bits.0",[(Expr_LitInt("65"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("64"));(Expr_LitInt("65"))],[(Expr_Array(Expr_Var("_R"),Expr_LitInt("2")));(Expr_LitInt("65"))]));(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("64"));(Expr_LitInt("65"))],[(Expr_Array(Expr_Var("_R"),Expr_LitInt("3")));(Expr_LitInt("65"))]))]))]))]))])) + Stmt_Assign(LExpr_Field(LExpr_Var("PSTATE"),Z),Expr_TApply("cvt_bool_bv.0",[],[(Expr_TApply("eq_bits.0",[(Expr_LitInt("64"))],[(Expr_Var("Cse0__5"));(Expr_LitBits("0000000000000000000000000000000000000000000000000000000000000000"))]))])) + Stmt_Assign(LExpr_Field(LExpr_Var("PSTATE"),N),Expr_Slices(Expr_Var("Cse0__5"),[(Slice_LoWd(Expr_LitInt("63"),Expr_LitInt("1")))])) + Stmt_Assign(LExpr_Array(LExpr_Var("_R"),Expr_LitInt("1")),Expr_Var("Cse0__5")) " 0xd10083ff " Decoding instruction A64 d10083ff SP_EL0 = add_bits.0 {{ 64 }} ( SP_EL0,'1111111111111111111111111111111111111111111111111111111111100000' ) ; "" - Stmt_Assign(LExpr_Var(SP_EL0),Expr_TApply(add_bits.0,[(Expr_LitInt("64"))],[(Expr_Var(SP_EL0));(Expr_LitBits("1111111111111111111111111111111111111111111111111111111111100000"))])) + Stmt_Assign(LExpr_Var("SP_EL0"),Expr_TApply("add_bits.0",[(Expr_LitInt("64"))],[(Expr_Var("SP_EL0"));(Expr_LitBits("1111111111111111111111111111111111111111111111111111111111100000"))])) " 0x1e630040 " @@ -50,17 +50,17 @@ note: concatenate all commands to avoid aslp startup overhead constant bits ( 64 ) Exp9__5 = FixedToFP.0 {{ 32,64 }} ( __array _R [ 2 ] [ 0 +: 32 ],0,TRUE,FPCR,cvt_bits_uint.0 {{ 3 }} ( FPDecodeRounding5__5 ) ) ; __array _Z [ 0 ] = ZeroExtend.0 {{ 64,128 }} ( Exp9__5,128 ) ; "" - Stmt_VarDeclsNoInit(Type_Bits(Expr_LitInt("3")),[(FPDecodeRounding5__5)]) - Stmt_Assign(LExpr_Var(FPDecodeRounding5__5),Expr_TApply(ZeroExtend.0,[(Expr_LitInt("2"));(Expr_LitInt("3"))],[(Expr_Slices(Expr_Var(FPCR),[(Slice_LoWd(Expr_LitInt("22"),Expr_LitInt("2")))]));(Expr_LitInt("3"))])) - Stmt_ConstDecl(Type_Bits(Expr_LitInt("64")),Exp9__5,Expr_TApply(FixedToFP.0,[(Expr_LitInt("32"));(Expr_LitInt("64"))],[(Expr_Slices(Expr_Array(Expr_Var(_R),Expr_LitInt("2")),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("32")))]));(Expr_LitInt("0"));(Expr_Var(TRUE));(Expr_Var(FPCR));(Expr_TApply(cvt_bits_uint.0,[(Expr_LitInt("3"))],[(Expr_Var(FPDecodeRounding5__5))]))])) - Stmt_Assign(LExpr_Array(LExpr_Var(_Z),Expr_LitInt("0")),Expr_TApply(ZeroExtend.0,[(Expr_LitInt("64"));(Expr_LitInt("128"))],[(Expr_Var(Exp9__5));(Expr_LitInt("128"))])) + Stmt_VarDeclsNoInit(Type_Bits(Expr_LitInt("3")),[("FPDecodeRounding5__5")]) + Stmt_Assign(LExpr_Var("FPDecodeRounding5__5"),Expr_TApply("ZeroExtend.0",[(Expr_LitInt("2"));(Expr_LitInt("3"))],[(Expr_Slices(Expr_Var("FPCR"),[(Slice_LoWd(Expr_LitInt("22"),Expr_LitInt("2")))]));(Expr_LitInt("3"))])) + Stmt_ConstDecl(Type_Bits(Expr_LitInt("64")),"Exp9__5",Expr_TApply("FixedToFP.0",[(Expr_LitInt("32"));(Expr_LitInt("64"))],[(Expr_Slices(Expr_Array(Expr_Var("_R"),Expr_LitInt("2")),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("32")))]));(Expr_LitInt("0"));(Expr_Var("TRUE"));(Expr_Var("FPCR"));(Expr_TApply("cvt_bits_uint.0",[(Expr_LitInt("3"))],[(Expr_Var("FPDecodeRounding5__5"))]))])) + Stmt_Assign(LExpr_Array(LExpr_Var("_Z"),Expr_LitInt("0")),Expr_TApply("ZeroExtend.0",[(Expr_LitInt("64"));(Expr_LitInt("128"))],[(Expr_Var("Exp9__5"));(Expr_LitInt("128"))])) " 0xd53b4200 " Decoding instruction A64 d53b4200 __array _R [ 0 ] = append_bits.0 {{ 36,28 }} ( append_bits.0 {{ 32,4 }} ( '00000000000000000000000000000000',append_bits.0 {{ 3,1 }} ( append_bits.0 {{ 2,1 }} ( append_bits.0 {{ 1,1 }} ( PSTATE . N,PSTATE . Z ),PSTATE . C ),PSTATE . V ) ),'0000000000000000000000000000' ) ; "" - Stmt_Assign(LExpr_Array(LExpr_Var(_R),Expr_LitInt("0")),Expr_TApply(append_bits.0,[(Expr_LitInt("36"));(Expr_LitInt("28"))],[(Expr_TApply(append_bits.0,[(Expr_LitInt("32"));(Expr_LitInt("4"))],[(Expr_LitBits("00000000000000000000000000000000"));(Expr_TApply(append_bits.0,[(Expr_LitInt("3"));(Expr_LitInt("1"))],[(Expr_TApply(append_bits.0,[(Expr_LitInt("2"));(Expr_LitInt("1"))],[(Expr_TApply(append_bits.0,[(Expr_LitInt("1"));(Expr_LitInt("1"))],[(Expr_Field(Expr_Var(PSTATE),N));(Expr_Field(Expr_Var(PSTATE),Z))]));(Expr_Field(Expr_Var(PSTATE),C))]));(Expr_Field(Expr_Var(PSTATE),V))]))]));(Expr_LitBits("0000000000000000000000000000"))])) + Stmt_Assign(LExpr_Array(LExpr_Var("_R"),Expr_LitInt("0")),Expr_TApply("append_bits.0",[(Expr_LitInt("36"));(Expr_LitInt("28"))],[(Expr_TApply("append_bits.0",[(Expr_LitInt("32"));(Expr_LitInt("4"))],[(Expr_LitBits("00000000000000000000000000000000"));(Expr_TApply("append_bits.0",[(Expr_LitInt("3"));(Expr_LitInt("1"))],[(Expr_TApply("append_bits.0",[(Expr_LitInt("2"));(Expr_LitInt("1"))],[(Expr_TApply("append_bits.0",[(Expr_LitInt("1"));(Expr_LitInt("1"))],[(Expr_Field(Expr_Var("PSTATE"),N));(Expr_Field(Expr_Var("PSTATE"),Z))]));(Expr_Field(Expr_Var("PSTATE"),C))]));(Expr_Field(Expr_Var("PSTATE"),V))]))]));(Expr_LitBits("0000000000000000000000000000"))])) " 0x0e000000 " @@ -109,47 +109,47 @@ note: concatenate all commands to avoid aslp startup overhead } __array _Z [ 0 ] = ZeroExtend.0 {{ 64,128 }} ( result__4,128 ) ; "" - Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),Cse7__5,Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) - Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),Cse6__5,Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("8"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) - Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),Cse5__5,Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("16"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) - Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),Cse4__5,Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("24"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) - Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),Cse3__5,Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("32"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) - Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),Cse2__5,Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("40"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) - Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),Cse1__5,Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("48"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) - Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),Cse0__5,Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("56"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) - Stmt_VarDeclsNoInit(Type_Bits(Expr_LitInt("64")),[(result__4)]) - Stmt_Assign(LExpr_Var(result__4),Expr_LitBits("0000000000000000000000000000000000000000000000000000000000000000")) - Stmt_If(Expr_TApply(slt_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse7__5));(Expr_LitBits("000010000"))]),[ - Stmt_Assert(Expr_TApply(and_bool.0,[],[(Expr_TApply(sle_bits.0,[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var(Cse7__5))]));(Expr_TApply(sle_bits.0,[(Expr_LitInt("13"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("12"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply(add_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse7__5));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) - Stmt_Assign(LExpr_Var(result__4),Expr_TApply(append_bits.0,[(Expr_LitInt("56"));(Expr_LitInt("8"))],[(Expr_LitBits("00000000000000000000000000000000000000000000000000000000"));(Expr_Slices(Expr_TApply(lsr_bits.0,[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")));(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("11"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]))])) + Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),"Cse7__5",Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) + Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),"Cse6__5",Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("8"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) + Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),"Cse5__5",Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("16"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) + Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),"Cse4__5",Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("24"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) + Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),"Cse3__5",Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("32"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) + Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),"Cse2__5",Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("40"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) + Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),"Cse1__5",Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("48"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) + Stmt_ConstDecl(Type_Bits(Expr_LitInt("9")),"Cse0__5",Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("9"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("56"),Expr_LitInt("8")))]));(Expr_LitInt("9"))])) + Stmt_VarDeclsNoInit(Type_Bits(Expr_LitInt("64")),[("result__4")]) + Stmt_Assign(LExpr_Var("result__4"),Expr_LitBits("0000000000000000000000000000000000000000000000000000000000000000")) + Stmt_If(Expr_TApply("slt_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse7__5"));(Expr_LitBits("000010000"))]),[ + Stmt_Assert(Expr_TApply("and_bool.0",[],[(Expr_TApply("sle_bits.0",[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var("Cse7__5"))]));(Expr_TApply("sle_bits.0",[(Expr_LitInt("13"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("12"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply("add_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse7__5"));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) + Stmt_Assign(LExpr_Var("result__4"),Expr_TApply("append_bits.0",[(Expr_LitInt("56"));(Expr_LitInt("8"))],[(Expr_LitBits("00000000000000000000000000000000000000000000000000000000"));(Expr_Slices(Expr_TApply("lsr_bits.0",[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")));(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("11"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]))])) ],[],[]) - Stmt_If(Expr_TApply(slt_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse6__5));(Expr_LitBits("000010000"))]),[ - Stmt_Assert(Expr_TApply(and_bool.0,[],[(Expr_TApply(sle_bits.0,[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var(Cse6__5))]));(Expr_TApply(sle_bits.0,[(Expr_LitInt("13"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("12"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply(add_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse6__5));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) - Stmt_Assign(LExpr_Var(result__4),Expr_TApply(append_bits.0,[(Expr_LitInt("48"));(Expr_LitInt("16"))],[(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("16"),Expr_LitInt("48")))]));(Expr_TApply(append_bits.0,[(Expr_LitInt("8"));(Expr_LitInt("8"))],[(Expr_Slices(Expr_TApply(lsr_bits.0,[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")));(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("11"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("8"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]))]))])) + Stmt_If(Expr_TApply("slt_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse6__5"));(Expr_LitBits("000010000"))]),[ + Stmt_Assert(Expr_TApply("and_bool.0",[],[(Expr_TApply("sle_bits.0",[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var("Cse6__5"))]));(Expr_TApply("sle_bits.0",[(Expr_LitInt("13"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("12"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply("add_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse6__5"));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) + Stmt_Assign(LExpr_Var("result__4"),Expr_TApply("append_bits.0",[(Expr_LitInt("48"));(Expr_LitInt("16"))],[(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("16"),Expr_LitInt("48")))]));(Expr_TApply("append_bits.0",[(Expr_LitInt("8"));(Expr_LitInt("8"))],[(Expr_Slices(Expr_TApply("lsr_bits.0",[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")));(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("11"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("8"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]))]))])) ],[],[]) - Stmt_If(Expr_TApply(slt_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse5__5));(Expr_LitBits("000010000"))]),[ - Stmt_Assert(Expr_TApply(and_bool.0,[],[(Expr_TApply(sle_bits.0,[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var(Cse5__5))]));(Expr_TApply(sle_bits.0,[(Expr_LitInt("13"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("12"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply(add_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse5__5));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) - Stmt_Assign(LExpr_Var(result__4),Expr_TApply(append_bits.0,[(Expr_LitInt("40"));(Expr_LitInt("24"))],[(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("24"),Expr_LitInt("40")))]));(Expr_TApply(append_bits.0,[(Expr_LitInt("8"));(Expr_LitInt("16"))],[(Expr_Slices(Expr_TApply(lsr_bits.0,[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")));(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("11"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("16"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("16")))]))]))])) + Stmt_If(Expr_TApply("slt_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse5__5"));(Expr_LitBits("000010000"))]),[ + Stmt_Assert(Expr_TApply("and_bool.0",[],[(Expr_TApply("sle_bits.0",[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var("Cse5__5"))]));(Expr_TApply("sle_bits.0",[(Expr_LitInt("13"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("12"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply("add_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse5__5"));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) + Stmt_Assign(LExpr_Var("result__4"),Expr_TApply("append_bits.0",[(Expr_LitInt("40"));(Expr_LitInt("24"))],[(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("24"),Expr_LitInt("40")))]));(Expr_TApply("append_bits.0",[(Expr_LitInt("8"));(Expr_LitInt("16"))],[(Expr_Slices(Expr_TApply("lsr_bits.0",[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")));(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("11"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("16"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("16")))]))]))])) ],[],[]) - Stmt_If(Expr_TApply(slt_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse4__5));(Expr_LitBits("000010000"))]),[ - Stmt_Assert(Expr_TApply(and_bool.0,[],[(Expr_TApply(sle_bits.0,[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var(Cse4__5))]));(Expr_TApply(sle_bits.0,[(Expr_LitInt("13"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("12"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply(add_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse4__5));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) - Stmt_Assign(LExpr_Var(result__4),Expr_TApply(append_bits.0,[(Expr_LitInt("32"));(Expr_LitInt("32"))],[(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("32"),Expr_LitInt("32")))]));(Expr_TApply(append_bits.0,[(Expr_LitInt("8"));(Expr_LitInt("24"))],[(Expr_Slices(Expr_TApply(lsr_bits.0,[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")));(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("11"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("24"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("24")))]))]))])) + Stmt_If(Expr_TApply("slt_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse4__5"));(Expr_LitBits("000010000"))]),[ + Stmt_Assert(Expr_TApply("and_bool.0",[],[(Expr_TApply("sle_bits.0",[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var("Cse4__5"))]));(Expr_TApply("sle_bits.0",[(Expr_LitInt("13"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("12"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply("add_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse4__5"));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) + Stmt_Assign(LExpr_Var("result__4"),Expr_TApply("append_bits.0",[(Expr_LitInt("32"));(Expr_LitInt("32"))],[(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("32"),Expr_LitInt("32")))]));(Expr_TApply("append_bits.0",[(Expr_LitInt("8"));(Expr_LitInt("24"))],[(Expr_Slices(Expr_TApply("lsr_bits.0",[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")));(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("11"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("24"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("24")))]))]))])) ],[],[]) - Stmt_If(Expr_TApply(slt_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse3__5));(Expr_LitBits("000010000"))]),[ - Stmt_Assert(Expr_TApply(and_bool.0,[],[(Expr_TApply(sle_bits.0,[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var(Cse3__5))]));(Expr_TApply(sle_bits.0,[(Expr_LitInt("13"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("12"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply(add_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse3__5));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) - Stmt_Assign(LExpr_Var(result__4),Expr_TApply(append_bits.0,[(Expr_LitInt("24"));(Expr_LitInt("40"))],[(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("40"),Expr_LitInt("24")))]));(Expr_TApply(append_bits.0,[(Expr_LitInt("8"));(Expr_LitInt("32"))],[(Expr_Slices(Expr_TApply(lsr_bits.0,[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")));(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("11"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("32"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("32")))]))]))])) + Stmt_If(Expr_TApply("slt_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse3__5"));(Expr_LitBits("000010000"))]),[ + Stmt_Assert(Expr_TApply("and_bool.0",[],[(Expr_TApply("sle_bits.0",[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var("Cse3__5"))]));(Expr_TApply("sle_bits.0",[(Expr_LitInt("13"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("12"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply("add_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse3__5"));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) + Stmt_Assign(LExpr_Var("result__4"),Expr_TApply("append_bits.0",[(Expr_LitInt("24"));(Expr_LitInt("40"))],[(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("40"),Expr_LitInt("24")))]));(Expr_TApply("append_bits.0",[(Expr_LitInt("8"));(Expr_LitInt("32"))],[(Expr_Slices(Expr_TApply("lsr_bits.0",[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")));(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("11"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("32"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("32")))]))]))])) ],[],[]) - Stmt_If(Expr_TApply(slt_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse2__5));(Expr_LitBits("000010000"))]),[ - Stmt_Assert(Expr_TApply(and_bool.0,[],[(Expr_TApply(sle_bits.0,[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var(Cse2__5))]));(Expr_TApply(sle_bits.0,[(Expr_LitInt("13"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("12"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply(add_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse2__5));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) - Stmt_Assign(LExpr_Var(result__4),Expr_TApply(append_bits.0,[(Expr_LitInt("16"));(Expr_LitInt("48"))],[(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("48"),Expr_LitInt("16")))]));(Expr_TApply(append_bits.0,[(Expr_LitInt("8"));(Expr_LitInt("40"))],[(Expr_Slices(Expr_TApply(lsr_bits.0,[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")));(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("11"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("40"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("40")))]))]))])) + Stmt_If(Expr_TApply("slt_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse2__5"));(Expr_LitBits("000010000"))]),[ + Stmt_Assert(Expr_TApply("and_bool.0",[],[(Expr_TApply("sle_bits.0",[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var("Cse2__5"))]));(Expr_TApply("sle_bits.0",[(Expr_LitInt("13"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("12"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply("add_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse2__5"));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) + Stmt_Assign(LExpr_Var("result__4"),Expr_TApply("append_bits.0",[(Expr_LitInt("16"));(Expr_LitInt("48"))],[(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("48"),Expr_LitInt("16")))]));(Expr_TApply("append_bits.0",[(Expr_LitInt("8"));(Expr_LitInt("40"))],[(Expr_Slices(Expr_TApply("lsr_bits.0",[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")));(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("11"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("40"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("40")))]))]))])) ],[],[]) - Stmt_If(Expr_TApply(slt_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse1__5));(Expr_LitBits("000010000"))]),[ - Stmt_Assert(Expr_TApply(and_bool.0,[],[(Expr_TApply(sle_bits.0,[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var(Cse1__5))]));(Expr_TApply(sle_bits.0,[(Expr_LitInt("13"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("12"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply(add_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse1__5));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) - Stmt_Assign(LExpr_Var(result__4),Expr_TApply(append_bits.0,[(Expr_LitInt("8"));(Expr_LitInt("56"))],[(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("56"),Expr_LitInt("8")))]));(Expr_TApply(append_bits.0,[(Expr_LitInt("8"));(Expr_LitInt("48"))],[(Expr_Slices(Expr_TApply(lsr_bits.0,[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")));(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("11"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("48"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("48")))]))]))])) + Stmt_If(Expr_TApply("slt_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse1__5"));(Expr_LitBits("000010000"))]),[ + Stmt_Assert(Expr_TApply("and_bool.0",[],[(Expr_TApply("sle_bits.0",[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var("Cse1__5"))]));(Expr_TApply("sle_bits.0",[(Expr_LitInt("13"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("12"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply("add_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse1__5"));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) + Stmt_Assign(LExpr_Var("result__4"),Expr_TApply("append_bits.0",[(Expr_LitInt("8"));(Expr_LitInt("56"))],[(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("56"),Expr_LitInt("8")))]));(Expr_TApply("append_bits.0",[(Expr_LitInt("8"));(Expr_LitInt("48"))],[(Expr_Slices(Expr_TApply("lsr_bits.0",[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")));(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("11"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("48"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("48")))]))]))])) ],[],[]) - Stmt_If(Expr_TApply(slt_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse0__5));(Expr_LitBits("000010000"))]),[ - Stmt_Assert(Expr_TApply(and_bool.0,[],[(Expr_TApply(sle_bits.0,[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var(Cse0__5))]));(Expr_TApply(sle_bits.0,[(Expr_LitInt("13"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("12"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply(add_bits.0,[(Expr_LitInt("9"))],[(Expr_Var(Cse0__5));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) - Stmt_Assign(LExpr_Var(result__4),Expr_TApply(append_bits.0,[(Expr_LitInt("8"));(Expr_LitInt("56"))],[(Expr_Slices(Expr_TApply(lsr_bits.0,[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")));(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply(mul_bits.0,[(Expr_LitInt("11"))],[(Expr_TApply(ZeroExtend.0,[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var(_Z),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("56"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var(result__4),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("56")))]))])) + Stmt_If(Expr_TApply("slt_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse0__5"));(Expr_LitBits("000010000"))]),[ + Stmt_Assert(Expr_TApply("and_bool.0",[],[(Expr_TApply("sle_bits.0",[(Expr_LitInt("9"))],[(Expr_LitBits("000000000"));(Expr_Var("Cse0__5"))]));(Expr_TApply("sle_bits.0",[(Expr_LitInt("13"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("12"));(Expr_LitInt("13"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("12"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("9"));(Expr_LitInt("12"))],[(Expr_TApply("add_bits.0",[(Expr_LitInt("9"))],[(Expr_Var("Cse0__5"));(Expr_LitBits("000000001"))]));(Expr_LitInt("12"))]));(Expr_LitBits("000000001000"))]));(Expr_LitInt("13"))]));(Expr_LitBits("0000010000000"))]))])) + Stmt_Assign(LExpr_Var("result__4"),Expr_TApply("append_bits.0",[(Expr_LitInt("8"));(Expr_LitInt("56"))],[(Expr_Slices(Expr_TApply("lsr_bits.0",[(Expr_LitInt("128"));(Expr_LitInt("12"))],[(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")));(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("11"));(Expr_LitInt("12"))],[(Expr_TApply("mul_bits.0",[(Expr_LitInt("11"))],[(Expr_TApply("ZeroExtend.0",[(Expr_LitInt("8"));(Expr_LitInt("11"))],[(Expr_Slices(Expr_Array(Expr_Var("_Z"),Expr_LitInt("0")),[(Slice_LoWd(Expr_LitInt("56"),Expr_LitInt("8")))]));(Expr_LitInt("11"))]));(Expr_LitBits("00000001000"))]));(Expr_LitInt("12"))]))]),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("8")))]));(Expr_Slices(Expr_Var("result__4"),[(Slice_LoWd(Expr_LitInt("0"),Expr_LitInt("56")))]))])) ],[],[]) - Stmt_Assign(LExpr_Array(LExpr_Var(_Z),Expr_LitInt("0")),Expr_TApply(ZeroExtend.0,[(Expr_LitInt("64"));(Expr_LitInt("128"))],[(Expr_Var(result__4));(Expr_LitInt("128"))])) + Stmt_Assign(LExpr_Array(LExpr_Var("_Z"),Expr_LitInt("0")),Expr_TApply("ZeroExtend.0",[(Expr_LitInt("64"));(Expr_LitInt("128"))],[(Expr_Var("result__4"));(Expr_LitInt("128"))]))