Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file smt2_solver.ml
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717817918018118218318418518618718818919019119219319419519619719819920020120220320420520620720820921021121221321421521621721821922022122222322422522622722822923023123223323423523623723823924024124224324424524624724824925025125225325425525625725825926026126226326426526626726826927027127227327427527627727827928028128228328428528628728828929029129229329429529629729829930030130230330430530630730830931031131231331431531631731831932032132232332432532632732832933033133233333433533633733833934034134234334434534634734834935035135235335435535635735835936036136236336436536636736836937037137237337437537637737837938038138238338438538638738838939039139239339439539639739839940040140240340440540640740840941041141241341441541641741841942042142242342442542642742842943043143243343443543643743843944044144244344444544644744844945045145245345445545645745845946046146246346446546646746846947047147247347447547647747847948048148248348448548648748848949049149249349449549649749849950050150250350450550650750850951051151251351451551651751851952052152252352452552652752852953053153253353453553653753853954054154254354454554654754854955055155255355455555655755855956056156256356456556656756856957057157257357457557657757857958058158258358458558658758858959059159259359459559659759859960060160260360460560660760860961061161261361461561661761861962062162262362462562662762862963063163263363463563663763863964064164264364464564664764864965065165265365465565665765865966066166266366466566666766866967067167267367467567667767867968068168268368468568668768868969069169269369469569669769869970070170270370470570670770870971071171271371471571671771871972072172272372472572672772872973073173273373473573673773873974074174274374474574674774874975075175275375475575675775875976076176276376476576676776876977077177277377477577677777877978078178278378478578678778878979079179279379479579679779879980080180280380480580680780880981081181281381481581681781881982082182282382482582682782882983083183283383483583683783883984084184284384484584684784884985085185285385485585685785885986086186286386486586686786886987087187287387487587687787887988088188288388488588688788888989089189289389489589689789889990090190290390490590690790890991091191291391491591691791891992092192292392492592692792892993093193293393493593693793893994094194294394494594694794894995095195295395495595695795895996096196296396496596696796896997097197297397497597697797897998098198298398498598698798898999099199299399499599699799899910001001100210031004100510061007100810091010101110121013101410151016101710181019102010211022102310241025102610271028102910301031103210331034103510361037103810391040104110421043104410451046104710481049105010511052105310541055105610571058105910601061106210631064106510661067106810691070107110721073107410751076107710781079108010811082108310841085108610871088108910901091109210931094109510961097109810991100110111021103110411051106110711081109111011111112111311141115111611171118111911201121112211231124112511261127112811291130113111321133113411351136113711381139114011411142114311441145114611471148114911501151115211531154115511561157115811591160116111621163116411651166116711681169117011711172117311741175117611771178117911801181118211831184118511861187118811891190119111921193119411951196119711981199120012011202120312041205120612071208120912101211121212131214121512161217121812191220122112221223(**************************************************************************)(* This file is part of BINSEC. *)(* *)(* Copyright (C) 2016-2024 *)(* CEA (Commissariat à l'énergie atomique et aux énergies *)(* alternatives) *)(* *)(* you can redistribute it and/or modify it under the terms of the GNU *)(* Lesser General Public License as published by the Free Software *)(* Foundation, version 2.1. *)(* *)(* It is distributed in the hope that it will be useful, *)(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)(* GNU Lesser General Public License for more details. *)(* *)(* See the GNU Lesser General Public License version 2.1 *)(* for more details (enclosed in the file licenses/LGPLv2.1). *)(* *)(**************************************************************************)letbyte_size=Natural.to_intBasic_types.Constants.bytesizemoduleSession=structletn=ref0typestate=Dead|Assert|Sat|Unsattypesession={solver:Prover.t;mutablestate:state;pid:Subprocess.t;stdin:out_channel;stdout:in_channel;stderr:in_channel;stdlog:out_channeloption;fdlog:out_channeloption;formatter:Format.formatter;}letcloset=ignore@@Subprocess.closet.pid;matcht.fdlogwithNone->()|Somefd->close_outfdletstart?stdlogtimeoutsolver=Options.Logger.debug"Openning session %d"!n;letfdlog=matchSmt_options.SMT_dir.get_opt()with|None->None|Somedir->ifnot(Sys.file_existsdir)thenUnix.mkdirdir0o777;letfilename=Filename.concatdir(Printf.sprintf"query_%d.smt2"!n)inSome(open_outfilename)inincrn;letcmd=Prover.command~incremental:truetimeoutsolverinletpid=Subprocess.spawn~pdeathsig:Sys.sigkillcmdinletstdin=Subprocess.stdinpidandstdout=Subprocess.stdoutpidandstderr=Subprocess.stderrpidinletformatter=match(stdlog,fdlog)with|None,None->Format.formatter_of_out_channelstdin|Somestdlog,None->letoutputstrposlen=output_substringstdlogstrposlen;output_substringstdinstrposlenandflush()=flushstdlog;flushstdininFormat.make_formatteroutputflush|None,Somefdlog->letoutputstrposlen=output_substringfdlogstrposlen;output_substringstdinstrposlenandflush()=flushfdlog;flushstdininFormat.make_formatteroutputflush|Somestdlog,Somefdlog->letoutputstrposlen=output_substringstdlogstrposlen;output_substringfdlogstrposlen;output_substringstdinstrposlenandflush()=flushstdlog;flushfdlog;flushstdininFormat.make_formatteroutputflushinFormat.fprintfformatter"@[<v 0>(set-option :print-success false)@ (set-info :smt-lib-version \
2.5)@ (set-logic QF_ABV)@ @]";{solver;state=Assert;pid;stdin;stdout;stderr;stdlog;fdlog;formatter;}typestatus=SAT|UNSAT|UNKNOWNletcheck_satt=Format.fprintft.formatter"(check-sat)@.";matchinput_linet.stdoutwith|"sat"->t.state<-Sat;SAT|"unsat"->t.state<-Unsat;UNSAT|"unknown"->t.state<-Assert;UNKNOWN|s->Options.Logger.fatal"Solver returned: %s"s|exceptionEnd_of_file->t.state<-Dead;UNKNOWNletvalue_of_constantcst=letopenSmtlibinmatchcstwith|CstBoolfalse->Z.zero|CstBooltrue->Z.one|CstBinaryb->Z.of_string_base2b|CstDecimald|CstDecimalSize(d,_)->Z.of_string_base10d|CstHexadecimalx->Z.of_string_base16x|CstNumeral_|CstString_->Options.Logger.fatal"Model construction: unexpected constant %a as bitvector value"Smtlib_pp.pp_spec_constantcstletget_valuetppx=assert(t.state=Sat);Format.fprintft.formatter"(get-value (%a))@."ppx;letlexbuf=Lexing.from_channelt.stdoutinletopenSmtlibinmatchSmtlib_parser.ivalueSmtlib_lexer.tokenlexbufwith|[(_,{term_desc=TermSpecConstantcst;_})]->value_of_constantcst|_->assertfalseletputtppx=ppt.formatterx;Format.pp_print_spacet.formatter();t.state<-Assertend(* utils *)letpp_int_as_bvppfx=function|1->Format.fprintfppf"#b%d"(xland1)|4->Format.fprintfppf"#x%01x"(xland0xf)|8->Format.fprintfppf"#x%02x"(xland0xff)|12->Format.fprintfppf"#x%03x"(xland0xfff)|16->Format.fprintfppf"#x%04x"(xland0xffff)|20->Format.fprintfppf"#x%05x"(xland0xfffff)|24->Format.fprintfppf"#x%06x"(xland0xffffff)|28->Format.fprintfppf"#x%07x"(xland0xfffffff)|32->Format.fprintfppf"#x%08x"(xland0xffffffff)|szwhenx<0->Format.fprintfppf"(_ bv%a %d)"Z.pp_print(Z.extract(Z.of_intx)0sz)sz|sz->Format.fprintfppf"(_ bv%d %d)"xszletpp_bvppfvaluesize=trypp_int_as_bvppf(Z.to_intvalue)sizewithZ.Overflow->Format.fprintfppf"(_ bv%a %d)"Z.pp_print(ifZ.ltvalueZ.zerothenZ.extractvalue0sizeelsevalue)sizemodulePrinter=structopenSexprtypeterm=string*inttypeaccess=Selectofterm*int|Storeofterm*intanddef=BlofExpr.t|BvofExpr.t|AxofMemory.tandt={fvariables:Expr.tStTbl.t;farrays:Memory.tStTbl.t;mutableid:Suid.t;bv_decl:stringBvTbl.t;bl_cons:stringBvTbl.t;bv_cons:stringBvTbl.t;ax_cons:stringAxTbl.t;ax_root:Memory.tAxTbl.t;ordered_defs:defQueue.t;ordered_mem:accessQueue.tAxTbl.t;word_size:int;debug:name:string->label:string->string;}letcreate?(word_size=Kernel_options.Machine.word_size())?(debug=fun~name~label:_->name)~next_id()=letbv_cons=BvTbl.create128andbl_cons=BvTbl.create32inBvTbl.addbl_consExpr.zero"false";BvTbl.addbv_consExpr.zero"#b0";BvTbl.addbl_consExpr.one"true";BvTbl.addbv_consExpr.one"#b1";{fvariables=StTbl.create16;farrays=StTbl.create4;id=next_id;bv_decl=BvTbl.create16;bl_cons;bv_cons;ax_cons=AxTbl.create64;ax_root=AxTbl.create64;ordered_defs=Queue.create();ordered_mem=AxTbl.create4;word_size;debug;}letpp_int_as_offsetsizeppfi=pp_bvppfisizeletonce=""letrecvisit_blctxbl=tryifBvTbl.findctx.bl_consbl==oncethen(letname=Suid.to_stringctx.idinctx.id<-Suid.incrctx.id;BvTbl.replacectx.bl_consblname)withNot_found->(matchblwith|Cst_->()|Load_(* cannot be a bl<1> *)->assertfalse|Unary{f=Not;x;_}->BvTbl.addctx.bl_consblonce;visit_blctxx;Queue.push(Blbl)ctx.ordered_defs|Binary{f=And|Or;x;y;_}->BvTbl.addctx.bl_consblonce;visit_blctxx;visit_blctxy;Queue.push(Blbl)ctx.ordered_defs|Binary{f=Eq|Diff|Uge|Ule|Ugt|Ult|Sge|Sle|Sgt|Slt;x;y;_;}->BvTbl.addctx.bl_consblonce;visit_bvctxx;visit_bvctxy;Queue.push(Blbl)ctx.ordered_defs|Ite{c;t;e;_}->BvTbl.addctx.bl_consblonce;visit_blctxc;visit_blctxt;visit_blctxe;Queue.push(Blbl)ctx.ordered_defs|Var_|Unary_|Binary_->visit_bvctxbl)andvisit_bvctxbv=tryifBvTbl.findctx.bv_consbv==oncethen(letname=Suid.to_stringctx.idinctx.id<-Suid.incrctx.id;BvTbl.replacectx.bv_consbvname)withNot_found->(matchbvwith|Var{name;size;label;_}->StTbl.addctx.fvariablesnamebv;letname=ctx.debug~name~labelinBvTbl.addctx.bv_consbvname;ifsize=1thenBvTbl.addctx.bl_consbv(Printf.sprintf"(= %s #b1)"name);BvTbl.addctx.bv_declbv(Format.sprintf"(declare-fun %s () (_ BitVec %d))"namesize)|Load{len;addr;label;_}->BvTbl.addctx.bv_consbvonce;visit_bvctxaddr;visit_bvctxaddr;visit_axctxlabel;iflen>1thenvisit_axctxlabel;Queue.push(Bvbv)ctx.ordered_defs;letroot=AxTbl.findctx.ax_rootlabelinletordered_mem=AxTbl.findctx.ordered_memrootinQueue.push(Select((BvTbl.findctx.bv_consaddr,Expr.sizeofaddr),len))ordered_mem|Cst_->BvTbl.addctx.bv_consbvonce;Queue.push(Bvbv)ctx.ordered_defs|Unary{x;_}->BvTbl.addctx.bv_consbvonce;visit_bvctxx;Queue.push(Bvbv)ctx.ordered_defs|Binary{f=Eq|Diff|Uge|Ule|Ugt|Ult|Sge|Sle|Sgt|Slt;_}->BvTbl.addctx.bv_consbvonce;visit_blctxbv;Queue.push(Bvbv)ctx.ordered_defs|Binary{f=Rol|Ror;x;y=(Load_|Unary_|Binary_|Ite_)asy;_;}->BvTbl.addctx.bv_consbvonce;visit_bvctxx;visit_bvctxx;visit_bvctxy;visit_bvctxy;Queue.push(Bvbv)ctx.ordered_defs|Binary{x;y;_}->BvTbl.addctx.bv_consbvonce;visit_bvctxx;visit_bvctxy;Queue.push(Bvbv)ctx.ordered_defs|Ite{c;t;e;_}->BvTbl.addctx.bv_consbvonce;visit_blctxc;visit_bvctxt;visit_bvctxe;Queue.push(Bvbv)ctx.ordered_defs)andvisit_axctx(ax:Memory.t)=tryifAxTbl.findctx.ax_consax==oncethen(letname=Suid.to_stringctx.idinctx.id<-Suid.incrctx.id;AxTbl.replacectx.ax_consaxname)withNot_found->(matchaxwith|Root->AxTbl.addctx.ax_consax(ctx.debug~name:Suid.(to_stringzero)~label:"memory");AxTbl.addctx.ax_rootaxax;AxTbl.addctx.ordered_memax(Queue.create())|Symbolname->StTbl.addctx.farraysnameax;AxTbl.addctx.ax_consaxname;AxTbl.addctx.ax_rootaxax;AxTbl.addctx.ordered_memax(Queue.create())|Layer{addr=Cst_;store;over;_}->AxTbl.addctx.ax_consaxonce;Store.iter_term(fun_bv->visit_bvctxbv;ifExpr.sizeofbv>1thenvisit_bvctxbv)store;visit_axctxover;letroot=AxTbl.findctx.ax_rootoverinAxTbl.addctx.ax_rootaxroot;Queue.push(Axax)ctx.ordered_defs;letordered_mem=AxTbl.findctx.ordered_memrootinStore.iter_term(funibv->letindex=Format.asprintf"%a"(pp_int_as_offsetctx.word_size)iinQueue.push(Store((index,ctx.word_size),Expr.sizeofbv))ordered_mem)store|Layer{addr;store;over;_}->AxTbl.addctx.ax_consaxonce;visit_bvctxaddr;visit_bvctxaddr;Store.iter_term(fun_bv->visit_bvctxbv;ifExpr.sizeofbv>1thenvisit_bvctxbv)store;visit_axctxover;letroot=AxTbl.findctx.ax_rootoverinAxTbl.addctx.ax_rootaxroot;Queue.push(Axax)ctx.ordered_defs;letordered_mem=AxTbl.findctx.ordered_memrootinletindex=BvTbl.findctx.bv_consaddrinStore.iter_term(funibv->letindex=Format.asprintf"(bvadd %s %a)"index(pp_int_as_offsetctx.word_size)iinQueue.push(Store((index,ctx.word_size),Expr.sizeofbv))ordered_mem)store)letpp_unopppf(op:Term.unaryTerm.operator)=matchopwith|Not->Format.pp_print_stringppf"bvnot"|Minus->Format.pp_print_stringppf"bvneg"|Uextn->Format.fprintfppf"(_ zero_extend %d)"n|Sextn->Format.fprintfppf"(_ sign_extend %d)"n|Restrict{Interval.hi;lo}->Format.fprintfppf"(_ extract %d %d)"hiloletpp_binop=letstring_of_binop(op:Term.binaryTerm.operator)=matchopwith|Plus->"bvadd"|Minus->"bvsub"|Mul->"bvmul"|Udiv->"bvudiv"|Sdiv->"bvsdiv"|Umod->"bvurem"|Smod->"bvsrem"|Or->"bvor"|And->"bvand"|Xor->"bvxor"|Concat->"concat"|Lsl->"bvshl"|Lsr->"bvlshr"|Asr->"bvashr"|Rol->"rotate_left"|Ror->"rotate_right"|Eq->"="|Diff->assertfalse|Ule->"bvule"|Ult->"bvult"|Uge->"bvuge"|Ugt->"bvugt"|Sle->"bvsle"|Slt->"bvslt"|Sge->"bvsge"|Sgt->"bvsgt"infunppff->Format.pp_print_stringppf(string_of_binopf)letrecprint_blctxppfbl=tryletname=BvTbl.findctx.bl_consblinifname==oncethenprint_bl_no_consctxppfblelseFormat.pp_print_stringppfnamewithNot_found->Format.pp_print_stringppf"(= ";Format.pp_print_spaceppf();print_bvctxppfbl;Format.pp_print_stringppf" #b1)"andprint_bl_no_consctxppfbl=matchblwith|Cst_(* true and false should already be in the cache *)|Load_(* cannot be a bl<1> *)->assertfalse|Unary{f=Not;x;_}->Format.pp_print_stringppf"(not";Format.pp_print_spaceppf();print_blctxppfx;Format.pp_print_charppf')'|Binary{f=(And|Or)asf;x;y;_}->Format.pp_print_charppf'(';(Format.pp_print_stringppf@@matchfwithAnd->"and"|Or->"or"|_->assertfalse);Format.pp_print_spaceppf();print_blctxppfx;Format.pp_print_spaceppf();print_blctxppfy;Format.pp_print_charppf')'|Binary{f=Diff;x;y;_}->Format.pp_print_stringppf"(not";Format.pp_print_spaceppf();Format.pp_print_stringppf"(=";Format.pp_print_spaceppf();print_bvctxppfx;Format.pp_print_spaceppf();print_bvctxppfy;Format.pp_print_stringppf"))"|Binary{f=(Eq|Uge|Ule|Ugt|Ult|Sge|Sle|Sgt|Slt)asf;x;y;_;}->Format.pp_print_charppf'(';pp_binopppff;Format.pp_print_spaceppf();print_bvctxppfx;Format.pp_print_spaceppf();print_bvctxppfy;Format.pp_print_charppf')'|Ite{c;t;e;_}->Format.pp_print_stringppf"(ite";Format.pp_print_spaceppf();print_blctxppfc;Format.pp_print_spaceppf();print_blctxppft;Format.pp_print_spaceppf();print_blctxppfe;Format.pp_print_charppf')'|Var_|Unary_|Binary_->Format.pp_print_stringppf"(=";Format.pp_print_spaceppf();print_bvctxppfbl;Format.pp_print_spaceppf();Format.pp_print_stringppf"#b1)"andprint_bvctxppfbv=letname=BvTbl.findctx.bv_consbvinifname==oncethenprint_bv_no_consctxppfbvelseFormat.pp_print_stringppfnameandprint_bv_no_consctxppfbv=matchbvwith|Var{name;_}->Format.pp_print_stringppfname|Load{len=1;addr;label;_}->Format.pp_print_stringppf"(select";Format.pp_print_spaceppf();print_axctxppflabel;Format.pp_print_spaceppf();print_bvctxppfaddr;Format.pp_print_charppf')'|Load{len;dir;addr;label;_}->Format.pp_print_stringppf"(concat";print_multi_selectdirppflen(AxTbl.findctx.ax_conslabel)(BvTbl.findctx.bv_consaddr)(Expr.sizeofaddr);Format.pp_print_charppf')'|Cstbv->letsize=Bv.size_ofbvandvalue=Bv.value_ofbvinpp_bvppfvaluesize|Unary{f;x;_}->Format.pp_print_charppf'(';pp_unopppff;Format.pp_print_spaceppf();print_bvctxppfx;Format.pp_print_charppf')'|Binary{f=Eq|Uge|Ule|Ugt|Ult|Sge|Sle|Sgt|Slt;_}->Format.pp_print_stringppf"(ite";Format.pp_print_spaceppf();print_blctxppfbv;Format.pp_print_spaceppf();Format.pp_print_stringppf"#b1";Format.pp_print_spaceppf();Format.pp_print_stringppf"#b0)"|Binary{f=Diff;x;y;_}->Format.pp_print_stringppf"(ite (=";Format.pp_print_spaceppf();print_bvctxppfx;Format.pp_print_spaceppf();print_bvctxppfy;Format.pp_print_charppf')';Format.pp_print_spaceppf();Format.pp_print_stringppf"#b0";Format.pp_print_spaceppf();Format.pp_print_stringppf"#b1)"|Binary{f=(Rol|Ror)asf;x;y=Cstbv;_}->Format.pp_print_stringppf"((_";Format.pp_print_spaceppf();pp_binopppff;Format.pp_print_spaceppf();Z.pp_printppf(Bv.value_ofbv);Format.pp_print_charppf')';Format.pp_print_spaceppf();print_bvctxppfx;Format.pp_print_charppf')'|Binary{f=(Rol|Ror)asf;x;y;_}->Format.pp_print_stringppf"(bvor";Format.pp_print_spaceppf();Format.pp_print_charppf'(';pp_binopppf(matchfwithRol->Lsl|Ror->Lsr|_->assertfalse);Format.pp_print_spaceppf();Format.pp_print_stringppf(BvTbl.findctx.bv_consx);Format.pp_print_spaceppf();Format.pp_print_stringppf(BvTbl.findctx.bv_consy);Format.pp_print_charppf')';Format.pp_print_spaceppf();Format.pp_print_charppf'(';pp_binopppf(matchfwithRol->Lsr|Ror->Lsl|_->assertfalse);Format.pp_print_spaceppf();Format.pp_print_stringppf(BvTbl.findctx.bv_consx);Format.pp_print_spaceppf();Format.pp_print_stringppf"(bvsub";Format.pp_print_spaceppf();pp_int_as_bvppf(Expr.sizeofx)(Expr.sizeofx);Format.pp_print_spaceppf();Format.pp_print_stringppf(BvTbl.findctx.bv_consy);Format.pp_print_stringppf")))"|Binary{f;x;y;_}->Format.pp_print_charppf'(';pp_binopppff;Format.pp_print_spaceppf();print_bvctxppfx;Format.pp_print_spaceppf();print_bvctxppfy;Format.pp_print_charppf')'|Ite{c;t;e;_}->Format.pp_print_stringppf"(ite";Format.pp_print_spaceppf();print_blctxppfc;Format.pp_print_spaceppf();print_bvctxppft;Format.pp_print_spaceppf();print_bvctxppfe;Format.pp_print_charppf')'andprint_axctxppfax=letname=AxTbl.findctx.ax_consaxinifname==oncethenprint_ax_no_consctxppfaxelseFormat.pp_print_stringppfnameandprint_ax_no_consctxppf(ax:Memory.t)=matchaxwith|Root->Suid.ppppfSuid.zero|Symbol_->assertfalse|Layer{addr;store;over;_}->Store.iter_term(fun_value->for_=1toExpr.sizeofvaluelsr3doFormat.pp_print_stringppf"(store";Format.pp_print_spaceppf()done)store;print_axctxppfover;letaddr_space=ctx.word_sizeinletrebase,idx=matchaddrwith|Cst_->(false,"")|_->(true,BvTbl.findctx.bv_consaddr)inletrecunroll_storeloibv=Format.pp_print_spaceppf();ifrebasethenifZ.zero=ithen(Format.pp_print_stringppfidx;Format.pp_print_spaceppf())else(Format.pp_print_stringppf"(bvadd";Format.pp_print_spaceppf();Format.pp_print_stringppfidx;Format.pp_print_spaceppf();pp_bvppfiaddr_space;Format.pp_print_charppf')')elsepp_bvppfiaddr_space;Format.pp_print_spaceppf();letsize=Expr.sizeofbvinifsize>8then(Format.fprintfppf"((_ extract %d %d)"(lo+7)lo;Format.pp_print_spaceppf();print_bvctxppfbv;Format.pp_print_stringppf"))";letlo'=lo+8iniflo'<sizethenunroll_storelo'(Z.succi)bv)else(print_bvctxppfbv;Format.pp_print_charppf')')inStore.iter_term(unroll_store0)storeandprint_multi_select=letrecprint_multi_select_leppflenaxbvsize=iflen=1thenFormat.fprintfppf" (select@ %s@ %s)"axbvelseletlen=len-1inFormat.fprintfppf" (select@ %s@ (bvadd@ %s@ "axbv;pp_int_as_bvppflensize;Format.pp_print_stringppf"))";print_multi_select_leppflenaxbvsizeinletrecprint_multi_select_beippflenaxbvsize=ifi=0then(Format.fprintfppf"@ (select@ %s@ %s)"axbv;print_multi_select_be1ppflenaxbvsize)elseifi<lenthen(Format.fprintfppf" (select@ %s@ (bvadd@ %s@ "axbv;pp_int_as_bvppfisize;Format.pp_print_stringppf"))";print_multi_select_be(i+1)ppflenaxbvsize)infunction|LittleEndian->print_multi_select_le|BigEndian->print_multi_select_be0letpp_print_declsppfctx=BvTbl.iter(fun_decl->Format.pp_print_stringppfdecl;Format.pp_print_spaceppf())ctx.bv_decl;AxTbl.iter(fun(ax:Memory.t)ordered_mem->matchaxwith|Root->Format.fprintfppf"(declare-fun %s () (Array (_ BitVec %d) (_ BitVec %d)))@ "(ctx.debug~name:Suid.(to_stringzero)~label:"memory")ctx.word_sizebyte_size|Symbolname->ifnot(Queue.is_emptyordered_mem)thenFormat.fprintfppf"(declare-fun %s () (Array (_ BitVec %d) (_ BitVec %d)))@ "namectx.word_sizebyte_size|_->assertfalse)ctx.ordered_memletpp_print_defsppfctx=Queue.iter(function|Blbl->letname=BvTbl.findctx.bl_consblinifname!=oncethen(Format.fprintfppf"@[<h>(define-fun %s () Bool "name;print_bl_no_consctxppfbl;Format.fprintfppf")@]@ ")|Bvbv->letname=BvTbl.findctx.bv_consbvinifname!=oncethen(Format.fprintfppf"@[<h>(define-fun %s () (_ BitVec %d) "name(Expr.sizeofbv);print_bv_no_consctxppfbv;Format.fprintfppf")@]@ ")|Axax->letname=AxTbl.findctx.ax_consaxinifname!=oncethen(Format.fprintfppf"@[<h>(define-fun %s () (Array (_ BitVec %d) (_ BitVec %d)) "name(Kernel_options.Machine.word_size())byte_size;print_ax_no_consctxppfax;Format.fprintfppf")@]@ "))ctx.ordered_defsletpp_print_bl=print_blletpp_print_bv=print_bvletpp_print_ax=print_axendmoduleCross=structopenSexprtypek=|BlofExpr.t|BvofExpr.t|AxofMemory.t|AssertofExpr.t|BvDefineofFormula.bv_var*Expr.t|AxDefineofFormula.ax_var*Memory.tandt={mutableid:Suid.t;bv_decl:Formula.declBvTbl.t;ax_decl:Formula.declAxTbl.t;bl_cons:Formula.bl_varBvTbl.t;bv_cons:Formula.bv_varBvTbl.t;ax_cons:Formula.ax_varAxTbl.t;ordered:kQueue.t;word_size:int;debug:name:string->label:string->string;}letcreate?(word_size=Kernel_options.Machine.word_size())?(debug=fun~name~label:_->name)~next_id()={id=next_id;bv_decl=BvTbl.create16;ax_decl=AxTbl.create1;bl_cons=BvTbl.create32;bv_cons=BvTbl.create128;ax_cons=AxTbl.create64;ordered=Queue.create();word_size;debug;}letbl_once=Formula.bl_var"!"letbv_once=Formula.bv_var"!"1letax_once=Formula.ax_var"!"11letrecvisit_blctxbl=tryifBvTbl.findctx.bl_consbl==bl_oncethen(letname=Suid.to_stringctx.idinctx.id<-Suid.incrctx.id;BvTbl.replacectx.bl_consbl(Formula.bl_varname))withNot_found->(matchblwith|Cst_->()|Load_(* cannot be a bl<1> *)->assertfalse|Unary{f=Not;x;_}->BvTbl.addctx.bl_consblbl_once;visit_blctxx;Queue.push(Blbl)ctx.ordered|Binary{f=And|Or;x;y;_}->BvTbl.addctx.bl_consblbl_once;visit_blctxx;visit_blctxy;Queue.push(Blbl)ctx.ordered|Binary{f=Eq|Diff|Uge|Ule|Ugt|Ult|Sge|Sle|Sgt|Slt;x;y;_;}->BvTbl.addctx.bl_consblbl_once;visit_bvctxx;visit_bvctxy;Queue.push(Blbl)ctx.ordered|Ite{c;t;e;_}->BvTbl.addctx.bl_consblbl_once;visit_blctxc;visit_blctxt;visit_blctxe;Queue.push(Blbl)ctx.ordered|Var_|Unary_|Binary_->visit_bvctxbl)andvisit_bvctxbv=tryifBvTbl.findctx.bv_consbv==bv_oncethen(letname=Suid.to_stringctx.idinctx.id<-Suid.incrctx.id;BvTbl.replacectx.bv_consbv(Formula.bv_varname(Expr.sizeofbv)))withNot_found->(matchbvwith|Var{name;size;label;_}->letname=ctx.debug~name~labelinletvar=Formula.bv_varnamesizeinBvTbl.addctx.bv_consbvvar;BvTbl.addctx.bv_declbv(Formula.mk_bv_declvar[])|Load{addr;label;_}->BvTbl.addctx.bv_consbvbv_once;visit_bvctxaddr;visit_axctxlabel;Queue.push(Bvbv)ctx.ordered|Cst_->BvTbl.addctx.bv_consbvbv_once;Queue.push(Bvbv)ctx.ordered|Unary{x;_}->BvTbl.addctx.bv_consbvbv_once;visit_bvctxx;Queue.push(Bvbv)ctx.ordered|Binary{f=Eq|Diff|Uge|Ule|Ugt|Ult|Sge|Sle|Sgt|Slt;_}->BvTbl.addctx.bv_consbvbv_once;visit_blctxbv;Queue.push(Bvbv)ctx.ordered|Binary{x;y;_}->BvTbl.addctx.bv_consbvbv_once;visit_bvctxx;visit_bvctxy;Queue.push(Bvbv)ctx.ordered|Ite{c;t;e;_}->BvTbl.addctx.bv_consbvbv_once;visit_blctxc;visit_bvctxt;visit_bvctxe;Queue.push(Bvbv)ctx.ordered)andvisit_axctxax=tryifAxTbl.findctx.ax_consax==ax_oncethen(letname=Suid.to_stringctx.idinctx.id<-Suid.incrctx.id;AxTbl.replacectx.ax_consax(Formula.ax_varnamectx.word_size8))withNot_found->(matchaxwith|Memory.Root->letvar=Formula.ax_var(ctx.debug~name:Suid.(to_stringzero)~label:"memory")ctx.word_size8inAxTbl.addctx.ax_consaxvar;AxTbl.addctx.ax_declax(Formula.mk_ax_declvar[])|Memory.Symbolname->letvar=Formula.ax_var(ctx.debug~name~label:"")ctx.word_size8inAxTbl.addctx.ax_consaxvar;AxTbl.addctx.ax_declax(Formula.mk_ax_declvar[])|Memory.Layer{addr;store;over;_}->AxTbl.addctx.ax_consaxax_once;visit_bvctxaddr;Store.iter_term(fun_bv->visit_bvctxbv)store;visit_axctxover;Queue.push(Axax)ctx.ordered)letassert_blctxbl=visit_blctxbl;Queue.push(Assertbl)ctx.orderedletdefine_bvctxnamebv=visit_bvctxbv;letvar=Formula.bv_varname(Expr.sizeofbv)inQueue.push(BvDefine(var,bv))ctx.orderedletdefine_axctxnameax=visit_axctxax;letvar=Formula.ax_varnamectx.word_size8inQueue.push(AxDefine(var,ax))ctx.orderedletmk_unop(op:Term.unaryTerm.operator)=matchopwith|Not->Formula.BvNot|Minus->Formula.BvNeg|Uextn->Formula.BvZeroExtendn|Sextn->Formula.BvSignExtendn|Restricti->Formula.BvExtractiletmk_comp(op:Term.binaryTerm.operator)=matchopwith|Eq->Formula.BvEqual|Diff->Formula.BvDistinct|Uge->Formula.BvUge|Ule->Formula.BvUle|Ugt->Formula.BvUgt|Ult->Formula.BvUlt|Sge->Formula.BvSge|Sle->Formula.BvSle|Sgt->Formula.BvSgt|Slt->Formula.BvSlt|Plus|Minus|Mul|Udiv|Sdiv|Umod|Smod|Or|And|Xor|Concat|Lsl|Lsr|Asr|Rol|Ror->assertfalseletmk_bnop(op:Term.binaryTerm.operator)=matchopwith|Eq|Diff|Uge|Ule|Ugt|Ult|Sge|Sle|Sgt|Slt->assertfalse|Plus->Formula.BvAdd|Minus->Formula.BvSub|Mul->Formula.BvMul|Udiv->Formula.BvUdiv|Sdiv->Formula.BvSdiv|Umod->Formula.BvUrem|Smod->Formula.BvSmod|Or->Formula.BvOr|And->Formula.BvAnd|Xor->Formula.BvXor|Concat->Formula.BvConcat|Lsl->Formula.BvShl|Lsr->Formula.BvLshr|Asr->Formula.BvAshr|Rol|Ror->assertfalseletrecmk_blctxbl=tryletvar=BvTbl.findctx.bl_consblinifvar==bl_oncethenmk_bl_no_consctxblelseFormula.mk_bl_varvarwithNot_found->Formula.mk_bv_equal(mk_bvctxbl)Formula.mk_bv_oneandmk_bl_no_consctxbl=matchblwith|Cstbv->ifBitvector.is_onebvthenFormula.mk_bl_trueelseFormula.mk_bl_false|Load_(* cannot be a bl<1> *)->assertfalse|Unary{f=Not;x;_}->Formula.mk_bl_not(mk_blctxx)|Binary{f=And;x;y;_}->Formula.mk_bl_and(mk_blctxx)(mk_blctxy)|Binary{f=Or;x;y;_}->Formula.mk_bl_or(mk_blctxx)(mk_blctxy)|Binary{f=(Eq|Diff|Uge|Ule|Ugt|Ult|Sge|Sle|Sgt|Slt)asf;x;y;_;}->Formula.mk_bv_comp(mk_compf)(mk_bvctxx)(mk_bvctxy)|Ite{c;t;e;_}->Formula.mk_bl_ite(mk_blctxc)(mk_blctxt)(mk_blctxe)|Var_|Unary_|Binary_->Formula.mk_bv_equal(mk_bvctxbl)Formula.mk_bv_oneandmk_bvctxbv=letvar=BvTbl.findctx.bv_consbvinifvar==bv_oncethenmk_bv_no_consctxbvelseFormula.mk_bv_varvarandmk_bv_no_consctxbv=matchbvwith|Var_->assertfalse|Load{len;dir=LittleEndian;addr;label;_}->Formula.mk_selectlen(mk_axctxlabel)(mk_bvctxaddr)|Load{len;dir=BigEndian;addr;label;_}->mk_select_belen(mk_axctxlabel)(mk_bvctxaddr)|Cstbv->Formula.mk_bv_cstbv|Unary{f;x;_}->Formula.mk_bv_unop(mk_unopf)(mk_bvctxx)|Binary{f=Eq|Diff|Uge|Ule|Ugt|Ult|Sge|Sle|Sgt|Slt;_}->Formula.mk_bv_ite(mk_blctxbv)Formula.mk_bv_oneFormula.mk_bv_zero|Binary{f=Rol;x;y=Cstbv;_}->Formula.mk_bv_rotate_left(Bv.to_uintbv)(mk_bvctxx)|Binary{f=Ror;x;y=Cstbv;_}->Formula.mk_bv_rotate_right(Bv.to_uintbv)(mk_bvctxx)|Binary{f=Rol;x;y;_}->Formula.mk_bv_or(Formula.mk_bv_shl(mk_bvctxx)(mk_bvctxy))(Formula.mk_bv_lshr(mk_bvctxx)(Formula.mk_bv_sub_int(mk_bvctxy)(Expr.sizeofx)))|Binary{f=Ror;x;y;_}->Formula.mk_bv_or(Formula.mk_bv_lshr(mk_bvctxx)(mk_bvctxy))(Formula.mk_bv_shl(mk_bvctxx)(Formula.mk_bv_sub_int(mk_bvctxy)(Expr.sizeofx)))|Binary{f;x;y;_}->Formula.mk_bv_bnop(mk_bnopf)(mk_bvctxx)(mk_bvctxy)|Ite{c;t;e;_}->Formula.mk_bv_ite(mk_blctxc)(mk_bvctxt)(mk_bvctxe)andmk_axctxax=letvar=AxTbl.findctx.ax_consaxinifvar==ax_oncethenmk_ax_no_consctxaxelseFormula.mk_ax_varvarandmk_ax_no_consctxax=matchaxwith|Memory.Root|Memory.Symbol_->assertfalse|Memory.Layer{addr;store;over;_}->letaddr=mk_bvctxaddrinStore.fold_term(funibvstore->Formula.mk_store1store(Formula.mk_bv_addaddr(Formula.mk_bv_cst(Bitvector.createictx.word_size)))(mk_bvctxbv))(mk_axctxover)storeandmk_select_be=letrecmk_select_belenaxbvsel=iflen=0thenselelseletlen=len-1inmk_select_belenaxbv(Formula.mk_bv_concatsel(Formula.mk_select1ax(Formula.mk_bv_add_intbvlen)))infunlenaxbv->letlen=len-1inmk_select_belenaxbv(Formula.mk_select1ax(Formula.mk_bv_add_intbvlen))letto_formulactx=Queue.fold(funformula->function|Blbl->letvar=BvTbl.findctx.bl_consblinifvar!=bl_oncethenFormula.push_front_define(Formula.mk_bl_defvar[](mk_bl_no_consctxbl))formulaelseformula|Bvbv->letvar=BvTbl.findctx.bv_consbvinifvar!=bv_oncethenFormula.push_front_define(Formula.mk_bv_defvar[](mk_bv_no_consctxbv))formulaelseformula|Axax->letvar=AxTbl.findctx.ax_consaxinifvar!=ax_oncethenFormula.push_front_define(Formula.mk_ax_defvar[](mk_ax_no_consctxax))formulaelseformula|Assertbl->Formula.push_front_assert(mk_blctxbl)formula|BvDefine(var,bv)->Formula.push_front_define(Formula.mk_bv_defvar[](mk_bvctxbv))formula|AxDefine(var,ax)->Formula.push_front_define(Formula.mk_ax_defvar[](mk_axctxax))formula)(BvTbl.fold(fun_declformula->Formula.push_front_declaredeclformula)ctx.bv_decl(AxTbl.fold(fun_declformula->Formula.push_front_declaredeclformula)ctx.ax_declFormula.empty))ctx.orderedendmoduleSolver():Solver_sig.S=structopenSexprtyperesult=Sat|Unsat|Unknowntypeterm=Printer.termletput(ctx:Printer.t)ppfconstraints=Format.pp_open_vboxppf0;(* visit assertions *)List.iter(Printer.visit_blctx)constraints;(* print declarations *)Printer.pp_print_declsppfctx;(* print assertions *)Format.pp_open_hovboxppf0;Printer.pp_print_defsppfctx;List.iter(funbl->Format.pp_print_stringppf"(assert ";Printer.print_blctxppfbl;Format.pp_print_charppf')';Format.pp_print_spaceppf())constraints;Format.pp_close_boxppf();Format.pp_close_boxppf()letsession=Session.start(* ~stdlog:stderr *)(Formula_options.Solver.Timeout.get())(Formula_options.Solver.get())letctx=refNoneletbindfideconstraints=letctx=letx=Printer.create~next_id:fid()inctx:=Somex;xinPrinter.visit_axctxMemory.root;Printer.visit_bvctxe;Printer.visit_bvctxe;putctxsession.formatterconstraints;(BvTbl.findctx.bv_conse,Expr.sizeofe)letputfidconstraints=letctx=letx=Printer.create~next_id:fid()inctx:=Somex;xinPrinter.visit_axctxMemory.root;putctxsession.formatterconstraintsletgete=(BvTbl.find(Option.get!ctx).bv_conse,Expr.sizeofe)letset_memory~addry=Session.putsession(funppf()->Format.fprintfppf"(assert (= (select %s "Suid.(to_stringzero);Format.pp_print_charppf' ';pp_bvppfaddr(Option.get!ctx).Printer.word_size;Format.pp_print_stringppf") ";pp_bvppfy8;Format.pp_print_stringppf"))")()letneq(e,s)x=Session.putsession(funppf()->Format.fprintfppf"(assert (not (= %s "e;pp_bvppfxs;Format.pp_print_stringppf")))")()letget_value(x,_)=Session.get_valuesessionFormat.pp_print_stringxletget_atnamexs=Session.get_valuesession(funppfx->Format.pp_print_stringppf"(select ";Format.pp_print_stringppfname;Format.pp_print_charppf' ';pp_bvppfxs;Format.pp_print_charppf')')xletiter_free_variablesf=StTbl.iterf(Option.get!ctx).fvariablesletiter_free_arraysf=StTbl.iterf(Option.get!ctx).farraysletget_arrayar=matchAxTbl.find(Option.get!ctx).ordered_memarwith|exceptionNot_found->[||]|history->ifQueue.is_emptyhistorythen[||]elseletdirty=BiTbl.create(Queue.lengthhistory)inletname=Format.asprintf"%a"(Printer.pp_print_ax(Option.get!ctx))arandaddr_space=(Option.get!ctx).word_sizeinletbinding=Queue.fold(funbinding(access:Printer.access)->matchaccesswith|Select(index,len)->letindex=get_valueindexinletrecfoldindexlenbinding=iflen=0thenbindingelseifBiTbl.memdirtyindexthenfold(Z.succindex)(len-1)bindingelseletk=get_atnameindexaddr_spaceinfold(Z.succindex)(len-1)((index,Char.unsafe_chr(Z.to_intk))::binding)infoldindexlenbinding|Store(index,len)->letindex=get_valueindexinletrecloopindexlen=iflen<>0then(BiTbl.replacedirtyindex();loop(Z.succindex)(len-1))inloopindexlen;binding)[]historyinArray.of_listbindingletcheck_sat()=matchSession.check_satsessionwith|UNKNOWN->Unknown|UNSAT->Unsat|SAT->Satletclose()=Session.closesessionend