123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585(******************************************************************************)(* ASLRef *)(******************************************************************************)(*
* SPDX-FileCopyrightText: Copyright 2022-2023 Arm Limited and/or its affiliates <open-source-office@arm.com>
* SPDX-License-Identifier: BSD-3-Clause
*)(******************************************************************************)(* Disclaimer: *)(* This material covers both ASLv0 (viz, the existing ASL pseudocode language *)(* which appears in the Arm Architecture Reference Manual) and ASLv1, a new, *)(* experimental, and as yet unreleased version of ASL. *)(* This material is work in progress, more precisely at pre-Alpha quality as *)(* per Arm’s quality standards. *)(* In particular, this means that it would be premature to base any *)(* production tool development on this material. *)(* However, any feedback, question, query and feature request would be most *)(* welcome; those can be sent to Arm’s Architecture Formal Team Lead *)(* Jade Alglave <jade.alglave@arm.com>, or by raising issues or PRs to the *)(* herdtools7 github repository. *)(******************************************************************************)openAST(** Error handling for {!Asllib}. *)typeerror_handling_time=Static|Dynamictypeerror_desc=|ReservedIdentifierofstring|BadFieldofstring*ty|MissingFieldofstringlist*ty|BadSlicesoferror_handling_time*slicelist*int|BadSliceofslice|EmptySlice|TypeInferenceNeeded|UndefinedIdentifierofidentifier|MismatchedReturnValueofstring|BadArityoferror_handling_time*identifier*int*int|BadParameterArityoferror_handling_time*version*identifier*int*int|UnsupportedBinopoferror_handling_time*binop*literal*literal|UnsupportedUnopoferror_handling_time*unop*literal|UnsupportedExproferror_handling_time*expr|UnsupportedTyoferror_handling_time*ty|InvalidExprofexpr|MismatchTypeofstring*type_desclist|NotYetImplementedofstring|ObsoleteSyntaxofstring|ConflictingTypesoftype_desclist*ty|AssertionFailedofexpr|CannotParse|UnknownSymbol|NoCallCandidateofstring*tylist|TooManyCallCandidatesofstring*tylist|BadTypesForBinopofbinop*ty*ty|CircularDeclarationsofstring|ImpureExpressionofexpr*SideEffect.SES.t|UnreconciliableTypesofty*ty|AssignToImmutableofstring|AlreadyDeclaredIdentifierofstring|BadReturnStmtoftyoption|UnexpectedSideEffectofstring|UncaughtExceptionofstring|OverlappingSlicesofslicelist*error_handling_time|BadLDIofAST.local_decl_item|BadRecursiveDeclsofidentifierlist|UnrespectedParserInvariant|BadATCofty*ty(** asserting, asserted *)|BadPatternofpattern*ty|ConstrainedIntegerExpectedofty|ParameterWithoutDeclofidentifier|BadParameterDeclofidentifier*identifierlist*identifierlist(** name, expected, actual *)|BaseValueEmptyTypeofty|ArbitraryEmptyTypeofty|BaseValueNonStaticofty*expr|SettingIntersectingSlicesofbitfieldlist|SetterWithoutCorrespondingGetteroffunc|NonReturningFunctionofidentifier|ConflictingSideEffectsofSideEffect.t*SideEffect.t|UnexpectedATC|UnreachableReached|LoopLimitReached|RecursionLimitReached|EmptyConstraints|UnexpectedPendingConstrained|BitfieldsDontAlignof{field1_absname:string;field2_absname:string;field1_absslices:string;field2_absslices:string;}|BadPrintTypeofty|ConfigTimeBrokenofexpr*SideEffect.SES.t|ConstantTimeBrokenofexpr*SideEffect.SES.t|MultipleWritesofidentifier|UnexpectedInitialisationThrowofty*identifier(* Exception type and global storage element name. *)typeerror=error_descannotatedexceptionASLExceptionoferrortype'aresult=('a,error)Result.tletfatale=raise(ASLExceptione)letfatal_frompose=fatal(ASTUtils.add_pos_frompose)letfatal_herepos_startpos_ende=fatal(ASTUtils.annotatedepos_startpos_endASTUtils.default_version)letfatal_unknown_pose=fatal(ASTUtils.add_dummy_annotatione)letinterceptf()=tryOk(f())withASLExceptione->Erroreleterror_handling_time_to_string=function|Static->"Static"|Dynamic->"Dynamic"typewarning_desc=|NoRecursionLimitofidentifierlist|NoLoopLimit|IntervalTooBigToBeExplodedofZ.t*Z.t|ConstraintSetPairToBigToBeExplodedof{op:binop;left:int_constraintlist;right:int_constraintlist;log_max:int;(** Maximum size breached by this constraint set pair. *)}|RemovingValuesFromConstraintsof{op:binop;prev:int_constraintlist;after:int_constraintlist;}|PragmaUseofidentifiertypewarning=warning_descannotatedleterror_label=function|ReservedIdentifier_->"ReservedIdentifier"|BadField_->"BadField"|BadPattern_->"BadPattern"|MissingField_->"MissingField"|BadSlices_->"BadSlices"|BadSlice_->"BadSlice"|EmptySlice->"EmptySlice"|TypeInferenceNeeded->"TypeInferenceNeeded"|UndefinedIdentifier_->"UndefinedIdentifier"|MismatchedReturnValue_->"MismatchedReturnValue"|BadArity_->"BadArity"|BadParameterArity_->"BadParameterArity"|UnsupportedBinop_->"UnsupportedBinop"|UnsupportedUnop_->"UnsupportedUnop"|UnsupportedExpr_->"UnsupportedExpr"|UnsupportedTy_->"UnsupportedTy"|InvalidExpr_->"InvalidExpr"|MismatchType_->"MismatchType"|NotYetImplemented_->"NotYetImplemented"|ObsoleteSyntax_->"ObsoleteSyntax"|ConflictingTypes_->"ConflictingTypes"|AssertionFailed_->"AssertionFailed"|CannotParse->"CannotParse"|UnknownSymbol->"UnknownSymbol"|NoCallCandidate_->"NoCallCandidate"|TooManyCallCandidates_->"TooManyCallCandidates"|BadTypesForBinop_->"BadTypesForBinop"|CircularDeclarations_->"CircularDeclarations"|ImpureExpression_->"ImpureExpression"|UnreconciliableTypes_->"UnreconciliableTypes"|AssignToImmutable_->"AssignToImmutable"|AlreadyDeclaredIdentifier_->"AlreadyDeclaredIdentifier"|BadReturnStmt_->"BadReturnStmt"|UnexpectedSideEffect_->"UnexpectedSideEffect"|UncaughtException_->"UncaughtException"|OverlappingSlices_->"OverlappingSlices"|BadLDI_->"BadLDI"|BadRecursiveDecls_->"BadRecursiveDecls"|UnrespectedParserInvariant->"UnrespectedParserInvariant"|BadATC_->"BadATC"|ConstrainedIntegerExpected_->"ConstrainedIntegerExpected"|ParameterWithoutDecl_->"ParameterWithoutDecl"|BadParameterDecl_->"BadParameterDecl"|BaseValueEmptyType_->"BaseValueEmptyType"|ArbitraryEmptyType_->"ArbitraryEmptyType"|BaseValueNonStatic_->"BaseValueNonStatic"|SettingIntersectingSlices_->"SettingIntersectingSlices"|SetterWithoutCorrespondingGetter_->"SetterWithoutCorrespondingGetter"|NonReturningFunction_->"NonReturningFunction"|UnexpectedATC->"UnexpectedATC"|UnreachableReached->"UnreachableReached"|LoopLimitReached->"LoopLimitReached"|RecursionLimitReached->"RecursionLimitReached"|EmptyConstraints->"EmptyConstraints"|UnexpectedPendingConstrained->"UnexpectedPendingConstrained"|BitfieldsDontAlign_->"BitfieldsDontAlign"|BadPrintType_->"BadPrintType"|ConflictingSideEffects_->"ConflictingSideEffects"|ConfigTimeBroken_->"ConfigTimeBroken"|ConstantTimeBroken_->"ConstantTimeBroken"|MultipleWrites_->"MultipleWrites"|UnexpectedInitialisationThrow_->"UnexpectedInitialisationThrow"letwarning_label=function|NoLoopLimit->"NoLoopLimit"|IntervalTooBigToBeExploded_->"IntervalTooBigToBeExploded"|ConstraintSetPairToBigToBeExploded_->"ConstraintSetPairToBigToBeExploded"|RemovingValuesFromConstraints_->"RemovingValuesFromConstraints"|NoRecursionLimit_->"NoRecursionLimit"|PragmaUse_->"PragmaUse"modulePPrint=structopenFormatopenPPletpp_comma_listpp_eltfli=pp_print_list~pp_sep:(funf()->fprintff",@ ")pp_eltfliletpp_type_descfty=pp_tyf(ASTUtils.add_dummy_annotationty)letpp_error_descfe=pp_open_hovboxf2;(matche.descwith|ReservedIdentifierid->fprintff"ASL Lexical error: %S is a reserved keyword."id|UnsupportedBinop(t,op,v1,v2)->fprintff"ASL %s error: Illegal application of operator %s for values@ %a@ \
and %a."(error_handling_time_to_stringt)(binop_to_stringop)pp_literalv1pp_literalv2|UnsupportedUnop(t,op,v)->fprintff"ASL %s error: Illegal application of operator %s for value@ %a."(error_handling_time_to_stringt)(unop_to_stringop)pp_literalv|UnsupportedExpr(t,e)->fprintff"ASL %s Error: Unsupported expression %a."(error_handling_time_to_stringt)pp_expre|UnsupportedTy(t,ty)->fprintff"ASL %s Error: Unsupported type %a."(error_handling_time_to_stringt)pp_tyty|InvalidExpre->fprintff"ASL Error: invalid expression %a."pp_expre|MismatchType(v,[ty])->fprintff"ASL Execution error: Mismatch type:@ value %s does not belong to \
type %a."vpp_type_descty|MismatchType(v,li)->fprintff"ASL Execution error: Mismatch type:@ value %s@ does not subtype any \
of those types:@ %a"v(pp_comma_listpp_type_desc)li|BadField(s,ty)->fprintff"ASL Error: There is no field '%s'@ on type %a."spp_tyty|MissingField(fields,ty)->fprintff"ASL Error: Fields mismatch for creating a value of type %a@ -- \
Passed fields are:@ %a"pp_tyty(pp_print_list~pp_sep:pp_print_spacepp_print_string)fields|EmptySlice->assert(e.version=V0);pp_print_textf"ASL Static Error: cannot slice with empty slicing operator. This \
might also be due to an incorrect getter/setter invocation."|BadSlices(t,slices,length)->fprintff"ASL %s error: Cannot extract from bitvector of length %d slice %a."(error_handling_time_to_stringt)lengthpp_slice_listslices|BadSliceslice->fprintff"ASL Static error: invalid slice %a."pp_sliceslice|TypeInferenceNeeded->pp_print_textf"ASL Internal error: Interpreter blocked. Type inference needed."|UndefinedIdentifiers->fprintff"ASL Error: Undefined identifier:@ '%s'"s|MismatchedReturnValues->fprintff"ASL Error: Mismatched use of return value from call to '%s'."s|BadArity(t,name,expected,provided)->fprintff"ASL %s Error: Arity error while calling '%s':@ %d arguments \
expected and %d provided."(error_handling_time_to_stringt)nameexpectedprovided|BadParameterArity(t,version,name,expected,provided)->(match(t,version)with|Static,V0->fprintff"ASL %s Error: Could not infer all parameters while calling \
'%s':@ %d parameters expected and %d inferred"(error_handling_time_to_stringt)nameexpectedprovided|_->fprintff"ASL %s Error: Arity error while calling '%s':@ %d parameters \
expected and %d provided"(error_handling_time_to_stringt)nameexpectedprovided)|NotYetImplementeds->pp_print_textf@@"ASL Internal error: Not yet implemented: "^s|ObsoleteSyntaxs->fprintff"%a@ %s"pp_print_text"ASL Grammar error: Obsolete syntax:"s|ConflictingTypes([expected],provided)->fprintff"ASL Typing error:@ a subtype of@ %a@ was expected,@ provided %a."pp_type_descexpectedpp_typrovided|ConflictingTypes(expected,provided)->fprintff"ASL Typing error:@ %a does@ not@ subtype@ any@ of:@ %a."pp_typrovided(pp_comma_listpp_type_desc)expected|AssertionFailede->fprintff"ASL Execution error: Assertion failed:@ %a."pp_expre|CannotParse->pp_print_stringf"ASL Error: Cannot parse."|UnknownSymbol->pp_print_stringf"ASL Error: Unknown symbol."|NoCallCandidate(name,types)->fprintff"ASL Typing error: No subprogram declaration matches the \
invocation:@ %s(%a)."name(pp_comma_listpp_ty)types|TooManyCallCandidates(name,types)->fprintff"ASL Typing error: Too many subprogram declaration match the \
invocation:@ %s(%a)."name(pp_comma_listpp_ty)types|BadTypesForBinop(op,t1,t2)->fprintff"ASL Typing error: Illegal application of operator %s on types@ %a@ \
and %a."(binop_to_stringop)pp_tyt1pp_tyt2|CircularDeclarationsx->fprintff"ASL Evaluation error: circular definition of constants, including \
%S."x|ImpureExpression(e,ses)->fprintff"ASL Typing error:@ a pure expression was expected,@ found %a,@ \
which@ produces@ the@ following@ side-effects:@ %a."pp_expreSideEffect.SES.pp_printses|UnreconciliableTypes(t1,t2)->fprintff"ASL Typing error:@ cannot@ find@ a@ common@ ancestor@ to@ those@ \
two@ types@ %a@ and@ %a."pp_tyt1pp_tyt2|AssignToImmutablex->fprintff"ASL Typing error:@ cannot@ assign@ to@ immutable@ storage@ %S."x|AlreadyDeclaredIdentifierx->fprintff"ASL Typing error:@ cannot@ declare@ already@ declared@ element@ %S."x|BadReturnStmtNone->pp_print_textf"ASL Typing error: cannot return something from a procedure."|UnexpectedSideEffects->fprintff"Unexpected side-effect: %s."s|UncaughtExceptions->fprintff"Uncaught exception: %s."s|OverlappingSlices(slices,t)->fprintff"ASL %s error:@ overlapping slices@ @[%a@]."(error_handling_time_to_stringt)pp_slice_listslices|BadLDIldi->fprintff"Unsupported declaration:@ @[%a@]."pp_local_decl_itemldi|BadRecursiveDeclsdecls->fprintff"ASL Typing error:@ multiple recursive declarations:@ @[%a@]."(pp_comma_list(funf->fprintff"%S"))decls|UnrespectedParserInvariant->fprintff"Parser invariant broke."|ConstrainedIntegerExpectedt->fprintff"ASL Typing error:@ constrained@ integer@ expected,@ provided@ %a."pp_tyt|ParameterWithoutDecls->fprintff"ASL Typing error:@ explicit@ parameter@ %S@ does@ not@ have@ a@ \
corresponding@ defining@ argument."s|BadParameterDecl(name,expected,actual)->fprintff"ASL Typing error:@ incorrect@ parameter@ declaration@ for@ %S,@ \
expected@ @[{%a}@]@ but@ @[{%a}@]@ provided"name(pp_comma_listpp_print_string)expected(pp_comma_listpp_print_string)actual|ArbitraryEmptyTypet->fprintff"ASL Execution error: ARBITRARY of empty type %a."pp_tyt|BaseValueEmptyTypet->fprintff"ASL Typing error: base value of empty type %a."pp_tyt|BaseValueNonStatic(t,e)->fprintff"ASL Typing error:@ base@ value@ of@ type@ %a@ cannot@ be@ \
statically@ determined@ since@ it@ consists@ of@ %a."pp_tytpp_expre|BadATC(t1,t2)->fprintff"ASL Typing error:@ cannot@ perform@ Asserted@ Type@ Conversion@ on@ \
%a@ by@ %a."pp_tyt1pp_tyt2|SettingIntersectingSlicesbitfields->fprintff"ASL Typing error:@ setting@ intersecting@ bitfields@ [%a]."pp_bitfieldsbitfields|SetterWithoutCorrespondingGetterfunc->letret,args=matchfunc.argswith|(_,ret)::args->(ret,List.mapsndargs)|_->assertfalseinfprintff"ASL Typing error:@ setter@ \"%s\"@ does@ not@ have@ a@ \
corresponding@ getter@ of@ signature@ @[@[%a@]@ ->@ %a@]."func.name(pp_comma_listpp_ty)argspp_tyret|UnexpectedATC->pp_print_textf"ASL Typing error: unexpected ATC."|BadPattern(p,t)->fprintff"ASL Typing error:@ Erroneous@ pattern@ %a@ for@ expression@ of@ \
type@ %a."pp_patternppp_tyt|UnreachableReached->pp_print_textf"ASL Dynamic error: Unreachable reached."|NonReturningFunctionname->fprintff"ASL Typing error:@ the@ function %S@ %a."namepp_print_text"may not terminate by returning a value or raising an exception."|RecursionLimitReached->pp_print_textf"ASL Dynamic error: recursion limit reached."|LoopLimitReached->pp_print_textf"ASL Dynamic error: loop limit reached."|ConflictingSideEffects(s1,s2)->fprintff"ASL Typing error: conflicting side effects %a and %a"SideEffect.pp_prints1SideEffect.pp_prints2|ConfigTimeBroken(e,ses)->fprintff"ASL Typing error:@ expected@ config-time@ expression,@ got@ %a,@ \
which@ produces@ the@ following@ side-effects:@ %a."pp_expreSideEffect.SES.pp_printses|ConstantTimeBroken(e,ses)->fprintff"ASL Typing error:@ expected@ constant-time@ expression,@ got@ %a,@ \
which@ produces@ the@ following@ side-effects:@ %a."pp_expreSideEffect.SES.pp_printses|BadReturnStmt(Somet)->fprintff"ASL Typing error:@ cannot@ return@ nothing@ from@ a@ function,@ an@ \
expression@ of@ type@ %a@ is@ expected."pp_tyt|EmptyConstraints->pp_print_textf"ASL Typing error: a well-constrained integer cannot have empty \
constraints."|BadPrintTypet->fprintff"ASL Typing error:@ %a@ %a."pp_print_text"print and println only accept singular types, found"pp_tyt|UnexpectedPendingConstrained->pp_print_textf"ASL Typing error: a pending constrained integer is illegal here."|BitfieldsDontAlign{field1_absname;field2_absname;field1_absslices;field2_absslices}->fprintff"ASL Typing error:@ bitfields `%s` and `%s` are in the same scope \
but define different slices of the containing bitvector type: %s \
and %s, respectively."field1_absnamefield2_absnamefield1_absslicesfield2_absslices|UnexpectedInitialisationThrow(exception_ty,global_storage_element_name)->fprintff"ASL Execution error:@ unexpected@ exception@ %a@ thrown@ during@ \
the@ evaluation@ of@ the@ initialisation@ of@ the global@ storage@ \
element@ %S."pp_tyexception_tyglobal_storage_element_name|MultipleWritesid->fprintff"ASL Typing error:@ multiple@ writes@ to@ %S."id);pp_close_boxf()letpp_warning_descfw=matchw.descwith|NoRecursionLimit[name]->fprintff"@[ASL Warning:@ the recursive function %s%a@]"namepp_print_text" has no recursive limit annotation."|NoRecursionLimitli->fprintff"@[ASL Warning:@ the mutually-recursive functions @[%a@]%a@]"(pp_comma_listpp_print_string)lipp_print_text" have no recursive limit annotation."|NoLoopLimit->fprintff"@[%a@]"pp_print_text"ASL Warning: Loop does not have a limit."|ConstraintSetPairToBigToBeExploded{op;left;right;log_max}->fprintff"@[%a@ %s@ %a%d@ with@ constraints@ %a@ and@ %a.@ %a@]"pp_print_text"Exploding sets for the binary operation"(binop_to_stringop)pp_print_text"could result in a constraint set bigger than 2^"log_maxPP.pp_int_constraintsleftPP.pp_int_constraintsrightpp_print_text"Continuing with the non-expanded constraints."|IntervalTooBigToBeExploded(za,zb)->fprintff"@[Interval too large: @[<h>[ %a .. %a ]@].@ Keeping it as an \
interval.@]"Z.pp_printzaZ.pp_printzb|RemovingValuesFromConstraints{op;prev;after}->fprintff"@[Warning:@ Removing@ some@ values@ that@ would@ fail@ with@ op %s@ \
from@ constraint@ set@ @[<h>{%a}@]@ gave@ @[<h>{%a}@].@ Continuing@ \
with@ this@ constraint@ set.@]"(binop_to_stringop)PP.pp_int_constraintsprevPP.pp_int_constraintsafter|PragmaUseid->fprintff"@[ASL Warning:@ pragma %s%a@]"idpp_print_text" will be ignored."letpp_pos_beginfpos=ifpos.pos_end!=Lexing.dummy_pos&&pos.pos_start!=Lexing.dummy_posthenfprintff"@[<h>%a:@]@ "pp_posposletpp_errorfe=fprintff"@[<v 0>%a%a@]"pp_pos_beginepp_error_desceletpp_warningfe=fprintff"@[<v 0>%a%a@]"pp_pos_beginepp_warning_desceleterror_desc_to_string=asprintf"%a"pp_error_descletdesc_to_string_infpp_desc=asprintf"%a"@@funfe->pp_set_marginf1_000_000_000;pp_descfeleterror_to_string=asprintf"%a"pp_errorendincludePPrintletescapes=letb=Buffer.create(String.lengths)inString.iter(function|'"'->Buffer.add_charb'"';Buffer.add_charb'"'|c->Buffer.add_charbc)s;Buffer.contentsbletpp_csvpp_desclabel=letpos_in_linepos=Lexing.(pos.pos_cnum-pos.pos_bol)infunfpos->Printf.fprintff"\"%s\",%d,%d,%d,%d,%s,\"%s\""(escapepos.pos_start.pos_fname)pos.pos_start.pos_lnum(pos_in_linepos.pos_start)pos.pos_end.pos_lnum(pos_in_linepos.pos_end)(labelpos.desc)(desc_to_string_infpp_descpos|>escape)letpp_error_csvfe=pp_csvpp_error_descerror_labelfeletpp_warning_csvfw=pp_csvpp_warning_descwarning_labelfwtypeoutput_format=HumanReadable|CSVmoduletypeERROR_PRINTER_CONFIG=sigvaloutput_format:output_formatendmoduleErrorPrinter(C:ERROR_PRINTER_CONFIG)=structleteprintlne=matchC.output_formatwith|HumanReadable->Format.eprintf"@[<2>%a@]@."pp_errore|CSV->Printf.eprintf"%a\n"pp_error_csveletwarnw=matchC.output_formatwith|HumanReadable->Format.eprintf"@[<2>%a@]@."pp_warningw|CSV->Printf.eprintf"%a\n"pp_warning_csvwletwarn_from~locw=ASTUtils.add_pos_fromlocw|>warnendlet()=Printexc.register_printer@@function|ASLExceptione->Some(error_to_stringe)|_->None