我在很早的时候就想接触基于SMT的程序分析，近日我开始了解这个方向。 这个方面有许多的框架，文章和教程，我会一点一点深入了解。
尽管我仍然在学习这部分内容，但无论如何我并不觉得这很先进或者很高大上，相反，它是非常基础的知识，Z3（来自Microsoft Research的一个定理证明的库）对于大部分初学者来说是十分简易的。 到目前为止，我所知道的除了来自Eric的Z3Py入门教材之外，还阅读Dennis Yurichev的文章"Quick introduction into SAT/SMT solvers and symbolic execution").
在上周的发表的博客中，我演示了在不运行的情况下如何编写基本模拟器来评估函数的返回值。 在本文中，我将展示如何将数千个算术运算从晦涩的x86汇编代码转换为月简易的Z3表达式,本文主要分为三个部分：
https://yurichev.com/writings/SAT_SMT_draft-EN.pdf
http://0xeb.net/2018/02/writing-a-simple-x86-emulator-with-idapython/
http://ericpony.github.io/z3py-tutorial/guide-examples.htm
简介本文的测试程序和上周的测试程序很类似，由主函数调用的12个挑战函数。每个挑战函数都是随机生成的，因此它包含随eax、ebx 、ecx、edx寄存器（以及立即数）一起工作的add、sub、dec、inc指令的随机序列。示例程序在附件中可以下载。下面是第一个挑战函数的汇编代码：
//-------------------------------------------------------------------------
uint32_t challenge_1(uint32_t c1, uint32_t c2, uint32_t c3, uint32_t c4) // 1953 operation(s)
{
uint32_t result;
__asm
{
pushad
mov eax, [c1]
mov edx, [c2]
mov ecx, [c3]
mov ebx, [c4]
sub eax, ebx
inc ebx
sub ebx, ecx
sub ecx, 0x852e4867
add ebx, ebx
inc ecx
add eax, edx
add ecx, ebx
sub ecx, ebx
inc ecx
sub ebx, edx
add eax, 0x7a20f9e6
add ebx, 0xaa5a1584
add edx, edx
sub ebx, 0x1ca0a567
sub eax, 0xf94f7d8c
inc ecx
inc eax
add edx, eax
sub ebx, edx
inc ebx
sub edx, 0xd68a9fa7
inc ebx
inc eax
inc eax
.
.
...1000+ instructions later...
.
sub ebx, edx
inc eax
sub ebx, edx
sub ecx, eax
add eax, ebx
add ecx, 0xd2cb013d
add ecx, 0xda9d6a2e
add edx, eax
sub edx, 0x25ebd85d
add ebx, ebx
add ebx, 0x936e2259
inc eax
add eax, ecx
add ebx, 0xc0c1aa
inc ebx
add edx, 0x921ee6d5
add edx, edx
add ecx, eax
add ecx, eax
inc ebx
sub ebx, edx
add ebx, eax
inc ebx
sub eax, 0xd9d2f9c2
add edx, eax
inc ecx
add ecx, 0xad2e6bb0
add ecx, eax
sub ecx, ebx
add ebx, eax
sub ecx, 0xe2786d0c
add eax, ebx
add eax, ecx
add eax, edx
mov dword ptr [result], eax
popad
}
return result;
}
//-------------------------------------------------------------------------
uint32_t challenge_1(uint32_t c1, uint32_t c2, uint32_t c3, uint32_t c4) // 1953 operation(s)
{
uint32_t result;
__asm
{
pushad
mov eax, [c1]
mov edx, [c2]
mov ecx, [c3]
mov ebx, [c4]
sub eax, ebx
inc ebx
sub ebx, ecx
sub ecx, 0x852e4867
add ebx, ebx
inc ecx
add eax, edx
add ecx, ebx
sub ecx, ebx
inc ecx
sub ebx, edx
add eax, 0x7a20f9e6
add ebx, 0xaa5a1584
add edx, edx
sub ebx, 0x1ca0a567
sub eax, 0xf94f7d8c
inc ecx
inc eax
add edx, eax
sub ebx, edx
inc ebx
sub edx, 0xd68a9fa7
inc ebx
inc eax
inc eax
.
.
...1000+ instructions later...
.
sub ebx, edx
inc eax
sub ebx, edx
sub ecx, eax
add eax, ebx
add ecx, 0xd2cb013d
add ecx, 0xda9d6a2e
add edx, eax
sub edx, 0x25ebd85d
add ebx, ebx
add ebx, 0x936e2259
inc eax
add eax, ecx
add ebx, 0xc0c1aa
inc ebx
add edx, 0x921ee6d5
add edx, edx
add ecx, eax
add ecx, eax
inc ebx
sub ebx, edx
add ebx, eax
inc ebx
sub eax, 0xd9d2f9c2
add edx, eax
inc ecx
add ecx, 0xad2e6bb0
add ecx, eax
sub ecx, ebx
add ebx, eax
sub ecx, 0xe2786d0c
add eax, ebx
add eax, ecx
add eax, edx
mov dword ptr [result], eax
popad
}
return result;
}
上面函数的汇编代码看起来很相似，分析不出什么东西，所以这里就不去分析了，直接使用F5大法查看伪代码：
int __cdecl challenge_1(unsigned int c1, unsigned int c2, unsigned int c3, unsigned int c4)
{
unsigned int v4; // edx
unsigned int v5; // ebx
unsigned int v6; // ecx
unsigned int v7; // eax
int v8; // ecx
int v9; // eax
int v10; // edx
int v11; // ebx
int v12; // ecx
int v13; // eax
int v14; // ebx
int v15; // edx
int v16; // eax
int v17; // ebx
int v18; // ecx
int v19; // edx
int v20; // ecx
int v21; // edx
int v22; // eax
int v23; // ebx
int v24; // edx
int v25; // eax
int v26; // ecx
int v27; // edx
int v28; // ecx
int v29; // edx
int v30; // eax
int v31; // ebx
int v32; // ecx
int v33; // eax
int v34; // edx
int v35; // ecx
int v36; // ebx
int v37; // edx
int v38; // ecx
int v39; // eax
int v40; // ebx
int v41; // ecx
int v42; // eax
int v43; // edx
int v44; // ebx
int v45; // ebx
int v46; // edx
int v47; // ecx
int v48; // eax
int v49; // edx
int v50; // ebx
int v51; // eax
int v52; // edx
int v53; // ebx
int v54; // eax
int v55; // edx
int v56; // ecx
int v57; // ecx
int v58; // eax
int v59; // edx
int v60; // eax
int v61; // ebx
int v62; // eax
int v63; // ebx
int v64; // ecx
int v65; // eax
int v66; // edx
int v67; // ecx
int v68; // ebx
int v69; // edx
int v70; // ebx
int v71; // edx
int v72; // ecx
int v73; // eax
int v74; // ecx
int v75; // edx
int v76; // ebx
int v77; // edx
int v78; // edx
int v79; // eax
int v80; // ebx
int v81; // ecx
int v82; // ebx
int v83; // eax
int v84; // ebx
int v85; // edx
int v86; // ebx
int v87; // eax
int v88; // edx
int v89; // ecx
int v90; // eax
int v91; // edx
int v92; // ebx
int v93; // ecx
int v94; // ebx
int v95; // eax
int v96; // ecx
int v97; // ecx
int v98; // ebx
int v99; // ecx
int v100; // eax
int v101; // edx
int v102; // ebx
int v103; // edx
int v104; // edx
int v105; // ecx
int v106; // eax
int v107; // ecx
int v108; // edx
int v109; // eax
int v110; // edx
int v111; // eax
int v112; // ebx
int v113; // ecx
int v114; // edx
int v115; // eax
int v116; // edx
int v117; // ecx
int v118; // ebx
int v119; // eax
int v120; // ecx
int v121; // edx
int v122; // edx
int v123; // eax
int v124; // edx
int v125; // ebx
int v126; // eax
int v127; // edx
int v128; // ecx
int v129; // ebx
int v130; // edx
int v131; // ebx
int v132; // ecx
int v133; // ebx
int v134; // ebx
int v135; // eax
int v136; // ecx
int v137; // ebx
int v138; // ebx
int v139; // edx
int v140; // ecx
int v141; // ebx
int v142; // eax
int v143; // ecx
int v144; // ebx
int v145; // edx
int v146; // ebx
int v147; // edx
int v148; // ecx
int v149; // eax
int v150; // ebx
int v151; // ecx
int v152; // ebx
int v153; // edx
int v154; // eax
int v155; // edx
int v156; // ebx
int v157; // edx
int v158; // ebx
int v159; // ecx
int v160; // ebx
int v161; // eax
int v162; // ecx
int v163; // ebx
int v164; // edx
int v165; // eax
int v166; // ecx
int v167; // eax
int v168; // edx
int v169; // ebx
int v170; // ecx
int v171; // eax
int v172; // ecx
int v173; // ebx
int v174; // ecx
int v175; // edx
int v176; // ebx
int v177; // ebx
int v178; // eax
int v179; // edx
int v180; // ecx
int v181; // eax
int v182; // edx
int v183; // eax
int v184; // eax
int v185; // ebx
int v186; // ecx
int v187; // ebx
int v188; // edx
int v189; // ecx
int v190; // ebx
int v191; // eax
int v192; // ecx
int v193; // eax
int v194; // edx
int v195; // ecx
int v196; // edx
int v197; // ecx
int v198; // eax
int v199; // edx
int v200; // eax
int v201; // ecx
int v202; // ebx
int v203; // eax
int v204; // ebx
int v205; // eax
int v206; // ecx
int v207; // edx
int v208; // ebx
int v209; // eax
int v210; // edx
int v211; // eax
int v212; // eax
int v213; // ecx
int v214; // ebx
int v215; // edx
int v216; // ecx
int v217; // edx
int v218; // ebx
int v219; // eax
int v220; // ecx
int v221; // eax
int v222; // ebx
int v223; // eax
int v224; // ecx
int v225; // ecx
int v226; // ebx
int v227; // eax
int v228; // ebx
int v229; // ecx
int v230; // edx
int v231; // eax
int v232; // ecx
int v233; // edx
int v234; // ecx
int v235; // edx
int v236; // edx
int v237; // ecx
int v238; // eax
int v239; // ebx
int v240; // edx
int v241; // ebx
int v242; // edx
int v243; // ebx
int v244; // eax
int v245; // ecx
int v246; // eax
int v247; // edx
int v248; // eax
int v249; // ebx
int v250; // ecx
int v251; // eax
int v252; // ecx
int v253; // ebx
int v254; // ecx
int v255; // edx
int v256; // eax
int v257; // edx
int v258; // ecx
int v259; // eax
int v260; // edx
int v261; // ebx
int v262; // ecx
int v263; // ecx
int v264; // eax
int v265; // edx
int v266; // eax
int v267; // ecx
int v268; // ebx
int v269; // edx
int v270; // eax
int v271; // ebx
int v272; // edx
int v273; // eax
int v274; // ecx
int v275; // ebx
int v276; // ecx
int v277; // eax
int v278; // edx
int v279; // ecx
int v280; // edx
int v281; // eax
int v282; // ecx
int v283; // ebx
int v284; // eax
int v285; // edx
int v286; // ebx
int v287; // eax
int v288; // ecx
int v289; // eax
int v290; // ebx
int v291; // eax
int v292; // ecx
int v293; // ebx
int v294; // edx
int v295; // eax
int v296; // ebx
int v297; // ecx
int v298; // edx
int v299; // ebx
int v300; // eax
int v301; // ebx
int v302; // eax
int v303; // ebx
int v304; // edx
int v305; // eax
int v306; // ecx
int v307; // eax
int v308; // ebx
int v309; // ecx
int v310; // ebx
int v311; // ecx
int v312; // ebx
int v313; // ecx
int v314; // edx
int v315; // eax
int v316; // edx
int v317; // ebx
int v318; // ecx
int v319; // eax
int v320; // edx
int v321; // ebx
int v322; // ecx
int v323; // edx
int v324; // ebx
int v325; // edx
int v326; // eax
int v327; // edx
int v328; // ebx
int v329; // eax
int v330; // eax
int v331; // eax
int v332; // edx
int v333; // ebx
int v334; // eax
int v335; // ecx
int v336; // ebx
int v337; // ecx
int v338; // eax
int v339; // ecx
int v340; // ebx
int v341; // ecx
int v342; // eax
int v343; // ecx
int v344; // eax
int v345; // ebx
int v346; // eax
int v347; // eax
int v348; // ecx
int v349; // eax
int v350; // ecx
int v351; // ebx
int v352; // edx
int v353; // eax
int v354; // ecx
int v355; // ebx
int v356; // edx
int v357; // ebx
int v358; // edx
int v359; // eax
int v360; // ebx
int v361; // edx
int v362; // ecx
int v363; // eax
int v364; // ebx
int v365; // ecx
int v366; // ebx
int v367; // ecx
int v368; // ebx
int v369; // ecx
int v370; // edx
int v371; // eax
int v372; // edx
int v373; // ecx
int v374; // eax
int v375; // edx
int v376; // ecx
int v377; // ebx
int v378; // eax
int v379; // edx
int v380; // ebx
int v381; // edx
int v382; // ebx
int v383; // edx
int v384; // eax
int v385; // ebx
int v386; // edx
int v387; // ecx
int v388; // eax
int v389; // edx
int v390; // ecx
int v391; // ebx
int v392; // edx
int v393; // eax
int v394; // ecx
int v395; // ebx
int v396; // edx
int v397; // ecx
int v398; // edx
int v399; // eax
int v400; // ecx
int v401; // eax
int v402; // ebx
int v403; // ecx
int v404; // eax
int v405; // edx
int v406; // ebx
int v407; // eax
int v408; // ecx
int v409; // edx
int v410; // ebx
int v411; // ebx
int v412; // ecx
int v413; // eax
int v414; // ebx
int v415; // ecx
int v416; // edx
int v417; // ecx
int v418; // ebx
int v419; // eax
int v420; // ecx
int v421; // eax
v4 = c2 + c1 - c4 - 2133754790 + 1 + 2 * c2 - 1785093898;
v5 = 2 * (c4 + 1 - c3)- c2- 1917226979- (c2+ c1 - c4 - 2133754790+ 2 * c2)+ 2- (c3+ 539193617)- v4- 350898193;
v6 = c3 + 539193617 - v5 - 879839410;
v5 += 2;
v6 += 3;
v4 += 2109602273;
v7 = 2 * (2 * (c2 + c1 - c4 - 2133754790 + 3 - (c3 + 539193617) - 1164434189 - v5 - v6) + 1);
v8 = 2 * v6 - 1873426435 - v7;
v9 = v7 - v4 + 1;
v10 = v4 - 971527202 + 730640080;
v11 = v5 + 1150557381 - v10 - 1412696239 + 1;
v12 = v11 + v8 - 396431529 + 1;
v13 = v9 + 2 - v12 + 1;
v14 = v12 + v11 + 1;
v15 = v10 + 204474460 - v13 - 1432203755;
v16 = v14 + v13 + 884313224 + 813147417;
v17 = v15 + v14 + 2;
v18 = v15 + v12 - 451236562 + 3;
v19 = v16 + v15 + 1;
v17 += 138511611;
v16 += 953411192;
v20 = v16 + v18;
v21 = v17 + 2 * (v19 + 1) + 119463169;
v17 -= 738693819;
v22 = v16 + 594867870 - v17 + 1413353867;
v23 = v17 - v22;
v22 += 520753425;
v24 = v22 + v21 + 144745048;
v25 = v24++ + v22 - 1828520841 + 1;
v26 = v20 + 3 - v24;
v27 = v24 - v26;
v28 = v27 + v26 + 763465995;
v29 = 2 * (v27 + 2);
v30 = v29 + v25 + 1017115747;
v31 = v23 - 879256061 + 1336943267 - v30;
v32 = v30 + v30 + v28 + 1689547303 - 1018772533 + 1;
v33 = v30 - v31 + 1;
v34 = v31 + v29 - v33 + 909973850;
v35 = v34 + v32 + 228062414;
v36 = v35 + v31 + 347278668;
v35 -= 720946967;
v37 = 2 * (v34 + 1 - v35);
v38 = v37 + v35 + 1;
v37 += 1888994439;
v39 = 2 * (v33 + 579771010) + 2103615418;
v40 = v36 - 276265002 - v37 + 1864035437;
v41 = v38 + 1 - v39;
v37 += 1786144130;
v42 = v39 + 1600574700 - v37;
v43 = v37 - v40;
v44 = v43 + v40 - v41 + 2105473564;
v41 *= 2;
v45 = 2 * (v44 - v41);
v46 = v43 - 1150894576 + 3;
v47 = v45 + v41 + 313221810 - v46 + 807301504;
v48 = v42 - 124125674 + 1 - v46 + 1 - v46 + 1;
v49 = v48 + v46;
v50 = v49 + v45 - 468305613 + 3 - 2100928955;
v51 = 2 * (v48 - v49 - ++v47) + 1;
v52 = v49 + 1 - v47++ + 3;
v53 = v52 + v50;
v54 = v51 - v53;
v55 = v52 - v47 + 1;
v53 -= 446157988;
v54 += 1553282976;
v56 = v54 + v53 + v47 + 1;
v53 *= 2;
v57 = v53 + v56 - 1230516346 + 1 + 1205548791;
v58 = v54 - v53 + 2128637547;
v59 = v58 + v55 + 1;
v60 = v58 - v57;
v57 += 377513439;
v61 = v53 - 799999952 - v57;
v62 = v61 + v60 + 1;
v63 = v61 - v57;
v59 += 848132728;
v64 = v57 - v63 - v59;
v65 = v59 + v62 - 2142680737 + 1764150285;
v63 += 2087876122;
v66 = v59 + 1814013069 - v63 - v64;
v67 = 2 * v64 - v65 + 1132472947;
v68 = v63 - 788948114 + 1 - v67;
v69 = v68 + v68 + v66 + 1553607352;
v67 += 2;
v70 = v69 + 2 * v68 + 1518868433;
v71 = v67 + v67 + v69 - v70;
v72 = v70 + v67;
v70 += 713535814;
v73 = 2 * v65 + 1429126951 - v70;
v70 -= 173942082;
v74 = v70 + v72 - 1888550847 + 1 - 394102299;
v75 = v71 + 256237465 - v74;
v76 = v75 + v70 + 1;
v77 = v75 - v74++;
v76 += 2140073780;
v78 = 2 * (v77 - 1454905092) - 1933992509;
v79 = v76 + 2 * (v73 + 1866717529) - v74 - 1310766122 - v78;
v80 = v76 - v74;
v81 = v80 + v74;
v82 = v79 + v80;
++v81;
v83 = v82 + v79 + 1;
v78 += 1083862846;
v84 = v82 + 1 - v81 - v78;
v85 = v81 + v78;
v81 -= 614253581;
v86 = v85 + v84 - 515607244 + 238772881;
v87 = v83 + 141351837 - v81 + 1;
v88 = v86++ + v85 - 543286513 + 1674408964 - 794464384;
v89 = v81 - 623767744 + 215241888;
v90 = 2 * (v89++ + v87 + 1710998538);
v91 = v86 + v86 + v88 + 1 + 1 - v89++;
v92 = v89 + v86;
v90 -= 885178085;
v91 += 1677704898;
v93 = v90++ + v89 - 940635716;
v94 = v92 + 1 - v90;
v95 = v91 + v90 + 1 + 1841924206;
v96 = v91 + v93 + 941760921;
v91 += 2;
v97 = v96 + 1 - v91 + 1530834091;
v98 = v94 - v97 + 1;
v99 = v95 + v97 + 1699993484;
v100 = v98 + v95 + 1;
v101 = v98 + v91 - 523060265 + 1789589531;
v102 = v98 + 1281582157 - v100;
v100 += 146514254;
v103 = v101 - v99 - v100++;
v99 += 2080302551;
v104 = 2 * (v99 + v103 + 1512882559 + 1);
v105 = v99 - v100;
v104 -= 784717007;
v106 = v104++ + v100 - 1584810020 + 2;
v107 = v104 + v105 + 1;
v106 += 1065502423;
v102 += 3;
v108 = v102 + v104 - v107 - v106 + 342809982;
v107 -= 1412780444;
v109 = v108 + v106 + 1 - 858330204;
v110 = v109 + v108;
v102 -= 664953144;
v111 = v109 - 1329716196 - v102;
v112 = v102 - v107;
v111 += 1373514701;
v113 = v107 - 1346592359 + 216683527 - v111;
v114 = v111 + v110 - 288276575 + 1500011784;
v115 = v113 + v111;
v116 = v115++ + v114;
v117 = 2 * (v113 - 1163128426);
v118 = v117 + v112 - 818961183 - v115 - 593940334;
v119 = v118 + v115 + 2;
v118 += 428412235;
v120 = v117 + 3 - v118;
v121 = v116 + 4 - v118 + 1;
v118 += 894601604;
v122 = v118 + v121;
v123 = v122 + v119 + 1 + 443477999;
v124 = v123 + v122;
v125 = 2 * v118 - v123;
v126 = v124 + v123 - 2061231162;
v127 = v124 - v125;
v128 = v126 + v120 + 1485909680 + 1483310720;
v129 = v128 + v127 + v125 - 1355157173 + 1;
v130 = v128 + v127;
v128 += 2;
v131 = v129 - v128;
v130 += 1683851829;
v132 = v128 - v131 - 354913611;
v133 = v131 - v132;
v132 -= 198220312;
v134 = v133 + 172443045 - v132;
v135 = v126 + 3 - v132 - v134;
v136 = v130 + 2 * (v132 - v134) - v135 + 471821392;
v137 = v130++ + v134 - v136;
v136 += 923861112;
v138 = v130 + 2 * (v137 + 1) + 1 - 1146928935 + 1 - v136;
v139 = v138 + 2 * v130 + 1;
v140 = v136 - 1156737329 - v138 + 2 - v138 - v139;
v141 = v140 + v138 + 1;
v142 = v135 - 608570200 + 1 - v141 + 1;
v139 += 2;
v143 = v140 - 1777203220 + 1;
v144 = v139 + v141 - v142 - 440487739 + 182778494 - v143;
v145 = v139 + 966597185 - v144;
v142 += 967980219;
v146 = v144 - 1652140998 + 1;
v147 = v142 + v145 - 1363945608 + 1 - v146;
v148 = v143 - v146 + 1350186086;
v149 = 2 * (v148 + 2 * v142);
v150 = v146 + 1 - v147 - 457990213;
v151 = v148 + 1 - v150;
v152 = v150 - 504705392 + 1;
v153 = v147 + 1193758906 - v152;
v154 = v149 + 1 - v152 + 144039938 - v153;
v155 = v154 + v153;
v154 += 2;
v156 = v152 + 2078215581 - v154 + 1;
v157 = v156 + v155 - 122946150 + 301662336;
v158 = v156 - v157;
v154 += 2;
v159 = v157++ + v158 + v151 - 958001904 + 1284137460 + 1;
v160 = v154 + v158 + 1002156873 - v157 + 170108160;
v161 = v154 - 1014383826 + 161227700;
v162 = v159 - v161;
v163 = v160 - 255510393 + 376777367;
v164 = v157 - v162 + 2;
v165 = v163 + v161 - 1912551381 + 1;
v166 = v165 + v162 - v163 + 1 + 1;
v167 = v166 + v165 + 1;
v168 = v163 + v164 + 201934410 + 968132783;
v169 = v163 - v168++;
v170 = v166 - v167;
v171 = v168 + v167;
v172 = v170 - v168;
v168 += 2029379458;
v173 = v168 + v169 - 1763166604 + 1 + 1;
v171 -= 1188417209;
v174 = v172 + 1 - v173 + 1;
v175 = v174 + v168 + 2140747580 - v171 + 668304081;
v176 = v173 - 26185106 + 474549714 - v174++;
v177 = v176 - v174;
v178 = v175 + v171 + 1;
v179 = v178 + v175;
v180 = v178 + v177 + v174 + 1 + 2141394379;
v181 = v178 - 826788372 + 3;
v182 = v181 + v179 + 1;
v177 += 741838009;
v183 = v177 + v181;
v177 *= 2;
v184 = v183 - 238554347 - v177 + 932383584;
v185 = v184 + v177 + 2100277479;
v186 = v185 + v180 + 54142085 - v182 - 1632592373;
v187 = v185 - v184 + 579181258;
v188 = 2 * (v182 + 1383200762) + 1;
v189 = v187 + v188 + v186 - v184 + 1 + 1172965920 + 1;
v190 = v187 - 101123714 - v189 + 1 - v189 - 96237627;
v188 += 2;
v191 = 2 * (v189 + v184 - 207227160 + 4) + 1;
v192 = v191 + v189 - v188;
v190 += 4;
v193 = v191 - 1353895842 + 1;
v194 = v190 + v188 + 2123750079 - v193;
v190 += 1696689707;
v195 = 2 * (v192 + 1 - v190);
v196 = v194 + 1 - v195 - 78101511;
v190 += 540662868;
v197 = v190 + v195 - 1145799797 - v196;
v198 = 2 * (v193 - 185780694) + 1;
v199 = v198 + v196;
v190 += 1255424563;
v200 = 2 * (v199 + v198) - 1727929676;
v199 += 2;
v201 = v190 + v199 + v197;
v202 = v190 - 1214148504 + 1;
v199 += 401187067;
v203 = v200 - 1564098266 + 917389966 - v202 - 1198776331 + 1 - v199;
v204 = v201 + v202 + 2 - v203;
v205 = v203 - 318781264 - v199 - 1605668317 + 2;
v206 = 2 * (v201 + 1844554225) - 1604774369;
v207 = 2 * (v205 + v199 + 790825996 - v206) + 1650229900;
v208 = v204 - 490598907 + 1;
v206 += 282040833;
v209 = v206 + v205 - 2006766853 - v208;
v206 += 2;
v210 = v207 + 1511399432 - v208 - 1551102207;
v211 = v206 + v206 + v209 - v210 - v208;
v206 += 1215172648;
v210 -= 959608047;
v212 = v211 + 1 - v206;
v213 = v206 - v212 - v210;
v214 = v212 + v208 + 1869175045 - v213 - 1424027273;
v215 = v210 + 1620160695 - v214;
v216 = v214 + v214 + v213 - v215 - 1065981445;
v217 = 2 * (v215 - 1244977230) + 1747029779;
v216 -= 1257866941;
v218 = v214 + 2143814783 - v216 - 1398907650;
v219 = 2 * v212 + 2 - v217++;
v220 = v219 + v216 + 1 - v218 + 1 - v217 - v217;
v221 = v219 - v217++;
v222 = v218 - 1855122676 + 1;
v223 = v222 + v221 + 2;
v224 = v223 + v217 + v220 - 1317237096;
v217 += 2;
v225 = v222 + v224;
v226 = v222 - v225 - 777710099;
v227 = v223 - 730911683 - v226;
v228 = v227 + v226 + 1;
v229 = v217 + v227 + v225 - 1217941265;
v230 = v217 - v228;
v231 = v230 + v228 + v227 - 1682643877;
v228 += 2;
v232 = v230 + v229 + 1938596261 + 1 - v228;
v228 += 584042825;
v233 = v230 - 2139100084 + 2;
v234 = v233 + v232 + 1;
v235 = 2 * (v228 + v233) + 1;
v228 += 1437309881;
v236 = v228 + v234 + v235 + 1 + 1;
v228 -= 716828805;
v237 = 2 * (v234 + 1 - v228) - 685322476;
v238 = v236 + v231 - 1381742058 + 1995963757 + 2;
v239 = v228 - 1516409973 + 1147924830;
v240 = v236 + 1 - v238 - v239 - 2104005844;
v241 = v239 + 1 - v240;
v238 -= 759057394;
v242 = v240 - v238;
v238 -= 623914540;
v243 = v241 - v238;
v244 = v238 - v243;
v243 += 237287396;
v245 = v243 + 2 * (v237 + 1002096745) - 2048248416 + 1892930438;
v246 = 2 * v244 + 1294486749;
v247 = v242 + 1612687194 - v243 - 660996117 - v246;
v248 = v247 + v246 + 720558110;
v247 += 977714025;
v248 -= 1491378659;
v249 = v243 + 1945659396 - v247;
v250 = v245 + 1 - v248;
v251 = v249 + v248 + 1185773403;
v252 = v250 - v249 + 1;
v253 = v251 + v249 + 401286047;
v254 = v252 - 998849865 + 1;
v255 = 2 * v247 + 754645442 - v254;
v256 = v251 - 1424315697 + 2 - v255;
v257 = v255 - v256;
v256 -= 1309666088;
v258 = v256 + v254 - v253;
v259 = v256 + 1 - v253 - 2033562943;
v260 = v257 + 1650643934 - v259 - 1415290431;
v261 = v260++ + v253 + 524627955;
v262 = v260 + v258 + 2013559893;
v260 -= 824578413;
v261 -= 446217575;
v263 = v262 + 508608480 - v261 + 1345436449;
v264 = v259 + 1403184861 - v260 + 1284484219;
v265 = v263 + v260;
v263 -= 242016614;
v266 = v264 + 1347235185 - v263;
v267 = v266 + v263 + 1 + 787180614;
v266 += 606099305;
v268 = 2 * (v261 + 520953472) + 165941725;
v269 = v268 + v265 - 1534490202 - v266 + 1;
v267 += 2120509468;
v270 = v266 + 689980400 - v269 - 2044475833 - v269;
v269 -= 1625687532;
v271 = v268 + 1 - v269 + 1;
v272 = v270 + v269 + 1252726713;
v273 = v270 - v267 + 1;
v274 = 2 * v267 - v271 + 1;
v272 += 531933468;
v275 = v271 - v274 - v274 + 2039136993;
v276 = v274 - v272;
v277 = v273 - 1600087378 + 1;
v278 = v275 + 2 * (v272 + 1);
v279 = v276 + 2 - v278;
v280 = v277 + v278;
++v275;
v281 = v277 - 1762733020 - v279 + 1;
v280 += 1278825738;
v282 = v279 + 147538177 - v275;
v283 = v275 - v281;
v284 = v281 + 693844065 - v280;
v285 = v280 - ++v282;
v286 = v282 + v283 + 1 - v284;
v287 = v284 - v285 - 74089317;
v288 = v282 - v287 - v286 - 681820438;
v289 = v287 - 1256120859 + 149723392 - v288;
v290 = v286 - 1421591606 - v289 + 2;
v285 += 1989232579;
v291 = v289 + 1 - v290;
v292 = 2 * (v288 - 685621057) + 1;
v293 = v290 - v291 - v285;
v294 = v285 - v292;
v295 = v291 - 1661767175 + 42969351;
v296 = v294 + v294 + v293 - 1972384502 + 2 - 1576459347 + 1;
v297 = v295 + v292 - 396668767 - 1534437557;
v298 = v296 + v294 - 1645192742 - v295 - 1479631423 + 2 - 331301694;
v299 = v296 - 106622097 + 668588646;
v300 = 2 * (v299 + v297 + v295 + 1 + 2) - 1263581112;
v297 += 1979779660;
v301 = v297 + v300 + v299 + 1343345468 + 481569519;
v298 += 861842343;
v302 = v298 + v300 - 1650922112 + 1803040625 - 1103549091 + 1;
v303 = v298 + v301 - 263499248;
v304 = v303 + v298;
v305 = v304++ + v302 - 438171503;
v306 = v297 - 2076009387 + 1524090740 - v304 + 1;
v304 += 575953311;
v307 = v305 + 1306759242 - v306;
v308 = v303 - 429496975 + 1812284714 - v307++;
v309 = 2 * (v306 + 1523384106) - 1468869015;
v310 = v304 + v308 + 1260443893 - v309;
v311 = v309 - 1158775838 - v307++;
v312 = 2 * v310 - 441360349;
v313 = v311 - v312;
v314 = v313++ + v307 + v304 - 1384238736;
v315 = 2 * v307 - v313 + 496097820;
v316 = v315 + v314 + 2 + 1;
v315 += 3;
v317 = 2 * (2 * v312 + 3 - v316 + 2070720611) - 1285251516 + 88029981;
v318 = v315 + v313 - 1389710860;
v319 = v315 - v318;
v320 = v319 + v319 + v316 - 589472948 + 1;
++v319;
v321 = 2 * v317 + 942166371;
v322 = v320 + v318 - 344804349 + 849785358;
v323 = v320 - v321;
v322 += 53013894;
v324 = v321 - v319;
v325 = v322 + v323 + 1;
v326 = 4 * (v325 + v319 - v322 - 2049097191 + 1);
v322 -= 1029516387;
v327 = v325 + 473722879 - v322;
v326 -= 1652737171;
v328 = v324 + 1 - v326;
v329 = v326 - v327;
v322 += 1088562794;
v327 += 78577575;
v330 = v329 - v322 - v327 + 132302044;
v328 -= 771106090;
v322 += 2;
v331 = v330 + 1 - v328;
v332 = v327 - v331;
v333 = v332 + v328;
v332 += 1152138250;
v334 = v322 + v331 - 1557943841 + 1;
v335 = v332 + v322 - v334;
v336 = v333 + 1293271530 - v332 - v335;
v334 += 245975965;
v337 = v334 + v335 + 2098061773;
v332 += 1210065134;
v338 = v334 - v336 + 1;
v339 = v337 + 1 - v332 + 1042845593;
v332 += 1017773432;
v340 = v336 - v338 + 544855734;
v341 = v340 + 2 * v339 + 1636319835;
v340 -= 2122376282;
v342 = v332 + v332 + v338 - 213405862;
v332 += 1914409404;
v343 = 2 * (v341 + 1) - v340 + 1026384791;
v344 = v332 + v342 - 207594250 + 1367733505 - v340;
v345 = v340 - v343++ + 1434173388;
v346 = v344 - 1373169356 - v332++;
v347 = v332 + v346 - 1698350246 + 807585909 - v343 - 1616726979;
v348 = v343 - v332;
v349 = v348 + v347;
v350 = v349++ + v348 + 1;
v351 = 2 * (v345 - 28630427 + 560310549 - v350 + 1) + 1587875006 - v349 - 258344410;
v352 = v332 - 390257379 + 1 - v349;
v353 = v352 + v349;
v354 = v352++ + v350 + 4;
v355 = v351 + 1 - v352;
v354 -= 1828963202;
v356 = v354 + 2 * v352 + 1;
v357 = v356 + v355 - 1265518153 + 1354618067;
v358 = v354 + v356 - v357;
v354 += 24457593;
v358 += 2081985567;
v359 = v354 + v353 + 1624829730 + 1;
v360 = 2 * (v358 + v357 - 1949374989) + 781522725;
v361 = ++v354 + v358;
v362 = v354 + 1493767541 - v359;
v361 += 4;
v363 = 2 * v359 - v361 - 1727523967;
v364 = v362 + v361 + v360 + 218569202 - v363 + 449916241;
v363 += 327109260;
v365 = v362 + 1549803007 - v363 + 957128236;
v363 += 916862246;
v366 = 2 * (v364 + 414246669) + 2040411505;
v367 = v365 + 536918145 - v366;
v368 = v366 - v367 + 1;
v369 = 2 * (v367 - 129161079 - v363 + 1) - 1900300983;
v370 = 2 * (v361 - 798140456) + 4;
v371 = v370 + v363 - 665700202 + 2;
v369 += 30341174;
v372 = v370 + 1 - v369 - 1952101394;
v373 = v372 + v369 - v371;
v374 = v373 + v371;
v375 = 2 * (v374 + v372 + 1 - 1317292497);
v376 = v373 - 2112199059 + 419983391;
v377 = v376 + 2 * (v368 - 1343830370 + 442537035) - 1033591519 + 1879391070 - v375 - 2060553041 + 1;
v378 = v375 + v375 + v374 + 738693954 + 1 - v377;
v379 = v375 + 1 - v377;
v380 = v377 - 1930629742 - v379 - 1928040188 + 1102478597;
v381 = v380 + 2 * v379 + 1 - 448866693;
v376 -= 2055000006;
v382 = 2 * (2 * (v380 + 604066061) + 2);
v383 = v382 + v376 + v381 - 1881910858;
v384 = v378 - 947925440 + 2;
v385 = v384 + v383 + v382 + 842529404 + 1;
v376 -= 168380786;
++v384;
v386 = v376 + v383 + 1;
v387 = v376 - v384 + 1919090703;
v388 = 2 * (v384 + 1 - v386 + 1) - 376075359 - v387;
v389 = v388 + v386 - 1078951762;
v388 += 4;
v390 = v388 + v387 + 1;
v388 += 1398399335;
v391 = v390 + v385 - 1475310267 - v389 + 1 + 9540715;
v392 = v389 - 1641637778 + 2 - v388 + 2;
v393 = v388 - 1972219276 + 1;
v392 -= 866747255;
v394 = v392 + v390 - 1373171668 + 1586106979;
v395 = v393 + v391 - 931348898;
v396 = v394 + v392 - 1900058436 - v395;
v397 = 2 * v394 + 1334476417;
v398 = v396 - 467332541 + 1817029648;
v399 = 2 * (v393 + 808026034) - 1047285892 + 609483421 - v397;
v395 += 1953163588;
v400 = v397 - 292607806 - v399 - 42192282 - v395 + 1;
v401 = v399 + 1 - v398 + 1;
v402 = v395 + 1 - v401;
v403 = v400 - v402;
v404 = v401 + 1 - v403 + 1872425146;
v405 = v398 - 195196821 + 377105645 - v404 - v404;
v406 = v402 - v404;
v407 = v404 - 1842186611 + 547686199;
v408 = v407 + v403 + 1374530959 - v405 + 1 - 184314042;
v409 = v405 - 1871472347 + 1;
v410 = v409 + v406;
v409 += 2027045620;
v411 = v409 + v410 - 855357098 + 1 - 2037318886;
v412 = v411 + v408 + 1324830997 - v409 + 1863672173;
v413 = 2 * (v407 - 1311778367) + 1;
v414 = v413 + v411;
v409 += 638982232;
v415 = v412 - 1420319999 - v409 + 1706741566;
v413 += 2;
v416 = v409 + 600153250 - v415 - 1749613292 + 1;
v417 = v415 - v413;
v418 = v414 - 103143630 + 151909657 - v416 + 1;
v419 = 2 * v413 - v416++;
v420 = v417 + 1 - ++v419;
v421 = v418 - v416 - v416 + v419;
v420 -= 1385665685;
return v420+ v421+ 1+ 640484926+ 2 * (v421 + v416 + 1815285368)+ v420+ v421+ 1+ 640484926+ v420+ v421+ 1+ v420+ v421 + 1+ v420- 1389466703+ 495424244+ 2 * (v420 + v421 + 1 + 640484926);
}
int __cdecl challenge_1(unsigned int c1, unsigned int c2, unsigned int c3, unsigned int c4)
{
unsigned int v4; // edx
unsigned int v5; // ebx
unsigned int v6; // ecx
unsigned int v7; // eax
int v8; // ecx
int v9; // eax
int v10; // edx
int v11; // ebx
int v12; // ecx
int v13; // eax
int v14; // ebx
int v15; // edx
int v16; // eax
int v17; // ebx
int v18; // ecx
int v19; // edx
int v20; // ecx
int v21; // edx
int v22; // eax
int v23; // ebx
int v24; // edx
int v25; // eax
int v26; // ecx
int v27; // edx
int v28; // ecx
int v29; // edx
int v30; // eax
int v31; // ebx
int v32; // ecx
int v33; // eax
int v34; // edx
int v35; // ecx
int v36; // ebx
int v37; // edx
int v38; // ecx
int v39; // eax
int v40; // ebx
int v41; // ecx
int v42; // eax
int v43; // edx
int v44; // ebx
int v45; // ebx
int v46; // edx
int v47; // ecx
int v48; // eax
int v49; // edx
int v50; // ebx
int v51; // eax
int v52; // edx
int v53; // ebx
int v54; // eax
int v55; // edx
int v56; // ecx
int v57; // ecx
int v58; // eax
int v59; // edx
int v60; // eax
int v61; // ebx
int v62; // eax
int v63; // ebx
int v64; // ecx
int v65; // eax
int v66; // edx
int v67; // ecx
int v68; // ebx
int v69; // edx
int v70; // ebx
int v71; // edx
int v72; // ecx
int v73; // eax
int v74; // ecx
int v75; // edx
int v76; // ebx
int v77; // edx
int v78; // edx
int v79; // eax
int v80; // ebx
int v81; // ecx
int v82; // ebx
int v83; // eax
int v84; // ebx
int v85; // edx
int v86; // ebx
int v87; // eax
int v88; // edx
int v89; // ecx
int v90; // eax
int v91; // edx
int v92; // ebx
int v93; // ecx
int v94; // ebx
int v95; // eax
int v96; // ecx
int v97; // ecx
int v98; // ebx
int v99; // ecx
int v100; // eax
int v101; // edx
int v102; // ebx
int v103; // edx
int v104; // edx
int v105; // ecx
int v106; // eax
int v107; // ecx
int v108; // edx
int v109; // eax
int v110; // edx
int v111; // eax
int v112; // ebx
int v113; // ecx
int v114; // edx
int v115; // eax
int v116; // edx
int v117; // ecx
int v118; // ebx
int v119; // eax
int v120; // ecx
int v121; // edx
int v122; // edx
int v123; // eax
int v124; // edx
int v125; // ebx
int v126; // eax
int v127; // edx
int v128; // ecx
int v129; // ebx
int v130; // edx
int v131; // ebx
int v132; // ecx
int v133; // ebx
int v134; // ebx
int v135; // eax
int v136; // ecx
int v137; // ebx
int v138; // ebx
int v139; // edx
int v140; // ecx
int v141; // ebx
int v142; // eax
int v143; // ecx
int v144; // ebx
int v145; // edx
int v146; // ebx
int v147; // edx
int v148; // ecx
int v149; // eax
int v150; // ebx
int v151; // ecx
int v152; // ebx
int v153; // edx
int v154; // eax
int v155; // edx
int v156; // ebx
int v157; // edx
int v158; // ebx
int v159; // ecx
int v160; // ebx
int v161; // eax
int v162; // ecx
int v163; // ebx
int v164; // edx
int v165; // eax
int v166; // ecx
int v167; // eax
int v168; // edx
int v169; // ebx
int v170; // ecx
int v171; // eax
int v172; // ecx
int v173; // ebx
int v174; // ecx
int v175; // edx
int v176; // ebx
int v177; // ebx
int v178; // eax
int v179; // edx
int v180; // ecx
int v181; // eax
int v182; // edx
int v183; // eax
int v184; // eax
int v185; // ebx
int v186; // ecx
int v187; // ebx
int v188; // edx
int v189; // ecx
int v190; // ebx
int v191; // eax
int v192; // ecx
int v193; // eax
int v194; // edx
int v195; // ecx
int v196; // edx
int v197; // ecx
int v198; // eax
int v199; // edx
int v200; // eax
int v201; // ecx
int v202; // ebx
int v203; // eax
int v204; // ebx
int v205; // eax
int v206; // ecx
int v207; // edx
int v208; // ebx
int v209; // eax
int v210; // edx
int v211; // eax
int v212; // eax
int v213; // ecx
int v214; // ebx
int v215; // edx
int v216; // ecx
int v217; // edx
int v218; // ebx
int v219; // eax
int v220; // ecx
int v221; // eax
int v222; // ebx
int v223; // eax
int v224; // ecx
int v225; // ecx
int v226; // ebx
int v227; // eax
int v228; // ebx
int v229; // ecx
int v230; // edx
int v231; // eax
int v232; // ecx
int v233; // edx
int v234; // ecx
int v235; // edx
int v236; // edx
int v237; // ecx
int v238; // eax
int v239; // ebx
int v240; // edx
int v241; // ebx
int v242; // edx
int v243; // ebx
int v244; // eax
int v245; // ecx
int v246; // eax
int v247; // edx
int v248; // eax
int v249; // ebx
int v250; // ecx
int v251; // eax
int v252; // ecx
int v253; // ebx
int v254; // ecx
int v255; // edx
int v256; // eax
int v257; // edx
int v258; // ecx
int v259; // eax
int v260; // edx
int v261; // ebx
int v262; // ecx
int v263; // ecx
int v264; // eax
int v265; // edx
int v266; // eax
int v267; // ecx
int v268; // ebx
int v269; // edx
int v270; // eax
int v271; // ebx
int v272; // edx
int v273; // eax
int v274; // ecx
int v275; // ebx
int v276; // ecx
int v277; // eax
int v278; // edx
int v279; // ecx
int v280; // edx
int v281; // eax
int v282; // ecx
int v283; // ebx
int v284; // eax
int v285; // edx
int v286; // ebx
int v287; // eax
int v288; // ecx
int v289; // eax
int v290; // ebx
int v291; // eax
int v292; // ecx
int v293; // ebx
int v294; // edx
int v295; // eax
int v296; // ebx
int v297; // ecx
int v298; // edx
int v299; // ebx
int v300; // eax
int v301; // ebx
int v302; // eax
int v303; // ebx
int v304; // edx
int v305; // eax
int v306; // ecx
int v307; // eax
int v308; // ebx
int v309; // ecx
int v310; // ebx
int v311; // ecx
int v312; // ebx
int v313; // ecx
int v314; // edx
int v315; // eax
int v316; // edx
int v317; // ebx
int v318; // ecx
int v319; // eax
int v320; // edx
int v321; // ebx
int v322; // ecx
int v323; // edx
int v324; // ebx
int v325; // edx
int v326; // eax
int v327; // edx
int v328; // ebx
int v329; // eax
int v330; // eax
int v331; // eax
int v332; // edx
int v333; // ebx
int v334; // eax
int v335; // ecx
int v336; // ebx
int v337; // ecx
int v338; // eax
int v339; // ecx
int v340; // ebx
int v341; // ecx
int v342; // eax
int v343; // ecx
int v344; // eax
int v345; // ebx
int v346; // eax
int v347; // eax
int v348; // ecx
int v349; // eax
int v350; // ecx
int v351; // ebx
int v352; // edx
int v353; // eax
int v354; // ecx
int v355; // ebx
int v356; // edx
int v357; // ebx
int v358; // edx
int v359; // eax
int v360; // ebx
int v361; // edx
int v362; // ecx
int v363; // eax
int v364; // ebx
int v365; // ecx
int v366; // ebx
int v367; // ecx
int v368; // ebx
int v369; // ecx
int v370; // edx
int v371; // eax
int v372; // edx
int v373; // ecx
int v374; // eax
int v375; // edx
int v376; // ecx
int v377; // ebx
int v378; // eax
int v379; // edx
int v380; // ebx
int v381; // edx
int v382; // ebx
int v383; // edx
int v384; // eax
int v385; // ebx
int v386; // edx
int v387; // ecx
int v388; // eax
int v389; // edx
int v390; // ecx
int v391; // ebx
int v392; // edx
int v393; // eax
int v394; // ecx
int v395; // ebx
int v396; // edx
int v397; // ecx
int v398; // edx
int v399; // eax
int v400; // ecx
int v401; // eax
int v402; // ebx
int v403; // ecx
int v404; // eax
int v405; // edx
int v406; // ebx
int v407; // eax
int v408; // ecx
int v409; // edx
int v410; // ebx
int v411; // ebx
int v412; // ecx
int v413; // eax
int v414; // ebx
int v415; // ecx
int v416; // edx
int v417; // ecx
int v418; // ebx
int v419; // eax
int v420; // ecx
int v421; // eax
v4 = c2 + c1 - c4 - 2133754790 + 1 + 2 * c2 - 1785093898;
v5 = 2 * (c4 + 1 - c3)- c2- 1917226979- (c2+ c1 - c4 - 2133754790+ 2 * c2)+ 2- (c3+ 539193617)- v4- 350898193;
v6 = c3 + 539193617 - v5 - 879839410;
v5 += 2;
v6 += 3;
v4 += 2109602273;
v7 = 2 * (2 * (c2 + c1 - c4 - 2133754790 + 3 - (c3 + 539193617) - 1164434189 - v5 - v6) + 1);
v8 = 2 * v6 - 1873426435 - v7;
v9 = v7 - v4 + 1;
v10 = v4 - 971527202 + 730640080;
v11 = v5 + 1150557381 - v10 - 1412696239 + 1;
v12 = v11 + v8 - 396431529 + 1;
v13 = v9 + 2 - v12 + 1;
v14 = v12 + v11 + 1;
v15 = v10 + 204474460 - v13 - 1432203755;
v16 = v14 + v13 + 884313224 + 813147417;
v17 = v15 + v14 + 2;
v18 = v15 + v12 - 451236562 + 3;
v19 = v16 + v15 + 1;
v17 += 138511611;
v16 += 953411192;
v20 = v16 + v18;
v21 = v17 + 2 * (v19 + 1) + 119463169;
v17 -= 738693819;
v22 = v16 + 594867870 - v17 + 1413353867;
v23 = v17 - v22;
v22 += 520753425;
v24 = v22 + v21 + 144745048;
v25 = v24++ + v22 - 1828520841 + 1;
v26 = v20 + 3 - v24;
v27 = v24 - v26;
v28 = v27 + v26 + 763465995;
v29 = 2 * (v27 + 2);
v30 = v29 + v25 + 1017115747;
v31 = v23 - 879256061 + 1336943267 - v30;
v32 = v30 + v30 + v28 + 1689547303 - 1018772533 + 1;
v33 = v30 - v31 + 1;
v34 = v31 + v29 - v33 + 909973850;
v35 = v34 + v32 + 228062414;
v36 = v35 + v31 + 347278668;
v35 -= 720946967;
v37 = 2 * (v34 + 1 - v35);
v38 = v37 + v35 + 1;
v37 += 1888994439;
v39 = 2 * (v33 + 579771010) + 2103615418;
v40 = v36 - 276265002 - v37 + 1864035437;
v41 = v38 + 1 - v39;
v37 += 1786144130;
v42 = v39 + 1600574700 - v37;
v43 = v37 - v40;
v44 = v43 + v40 - v41 + 2105473564;
v41 *= 2;
v45 = 2 * (v44 - v41);
v46 = v43 - 1150894576 + 3;
v47 = v45 + v41 + 313221810 - v46 + 807301504;
v48 = v42 - 124125674 + 1 - v46 + 1 - v46 + 1;
v49 = v48 + v46;
v50 = v49 + v45 - 468305613 + 3 - 2100928955;
v51 = 2 * (v48 - v49 - ++v47) + 1;
v52 = v49 + 1 - v47++ + 3;
v53 = v52 + v50;
v54 = v51 - v53;
v55 = v52 - v47 + 1;
v53 -= 446157988;
v54 += 1553282976;
v56 = v54 + v53 + v47 + 1;
v53 *= 2;
v57 = v53 + v56 - 1230516346 + 1 + 1205548791;
v58 = v54 - v53 + 2128637547;
v59 = v58 + v55 + 1;
v60 = v58 - v57;
v57 += 377513439;
v61 = v53 - 799999952 - v57;
v62 = v61 + v60 + 1;
v63 = v61 - v57;
v59 += 848132728;
v64 = v57 - v63 - v59;
v65 = v59 + v62 - 2142680737 + 1764150285;
v63 += 2087876122;
v66 = v59 + 1814013069 - v63 - v64;
v67 = 2 * v64 - v65 + 1132472947;
v68 = v63 - 788948114 + 1 - v67;
v69 = v68 + v68 + v66 + 1553607352;
v67 += 2;
v70 = v69 + 2 * v68 + 1518868433;
v71 = v67 + v67 + v69 - v70;
v72 = v70 + v67;
v70 += 713535814;
v73 = 2 * v65 + 1429126951 - v70;
v70 -= 173942082;
v74 = v70 + v72 - 1888550847 + 1 - 394102299;
v75 = v71 + 256237465 - v74;
v76 = v75 + v70 + 1;
v77 = v75 - v74++;
v76 += 2140073780;
v78 = 2 * (v77 - 1454905092) - 1933992509;
v79 = v76 + 2 * (v73 + 1866717529) - v74 - 1310766122 - v78;
v80 = v76 - v74;
v81 = v80 + v74;
v82 = v79 + v80;
++v81;
v83 = v82 + v79 + 1;
v78 += 1083862846;
v84 = v82 + 1 - v81 - v78;
v85 = v81 + v78;
v81 -= 614253581;
v86 = v85 + v84 - 515607244 + 238772881;
v87 = v83 + 141351837 - v81 + 1;
v88 = v86++ + v85 - 543286513 + 1674408964 - 794464384;
v89 = v81 - 623767744 + 215241888;
v90 = 2 * (v89++ + v87 + 1710998538);
v91 = v86 + v86 + v88 + 1 + 1 - v89++;
v92 = v89 + v86;
v90 -= 885178085;
v91 += 1677704898;
v93 = v90++ + v89 - 940635716;
v94 = v92 + 1 - v90;
v95 = v91 + v90 + 1 + 1841924206;
v96 = v91 + v93 + 941760921;
v91 += 2;
v97 = v96 + 1 - v91 + 1530834091;
v98 = v94 - v97 + 1;
v99 = v95 + v97 + 1699993484;
v100 = v98 + v95 + 1;
v101 = v98 + v91 - 523060265 + 1789589531;
v102 = v98 + 1281582157 - v100;
v100 += 146514254;
v103 = v101 - v99 - v100++;
v99 += 2080302551;
v104 = 2 * (v99 + v103 + 1512882559 + 1);
v105 = v99 - v100;
v104 -= 784717007;
v106 = v104++ + v100 - 1584810020 + 2;
v107 = v104 + v105 + 1;
v106 += 1065502423;
v102 += 3;
v108 = v102 + v104 - v107 - v106 + 342809982;
v107 -= 1412780444;
v109 = v108 + v106 + 1 - 858330204;
v110 = v109 + v108;
v102 -= 664953144;
v111 = v109 - 1329716196 - v102;
v112 = v102 - v107;
v111 += 1373514701;
v113 = v107 - 1346592359 + 216683527 - v111;
v114 = v111 + v110 - 288276575 + 1500011784;
v115 = v113 + v111;
v116 = v115++ + v114;
v117 = 2 * (v113 - 1163128426);
v118 = v117 + v112 - 818961183 - v115 - 593940334;
v119 = v118 + v115 + 2;
v118 += 428412235;
v120 = v117 + 3 - v118;
v121 = v116 + 4 - v118 + 1;
v118 += 894601604;
v122 = v118 + v121;
v123 = v122 + v119 + 1 + 443477999;
v124 = v123 + v122;
v125 = 2 * v118 - v123;
v126 = v124 + v123 - 2061231162;
v127 = v124 - v125;
v128 = v126 + v120 + 1485909680 + 1483310720;
v129 = v128 + v127 + v125 - 1355157173 + 1;
v130 = v128 + v127;
v128 += 2;
v131 = v129 - v128;
v130 += 1683851829;
v132 = v128 - v131 - 354913611;
v133 = v131 - v132;
v132 -= 198220312;
v134 = v133 + 172443045 - v132;
v135 = v126 + 3 - v132 - v134;
v136 = v130 + 2 * (v132 - v134) - v135 + 471821392;
v137 = v130++ + v134 - v136;
v136 += 923861112;
v138 = v130 + 2 * (v137 + 1) + 1 - 1146928935 + 1 - v136;
v139 = v138 + 2 * v130 + 1;
v140 = v136 - 1156737329 - v138 + 2 - v138 - v139;
v141 = v140 + v138 + 1;
v142 = v135 - 608570200 + 1 - v141 + 1;
v139 += 2;
v143 = v140 - 1777203220 + 1;
v144 = v139 + v141 - v142 - 440487739 + 182778494 - v143;
v145 = v139 + 966597185 - v144;
v142 += 967980219;
v146 = v144 - 1652140998 + 1;
v147 = v142 + v145 - 1363945608 + 1 - v146;
v148 = v143 - v146 + 1350186086;
v149 = 2 * (v148 + 2 * v142);
v150 = v146 + 1 - v147 - 457990213;
v151 = v148 + 1 - v150;
v152 = v150 - 504705392 + 1;
v153 = v147 + 1193758906 - v152;
v154 = v149 + 1 - v152 + 144039938 - v153;
v155 = v154 + v153;
v154 += 2;
v156 = v152 + 2078215581 - v154 + 1;
v157 = v156 + v155 - 122946150 + 301662336;
v158 = v156 - v157;
v154 += 2;
v159 = v157++ + v158 + v151 - 958001904 + 1284137460 + 1;
v160 = v154 + v158 + 1002156873 - v157 + 170108160;
v161 = v154 - 1014383826 + 161227700;
v162 = v159 - v161;
v163 = v160 - 255510393 + 376777367;
v164 = v157 - v162 + 2;
v165 = v163 + v161 - 1912551381 + 1;
v166 = v165 + v162 - v163 + 1 + 1;
v167 = v166 + v165 + 1;
v168 = v163 + v164 + 201934410 + 968132783;
v169 = v163 - v168++;
v170 = v166 - v167;
v171 = v168 + v167;
v172 = v170 - v168;
v168 += 2029379458;
v173 = v168 + v169 - 1763166604 + 1 + 1;
v171 -= 1188417209;
v174 = v172 + 1 - v173 + 1;
v175 = v174 + v168 + 2140747580 - v171 + 668304081;
v176 = v173 - 26185106 + 474549714 - v174++;
v177 = v176 - v174;
v178 = v175 + v171 + 1;
v179 = v178 + v175;
v180 = v178 + v177 + v174 + 1 + 2141394379;
v181 = v178 - 826788372 + 3;
v182 = v181 + v179 + 1;
v177 += 741838009;
v183 = v177 + v181;
v177 *= 2;
v184 = v183 - 238554347 - v177 + 932383584;
v185 = v184 + v177 + 2100277479;
v186 = v185 + v180 + 54142085 - v182 - 1632592373;
v187 = v185 - v184 + 579181258;
v188 = 2 * (v182 + 1383200762) + 1;
v189 = v187 + v188 + v186 - v184 + 1 + 1172965920 + 1;
v190 = v187 - 101123714 - v189 + 1 - v189 - 96237627;
v188 += 2;
v191 = 2 * (v189 + v184 - 207227160 + 4) + 1;
v192 = v191 + v189 - v188;
v190 += 4;
v193 = v191 - 1353895842 + 1;
v194 = v190 + v188 + 2123750079 - v193;
v190 += 1696689707;
v195 = 2 * (v192 + 1 - v190);
v196 = v194 + 1 - v195 - 78101511;
v190 += 540662868;
v197 = v190 + v195 - 1145799797 - v196;
v198 = 2 * (v193 - 185780694) + 1;
v199 = v198 + v196;
v190 += 1255424563;
v200 = 2 * (v199 + v198) - 1727929676;
v199 += 2;
v201 = v190 + v199 + v197;
v202 = v190 - 1214148504 + 1;
v199 += 401187067;
v203 = v200 - 1564098266 + 917389966 - v202 - 1198776331 + 1 - v199;
v204 = v201 + v202 + 2 - v203;
v205 = v203 - 318781264 - v199 - 1605668317 + 2;
v206 = 2 * (v201 + 1844554225) - 1604774369;
v207 = 2 * (v205 + v199 + 790825996 - v206) + 1650229900;
v208 = v204 - 490598907 + 1;
v206 += 282040833;
v209 = v206 + v205 - 2006766853 - v208;
v206 += 2;
v210 = v207 + 1511399432 - v208 - 1551102207;
v211 = v206 + v206 + v209 - v210 - v208;
v206 += 1215172648;
v210 -= 959608047;
v212 = v211 + 1 - v206;
v213 = v206 - v212 - v210;
v214 = v212 + v208 + 1869175045 - v213 - 1424027273;
v215 = v210 + 1620160695 - v214;
v216 = v214 + v214 + v213 - v215 - 1065981445;
v217 = 2 * (v215 - 1244977230) + 1747029779;
v216 -= 1257866941;
v218 = v214 + 2143814783 - v216 - 1398907650;
v219 = 2 * v212 + 2 - v217++;
v220 = v219 + v216 + 1 - v218 + 1 - v217 - v217;
v221 = v219 - v217++;
v222 = v218 - 1855122676 + 1;
v223 = v222 + v221 + 2;
v224 = v223 + v217 + v220 - 1317237096;
v217 += 2;
v225 = v222 + v224;
v226 = v222 - v225 - 777710099;
v227 = v223 - 730911683 - v226;
v228 = v227 + v226 + 1;
v229 = v217 + v227 + v225 - 1217941265;
v230 = v217 - v228;
v231 = v230 + v228 + v227 - 1682643877;
v228 += 2;
v232 = v230 + v229 + 1938596261 + 1 - v228;
v228 += 584042825;
v233 = v230 - 2139100084 + 2;
v234 = v233 + v232 + 1;
v235 = 2 * (v228 + v233) + 1;
v228 += 1437309881;
v236 = v228 + v234 + v235 + 1 + 1;
v228 -= 716828805;
v237 = 2 * (v234 + 1 - v228) - 685322476;
v238 = v236 + v231 - 1381742058 + 1995963757 + 2;
v239 = v228 - 1516409973 + 1147924830;
v240 = v236 + 1 - v238 - v239 - 2104005844;
v241 = v239 + 1 - v240;
v238 -= 759057394;
v242 = v240 - v238;
v238 -= 623914540;
v243 = v241 - v238;
v244 = v238 - v243;
v243 += 237287396;
v245 = v243 + 2 * (v237 + 1002096745) - 2048248416 + 1892930438;
v246 = 2 * v244 + 1294486749;
v247 = v242 + 1612687194 - v243 - 660996117 - v246;
v248 = v247 + v246 + 720558110;
v247 += 977714025;
v248 -= 1491378659;
v249 = v243 + 1945659396 - v247;
v250 = v245 + 1 - v248;
v251 = v249 + v248 + 1185773403;
v252 = v250 - v249 + 1;
v253 = v251 + v249 + 401286047;
v254 = v252 - 998849865 + 1;
v255 = 2 * v247 + 754645442 - v254;
v256 = v251 - 1424315697 + 2 - v255;
v257 = v255 - v256;
v256 -= 1309666088;
v258 = v256 + v254 - v253;
v259 = v256 + 1 - v253 - 2033562943;
v260 = v257 + 1650643934 - v259 - 1415290431;
v261 = v260++ + v253 + 524627955;
v262 = v260 + v258 + 2013559893;
v260 -= 824578413;
v261 -= 446217575;
v263 = v262 + 508608480 - v261 + 1345436449;
v264 = v259 + 1403184861 - v260 + 1284484219;
v265 = v263 + v260;
v263 -= 242016614;
v266 = v264 + 1347235185 - v263;
v267 = v266 + v263 + 1 + 787180614;
v266 += 606099305;
v268 = 2 * (v261 + 520953472) + 165941725;
v269 = v268 + v265 - 1534490202 - v266 + 1;
v267 += 2120509468;
v270 = v266 + 689980400 - v269 - 2044475833 - v269;
v269 -= 1625687532;
v271 = v268 + 1 - v269 + 1;
v272 = v270 + v269 + 1252726713;
v273 = v270 - v267 + 1;
v274 = 2 * v267 - v271 + 1;
v272 += 531933468;
v275 = v271 - v274 - v274 + 2039136993;
v276 = v274 - v272;
v277 = v273 - 1600087378 + 1;
v278 = v275 + 2 * (v272 + 1);
v279 = v276 + 2 - v278;
v280 = v277 + v278;
++v275;
v281 = v277 - 1762733020 - v279 + 1;
v280 += 1278825738;
v282 = v279 + 147538177 - v275;
v283 = v275 - v281;
v284 = v281 + 693844065 - v280;
v285 = v280 - ++v282;
v286 = v282 + v283 + 1 - v284;
v287 = v284 - v285 - 74089317;
v288 = v282 - v287 - v286 - 681820438;
v289 = v287 - 1256120859 + 149723392 - v288;
v290 = v286 - 1421591606 - v289 + 2;
v285 += 1989232579;
v291 = v289 + 1 - v290;
v292 = 2 * (v288 - 685621057) + 1;
v293 = v290 - v291 - v285;
v294 = v285 - v292;
v295 = v291 - 1661767175 + 42969351;
v296 = v294 + v294 + v293 - 1972384502 + 2 - 1576459347 + 1;
v297 = v295 + v292 - 396668767 - 1534437557;
v298 = v296 + v294 - 1645192742 - v295 - 1479631423 + 2 - 331301694;
v299 = v296 - 106622097 + 668588646;
v300 = 2 * (v299 + v297 + v295 + 1 + 2) - 1263581112;
v297 += 1979779660;
v301 = v297 + v300 + v299 + 1343345468 + 481569519;
v298 += 861842343;
v302 = v298 + v300 - 1650922112 + 1803040625 - 1103549091 + 1;
v303 = v298 + v301 - 263499248;
v304 = v303 + v298;
v305 = v304++ + v302 - 438171503;
v306 = v297 - 2076009387 + 1524090740 - v304 + 1;
v304 += 575953311;
v307 = v305 + 1306759242 - v306;
v308 = v303 - 429496975 + 1812284714 - v307++;
v309 = 2 * (v306 + 1523384106) - 1468869015;
v310 = v304 + v308 + 1260443893 - v309;
v311 = v309 - 1158775838 - v307++;
v312 = 2 * v310 - 441360349;
v313 = v311 - v312;
v314 = v313++ + v307 + v304 - 1384238736;
v315 = 2 * v307 - v313 + 496097820;
v316 = v315 + v314 + 2 + 1;
v315 += 3;
v317 = 2 * (2 * v312 + 3 - v316 + 2070720611) - 1285251516 + 88029981;
v318 = v315 + v313 - 1389710860;
v319 = v315 - v318;
v320 = v319 + v319 + v316 - 589472948 + 1;
++v319;
v321 = 2 * v317 + 942166371;
v322 = v320 + v318 - 344804349 + 849785358;
v323 = v320 - v321;
v322 += 53013894;
v324 = v321 - v319;
v325 = v322 + v323 + 1;
v326 = 4 * (v325 + v319 - v322 - 2049097191 + 1);
v322 -= 1029516387;
v327 = v325 + 473722879 - v322;
v326 -= 1652737171;
v328 = v324 + 1 - v326;
v329 = v326 - v327;
v322 += 1088562794;
v327 += 78577575;
v330 = v329 - v322 - v327 + 132302044;
v328 -= 771106090;
v322 += 2;
v331 = v330 + 1 - v328;
v332 = v327 - v331;
v333 = v332 + v328;
v332 += 1152138250;
v334 = v322 + v331 - 1557943841 + 1;
v335 = v332 + v322 - v334;
v336 = v333 + 1293271530 - v332 - v335;
v334 += 245975965;
v337 = v334 + v335 + 2098061773;
v332 += 1210065134;
v338 = v334 - v336 + 1;
v339 = v337 + 1 - v332 + 1042845593;
v332 += 1017773432;
v340 = v336 - v338 + 544855734;
v341 = v340 + 2 * v339 + 1636319835;
v340 -= 2122376282;
v342 = v332 + v332 + v338 - 213405862;
v332 += 1914409404;
v343 = 2 * (v341 + 1) - v340 + 1026384791;
v344 = v332 + v342 - 207594250 + 1367733505 - v340;
v345 = v340 - v343++ + 1434173388;
v346 = v344 - 1373169356 - v332++;
v347 = v332 + v346 - 1698350246 + 807585909 - v343 - 1616726979;
v348 = v343 - v332;
v349 = v348 + v347;
v350 = v349++ + v348 + 1;
v351 = 2 * (v345 - 28630427 + 560310549 - v350 + 1) + 1587875006 - v349 - 258344410;
v352 = v332 - 390257379 + 1 - v349;
v353 = v352 + v349;
v354 = v352++ + v350 + 4;
v355 = v351 + 1 - v352;
v354 -= 1828963202;
v356 = v354 + 2 * v352 + 1;
v357 = v356 + v355 - 1265518153 + 1354618067;
v358 = v354 + v356 - v357;
v354 += 24457593;
v358 += 2081985567;
v359 = v354 + v353 + 1624829730 + 1;
v360 = 2 * (v358 + v357 - 1949374989) + 781522725;
v361 = ++v354 + v358;
v362 = v354 + 1493767541 - v359;
v361 += 4;
v363 = 2 * v359 - v361 - 1727523967;
v364 = v362 + v361 + v360 + 218569202 - v363 + 449916241;
v363 += 327109260;
v365 = v362 + 1549803007 - v363 + 957128236;
v363 += 916862246;
v366 = 2 * (v364 + 414246669) + 2040411505;
v367 = v365 + 536918145 - v366;
v368 = v366 - v367 + 1;
v369 = 2 * (v367 - 129161079 - v363 + 1) - 1900300983;
v370 = 2 * (v361 - 798140456) + 4;
v371 = v370 + v363 - 665700202 + 2;
v369 += 30341174;
v372 = v370 + 1 - v369 - 1952101394;
v373 = v372 + v369 - v371;
v374 = v373 + v371;
v375 = 2 * (v374 + v372 + 1 - 1317292497);
v376 = v373 - 2112199059 + 419983391;
v377 = v376 + 2 * (v368 - 1343830370 + 442537035) - 1033591519 + 1879391070 - v375 - 2060553041 + 1;
v378 = v375 + v375 + v374 + 738693954 + 1 - v377;
v379 = v375 + 1 - v377;
v380 = v377 - 1930629742 - v379 - 1928040188 + 1102478597;
v381 = v380 + 2 * v379 + 1 - 448866693;
v376 -= 2055000006;
v382 = 2 * (2 * (v380 + 604066061) + 2);
v383 = v382 + v376 + v381 - 1881910858;
v384 = v378 - 947925440 + 2;
v385 = v384 + v383 + v382 + 842529404 + 1;
v376 -= 168380786;
++v384;
v386 = v376 + v383 + 1;
v387 = v376 - v384 + 1919090703;
v388 = 2 * (v384 + 1 - v386 + 1) - 376075359 - v387;
v389 = v388 + v386 - 1078951762;
v388 += 4;
v390 = v388 + v387 + 1;
v388 += 1398399335;
v391 = v390 + v385 - 1475310267 - v389 + 1 + 9540715;
v392 = v389 - 1641637778 + 2 - v388 + 2;
v393 = v388 - 1972219276 + 1;
v392 -= 866747255;
v394 = v392 + v390 - 1373171668 + 1586106979;
v395 = v393 + v391 - 931348898;
v396 = v394 + v392 - 1900058436 - v395;
v397 = 2 * v394 + 1334476417;
v398 = v396 - 467332541 + 1817029648;
v399 = 2 * (v393 + 808026034) - 1047285892 + 609483421 - v397;
v395 += 1953163588;
v400 = v397 - 292607806 - v399 - 42192282 - v395 + 1;
v401 = v399 + 1 - v398 + 1;
v402 = v395 + 1 - v401;
v403 = v400 - v402;
v404 = v401 + 1 - v403 + 1872425146;
v405 = v398 - 195196821 + 377105645 - v404 - v404;
v406 = v402 - v404;
v407 = v404 - 1842186611 + 547686199;
v408 = v407 + v403 + 1374530959 - v405 + 1 - 184314042;
v409 = v405 - 1871472347 + 1;
v410 = v409 + v406;
v409 += 2027045620;
v411 = v409 + v410 - 855357098 + 1 - 2037318886;
v412 = v411 + v408 + 1324830997 - v409 + 1863672173;
v413 = 2 * (v407 - 1311778367) + 1;
v414 = v413 + v411;
v409 += 638982232;
v415 = v412 - 1420319999 - v409 + 1706741566;
v413 += 2;
v416 = v409 + 600153250 - v415 - 1749613292 + 1;
v417 = v415 - v413;
v418 = v414 - 103143630 + 151909657 - v416 + 1;
v419 = 2 * v413 - v416++;
v420 = v417 + 1 - ++v419;
v421 = v418 - v416 - v416 + v419;
v420 -= 1385665685;
return v420+ v421+ 1+ 640484926+ 2 * (v421 + v416 + 1815285368)+ v420+ v421+ 1+ 640484926+ v420+ v421+ 1+ v420+ v421 + 1+ v420- 1389466703+ 495424244+ 2 * (v420 + v421 + 1 + 640484926);
}
正如你所看到的，F5(Hex-Rays插件)在这种情况下没有实质性的帮助。 由于IDA和Hex-Rays是高度可编程的，因此其实可以自己改进Hex-Rays反编译器的输出并教导它简化这些表达式（当然这就算是另一个话题了）。除非我们将这个函数作为黑盒算法来处理，否则我们通过F5并真正理解它的操作。 我们将使用Z3库并查看它是否可以将所有这些指令简化为可读的有意义的内容。
Z3库的快速上手
Dennis和Eric对Z3的介绍已经做得很好，因此我会尽量缩短关于Z3的基础部分的章节。假设我们遇到这样一段汇编代码：
Z3库的快速上手
.text:0040EF04 mov eax, [ebp+c1]
.text:0040EF07 mov edx, [ebp+c2]
.text:0040EF0A mov ecx, [ebp+c3]
.text:0040EF0D mov ebx, [ebp+c4]
.text:0040EF10 inc eax
.text:0040EF11 inc ebx
.text:0040EF12 inc edx
.text:0040EF13 inc ecx
.text:0040EF14 add ebx, edx
.text:0040EF16 add ecx, 123h
.text:0040EF1C add eax, ebx
.text:0040EF1E add ebx, 456h
.text:0040EF24 add edx, eax
.text:0040EF26 add ecx, eax
.text:0040EF28 add edx, ebx
.text:0040EF2A sub eax, 12312312h
.text:0040EF2F add ecx, eax
.text:0040EF31 add eax, ebx
.text:0040EF33 add eax, ecx
.text:0040EF35 add eax, edx
.text:0040EF37 mov [ebp+result], eax
从0x040EF04到0x040EF0D，我们看到eax == c1，edx == c2，ecx == c3，ebx == c4（4个输入参数）。从0x040EF10到0x040EF35，我们看到一些操作发生，并且操作的结果被复制到0x040EF37处的eax。我们可以将上面的列表翻译成一系列表达式：
.text:0040EF04 mov eax, [ebp+c1]
.text:0040EF07 mov edx, [ebp+c2]
.text:0040EF0A mov ecx, [ebp+c3]
.text:0040EF0D mov ebx, [ebp+c4]
.text:0040EF10 inc eax
.text:0040EF11 inc ebx
.text:0040EF12 inc edx
.text:0040EF13 inc ecx
.text:0040EF14 add ebx, edx
.text:0040EF16 add ecx, 123h
.text:0040EF1C add eax, ebx
.text:0040EF1E add ebx, 456h
.text:0040EF24 add edx, eax
.text:0040EF26 add ecx, eax
.text:0040EF28 add edx, ebx
.text:0040EF2A sub eax, 12312312h
.text:0040EF2F add ecx, eax
.text:0040EF31 add eax, ebx
.text:0040EF33 add eax, ecx
.text:0040EF35 add eax, edx
.text:0040EF37 mov [ebp+result], eax
.text:0040EF10 eax = eax + 1
.text:0040EF11 ebx = ebx + 1
.text:0040EF12 edx = edx + 1
.text:0040EF13 ecx = ecx + 1
.text:0040EF14 ebx = ebx + edx
.text:0040EF16 ecx = ecx + 0x123
.text:0040EF1C eax = eax + ebx
.text:0040EF1E ebx = ebx + 0x456
.text:0040EF24 edx = edx + eax
.text:0040EF26 ecx = ecx + eax
.text:0040EF28 edx = edx + ebx
.text:0040EF2A eax = eax - 0x12312312
.text:0040EF2F ecx = ecx + eax
.text:0040EF31 eax = eax + ebx
.text:0040EF33 eax = eax + ecx
.text:0040EF35 eax = eax + edx
.text:0040EF10 eax = eax + 1
.text:0040EF11 ebx = ebx + 1
.text:0040EF12 edx = edx + 1
.text:0040EF13 ecx = ecx + 1
.text:0040EF14 ebx = ebx + edx
.text:0040EF16 ecx = ecx + 0x123
.text:0040EF1C eax = eax + ebx
.text:0040EF1E ebx = ebx + 0x456
.text:0040EF24 edx = edx + eax
.text:0040EF26 ecx = ecx + eax
.text:0040EF28 edx = edx + ebx
.text:0040EF2A eax = eax - 0x12312312
.text:0040EF2F ecx = ecx + eax
.text:0040EF31 eax = eax + ebx
.text:0040EF33 eax = eax + ecx
.text:0040EF35 eax = eax + edx
现在让我们把这些表达式通过Z3库来表示一下（注意Z3重载算术运算符）：
import z3
c1, c2, c3, c4 = z3.BitVecs('c1 c2 c3 c4', 32)
eax, edx, ecx, ebx = c1, c2, c3, c4
eax = eax + 1
ebx = ebx + 1
edx = edx + 1
ecx = ecx + 1
ebx = ebx + edx
ecx = ecx + 0x123
eax = eax + ebx
ebx = ebx + 0x456
edx = edx + eax
ecx = ecx + eax
edx = edx + ebx
eax = eax - 0x12312312
ecx = ecx + eax
eax = eax + ebx
eax = eax + ecx
eax = eax + edx
print(eax)
import z3
c1, c2, c3, c4 = z3.BitVecs('c1 c2 c3 c4', 32)
eax, edx, ecx, ebx = c1, c2, c3, c4
eax = eax + 1
ebx = ebx + 1
edx = edx + 1
ecx = ecx + 1
ebx = ebx + edx
ecx = ecx + 0x123
eax = eax + ebx
ebx = ebx + 0x456
edx = edx + eax
ecx = ecx + eax
edx = edx + ebx
eax = eax - 0x12312312
ecx = ecx + eax
eax = eax + ebx
eax = eax + ecx
eax = eax + edx
print(eax)
最后的结果是：
c1 + 1 + c4 + 1 + c2 + 1 - 305210130 +c4 + 1 + c2 + 1 + 1110 + c3 +1 + 291 + c1 + 1 + c4 + 1 + c2 +1 + c1 + 1 + c4 + 1 + c2 + 1 - 305210130 +c2 + 1 + c1 + 1 + c4 + 1 + c2 + 1 + c4 + 1 +c2 + 1 + 1110
c1 + 1 + c4 + 1 + c2 + 1 - 305210130 +c4 + 1 + c2 + 1 + 1110 + c3 +1 + 291 + c1 + 1 + c4 + 1 + c2 +1 + c1 + 1 + c4 + 1 + c2 + 1 - 305210130 +c2 + 1 + c1 + 1 + c4 + 1 + c2 + 1 + c4 + 1 +c2 + 1 + 1110
然而，我们仍然可以通过调用z3.simplify（eax）来让Z3简化最终的表达式，并获得更为简单的输出：
3684549565 + 4*c1 + 6*c4 + 7*c2 + c3
现在我们有了最后的简化的表达式，我们可以对这个表达式进行求解：
solver = z3.Solver()
result = z3.BitVec('result', 32)
solver.add(c1 == 1,
c2 == 2,
c3 == 3,
c4 == 4,
eax == result)
if solver.check() == z3.sat:
m = solver.model()
print("result=%08X" % m[result].as_long())
solver = z3.Solver()
result = z3.BitVec('result', 32)
solver.add(c1 == 1,
c2 == 2,
c3 == 3,
c4 == 4,
eax == result)
if solver.check() == z3.sat:
m = solver.model()
print("result=%08X" % m[result].as_long())
最终，我们让解算器在给定 c1 == 1，c2 == 2，c3 == 3和c4 == 4的情况下查找表达式的结果（eax == result）。输出为restult= DB9DC3F1。
将汇编转成Z3表达式
[招生]科锐逆向工程师培训(2024年11月15日实地，远程教学同时开班, 第51期)
最后于 2018-9-19 18:08
被skeep编辑
，原因： 部分内容被折叠，新版UI发布后重新修改代码格式
