Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file script.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246(**************************************************************************)(* This file is part of BINSEC. *)(* *)(* Copyright (C) 2016-2023 *)(* 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). *)(* *)(**************************************************************************)openTypesmoduleExpr=structincludeDba.Exprletneg=uminusletsucce=adde(constant(Bitvector.createZ.one(size_ofe)))endmodulePexpr:Ast_types.PARSER_EXPRESSIONwithtypeexpr:=Expr.t=structtypet=IntofZ.t|ExprofExpr.tletint_to_exprni=ifZ.numbitsi>nthenOptions.Logger.fatal"integer %a does not fit in %a"Z.pp_printi(funppfn->ifn=1thenFormat.pp_print_stringppf"bool"elseFormat.fprintfppf"bitvector of %d bits"n)nelseExpr.constant(Bitvector.createin)letto_exprnx=matchxwith|Inti->int_to_exprni|Expre->ifExpr.size_ofe<>nthenOptions.Logger.fatal"%a was expected to be a bitvector of %d bit%s"Dba_printer.Ascii.pp_bl_termen(ifn=1then""else"s")elseeletto_bool=to_expr1letunary(o:Dba.Unary_op.t)x=matchxwith|Int_->Options.Logger.fatal"unable to apply %a operator on an integer"Dba_printer.Ascii.pp_unary_opo|Expre->Expr(Expr.unaryoe)letbinary(o:Dba.Binary_op.t)xy=match(x,y)with|Int_,Int_->Options.Logger.fatal"unable to apply %a operator on two integers"Dba_printer.Ascii.pp_binary_opo|Inti,Expre->ExprExpr.(binaryo(int_to_expr(size_ofe)i)e)|Expre,Inti->ExprExpr.(binaryoe(int_to_expr(size_ofe)i))|Expre,Expre'->Expr(Expr.binaryoee')letadd=binaryPlusletsub=binaryMinusletmul=binaryMultletneg=unaryUMinusletudiv=binaryDivUletumod=binaryModUleturem=binaryModUletsdiv=binaryDivSletsmod=binaryModSletsrem=binaryModSletequal=binaryEqletdiff=binaryDiffletule=binaryLeqUletuge=binaryGeqUletult=binaryLtUletugt=binaryGtUletsle=binaryLeqSletsge=binaryGeqSletslt=binaryLtSletsgt=binaryGtSletlogand=binaryAndletlogor=binaryOrletlognot=unaryNotletlogxor=binaryXorletshift_left=binaryLShiftletshift_right=binaryRShiftUletshift_right_signed=binaryRShiftSletrotate_left=binaryLeftRotateletrotate_right=binaryRightRotateletsextnx=unary(Sextn)xletuextnx=unary(Uextn)xletrestrictlohix=matchxwith|Inti->letn=hi-lo+1inExpr(Expr.constant(Bitvector.create(Z.extractilon)n))|Expre->Expr(Expr.restrictlohie)letappendxy=match(x,y)with|Int_,_|_,Int_->Options.Logger.fatal"unable to concatenate integer without size"|Expra,Exprb->Expr(Expr.append ab)letitecxy=lett,e=match(x,y)with|Int_,Int_->Options.Logger.fatal"unable to infer the size of ite body"|Inti,Expre->(int_to_expr(Expr.size_ofe)i,e)|Expre,Inti->(e,int_to_expr(Expr.size_ofe)i)|Expre,Expre'->(e,e')inExpr(Expr.itecte)endmoduleLValue=Dba.LValuemoduleInstr=structtypet=|AssignofLValue.t*Expr.t|UndefofLValue.t|NondetofLValue.t|AssumeofExpr.t|AssertofExpr.t|ItofExpr.t*string|Gotoofstring|JumpofExpr.t|Labelofstring|Haltletassignlocvalue=Assign(loc,value)letundefloc=Undeflocletnondetloc=Nondetlocletassumetest=Assumetestletdynamic_asserttest=Asserttestletconditional_jumptesttarget=It(test,target)letgototarget=Gototargetletdynamic_jumptarget=Jumptargetletlabelname=Labelnamelethalt=Haltletpp_listppfhunk=Format.pp_open_vboxppf0;Format.pp_open_vboxppf2;List.iter(funinstr->matchinstrwith|Assign(lval,rval)->Format.fprintfppf"@ @[<hov>%a := %a@]"Dba_printer.Ascii.pp_lhslvalDba_printer.Ascii.pp_bl_termrval|Undeflval->Format.fprintfppf"@ @[<hov>%a := \\undef@]"Dba_printer.Ascii.pp_lhslval|Nondetlval->Format.fprintfppf"@ @[<hov>%a := \\nondet@]"Dba_printer.Ascii.pp_lhslval|Assumetest->Format.fprintfppf"@ @[<hov>assume %a@]"Dba_printer.Ascii.pp_bl_termtest|Asserttest->Format.fprintfppf"@ @[<hov>assert %a]"Dba_printer.Ascii.pp_bl_termtest|It(test,target)->Format.fprintfppf"@ @[<hov>if %a@ goto %s@]"Dba_printer.Ascii.pp_bl_termtesttarget|Gototarget->Format.fprintfppf"@ goto %s"target|Jumptarget->Format.fprintfppf"@ @[<hov>jump %a@]"Dba_printer.Ascii.pp_bl_termtarget|Labelname->Format.fprintfppf"@]@ @[<v 2>%s:"name|Halt->Format.fprintfppf"@ halt")hunk;Format.pp_close_boxppf();Format.pp_close_boxppf()endmoduleDirective=structtypet=|CutofExpr.toption|AssumeofExpr.t|AssertofExpr.t|Reachofint*Expr.toption*Output.tlist|Enumerateofint*Expr.tendtypet=|Start_fromofExpr.t*Instr.tlist|Start_from_coreofInstr.tlist|Load_sectionsofstringlist|Load_dataofExpr.t|Import_symbolsof(string*Dba.Var.Tag.attribute)list*string|StubofExpr.tlist*Instr.tlist|InitofInstr.tlist|DirectiveofExpr.t*Directive.t