Skip to content

Commit

Permalink
Proof gen for other types of sequenceof
Browse files Browse the repository at this point in the history
  • Loading branch information
@mario-bucev
mario-bucev committed Apr 13, 2024
1 parent de95a62 commit b6f7ab4
Show file tree
Hide file tree
Showing 19 changed files with 585 additions and 230 deletions.
116 changes: 80 additions & 36 deletions BackendAst/DAstACN.fs
View file

Large diffs are not rendered by default.

226 changes: 167 additions & 59 deletions BackendAst/DAstUPer.fs
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion BackendAst/DAstUtilFunctions.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -937,7 +937,7 @@ let hasUperEncodeFunction (encFunc : UPerFunction option) =
| None -> false
| Some fnc ->
let p = {CallerScope.modName = ""; arg = Selection.valueEmptyPath "dummy"}
match fnc.funcBody p with
match fnc.funcBody (NestingScope.init 0I 0I) p with
| None -> false
| Some _ -> true

Expand Down
10 changes: 5 additions & 5 deletions CommonTypes/AbstractMacros.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -325,17 +325,17 @@ Generated by the C stg macros with the following command
abstract member Enumerated_item : p:string -> sName:string -> nIndex:BigInteger -> nLastItemIndex:BigInteger -> codec:Codec -> string;
abstract member Enumerated : p:string -> td:FE_EnumeratedTypeDefinition -> arrsItem:seq<string> -> nMin:BigInteger -> nMax:BigInteger -> nBits:BigInteger -> sErrCode:string -> nLastItemIndex:BigInteger -> sFirstItemName:string -> codec:Codec -> string;
abstract member choice_child : p:string -> sAcc:string -> sChildID:string -> nChildIndex:BigInteger -> nIndexSizeInBits:BigInteger -> nLastItemIndex:BigInteger -> sChildContent:string -> sChildName:string -> sChildTypeDef:string -> sChoiceTypeName:string -> sChildInitExpr:string -> bIsSequence:bool -> bIsEnum:bool -> codec:Codec -> string;
abstract member choice : p:string -> sAcc:string -> arrsChildren:seq<string> -> nLastItemIndex:BigInteger -> sChoiceIndexName:string -> sErrCode:string -> td:FE_ChoiceTypeDefinition -> nIndexSizeInBits:BigInteger -> codec:Codec -> string;
abstract member choice : p:string -> sAcc:string -> arrsChildren:seq<string> -> nLastItemIndex:BigInteger -> sChoiceIndexName:string -> sErrCode:string -> td:FE_ChoiceTypeDefinition -> nIndexSizeInBits:BigInteger -> bIntroSnap:bool -> codec:Codec -> string;
abstract member sequence_presence_bit : p:string -> sAcc:string -> sChName:string -> soExistVar:string option -> sErrCode:string -> codec:Codec -> string;
abstract member sequence_presence_bit_fix : p:string -> sAcc:string -> sChName:string -> soExistVar:string option -> sErrCode:string -> sVal:string -> codec:Codec -> string;
abstract member sequence_mandatory_child : sChName:string -> sChildContent:string -> codec:Codec -> string;
abstract member sequence_optional_child : p:string -> sAcc:string -> sChName:string -> sChildContent:string -> soExistVar:string option -> soChildExpr:string option -> sChildTypedef:string -> codec:Codec -> string;
abstract member sequence_default_child : p:string -> sAcc:string -> sChName:string -> sChildContent:string -> soExistVar:string option -> soChildExpr:string option -> sChildTypedef:string -> sInitWithDefaultValue:string -> codec:Codec -> string;
abstract member sequence_build : p:string -> sTypeDefName:string -> arrsChildren:seq<string> -> string;
abstract member str_FixedSize : p:string -> sTasName:string -> i:string -> sInternalItem:string -> nFixedSize:BigInteger -> nIntItemMinSize:BigInteger -> nIntItemMaxSize:BigInteger -> nAlignSize:BigInteger -> soInitExpr:string option -> codec:Codec -> string;
abstract member str_FixedSize : p:string -> sTasName:string -> i:string -> sInternalItem:string -> nFixedSize:BigInteger -> nIntItemMinSize:BigInteger -> nIntItemMaxSize:BigInteger -> nAlignSize:BigInteger -> soInitExpr:string option -> bIntroSnap:bool -> soPreSerde:string option -> soPostSerde:string option -> soPostInc:string option -> soInvariant:string option -> codec:Codec -> string;
abstract member str_VarSize : p:string -> sTasName:string -> i:string -> sInternalItem:string -> nSizeMin:BigInteger -> nSizeMax:BigInteger -> nSizeInBits:BigInteger -> nIntItemMinSize:BigInteger -> nIntItemMaxSize:BigInteger -> nAlignSize:BigInteger -> soInitExpr:string option -> codec:Codec -> string;
abstract member seqOf_FixedSize : p:string -> sTasName:string -> i:string -> sInternalItem:string -> nFixedSize:BigInteger -> nIntItemMinSize:BigInteger -> nIntItemMaxSize:BigInteger -> nAlignSize:BigInteger -> sChildInitExpr:string -> codec:Codec -> string;
abstract member seqOf_VarSize : p:string -> sAcc:string -> sTasName:string -> i:string -> sInternalItem:string -> nSizeMin:BigInteger -> nSizeMax:BigInteger -> nSizeInBits:BigInteger -> nIntItemMinSize:BigInteger -> nIntItemMaxSize:BigInteger -> nAlignSize:BigInteger -> sChildInitExpr:string -> sErrCode:string -> soPreSerde:string option -> soPostSerde:string option -> soPostInc:string option -> soInvariant:string option -> codec:Codec -> string;
abstract member seqOf_VarSize : p:string -> sAcc:string -> sTasName:string -> i:string -> sInternalItem:string -> nSizeMin:BigInteger -> nSizeMax:BigInteger -> nSizeInBits:BigInteger -> nIntItemMinSize:BigInteger -> nIntItemMaxSize:BigInteger -> nAlignSize:BigInteger -> sChildInitExpr:string -> sErrCode:string -> nAbsOffset:BigInteger -> nRemainingMinBits:BigInteger -> nLevel:BigInteger -> nIx:BigInteger -> nOffset:BigInteger -> bIntroSnap:bool -> soPreSerde:string option -> soPostSerde:string option -> soPostInc:string option -> soInvariant:string option -> codec:Codec -> string;
abstract member octet_FixedSize : sTypeDefName:string -> p:string -> sAcc:string -> nFixedSize:BigInteger -> codec:Codec -> string;
abstract member octet_VarSize : sTypeDefName:string -> p:string -> sAcc:string -> nSizeMin:BigInteger -> nSizeMax:BigInteger -> nSizeInBits:BigInteger -> sErrCode:string -> codec:Codec -> string;
abstract member bitString_FixSize : sTypeDefName:string -> p:string -> sAcc:string -> nFixedSize:BigInteger -> sErrCode:string -> codec:Codec -> string;
Expand Down Expand Up @@ -411,8 +411,8 @@ Generated by the C stg macros with the following command
abstract member Acn_IA5String_CharIndex_External_Field_Determinant : p:string -> sErrCode:string -> nAsn1Max:BigInteger -> sExtFld:string -> td:FE_StringTypeDefinition -> nCharSize:BigInteger -> nRemainingBits:BigInteger -> codec:Codec -> string;
abstract member oct_external_field : sTypedefName:string -> p:string -> sAcc:string -> noSizeMin:BigInteger option -> nSizeMax:BigInteger -> sExtFld:string -> bIsUnsigned:bool -> nAlignSize:BigInteger -> sErrCode:string -> codec:Codec -> string;
abstract member oct_external_field_fix_size : sTypedefName:string -> p:string -> sAcc:string -> noSizeMin:BigInteger option -> nSizeMax:BigInteger -> sExtFld:string -> bIsUnsigned:bool -> nAlignSize:BigInteger -> sErrCode:string -> codec:Codec -> string;
abstract member sqf_external_field : sTypeDefName:string -> p:string -> sAcc:string -> i:string -> sInternalItem:string -> noSizeMin:BigInteger option -> nSizeMax:BigInteger -> sExtFld:string -> bIsUnsigned:bool -> nAlignSize:BigInteger -> sErrCode:string -> nIntItemMinSize:BigInteger -> nIntItemMaxSize:BigInteger -> sChildInitExpr:string -> soPreSerde:string option -> soPostSerde:string option -> soPostInc:string option -> soInvariant:string option -> codec:Codec -> string;
abstract member sqf_external_field_fix_size : sTypeDefName:string -> p:string -> sAcc:string -> i:string -> sInternalItem:string -> noSizeMin:BigInteger option -> nSizeMax:BigInteger -> sExtFld:string -> bIsUnsigned:bool -> nAlignSize:BigInteger -> sErrCode:string -> nIntItemMinSize:BigInteger -> nIntItemMaxSize:BigInteger -> sChildInitExpr:string -> soPreSerde:string option -> soPostSerde:string option -> soPostInc:string option -> soInvariant:string option -> codec:Codec -> string;
abstract member sqf_external_field : sTypeDefName:string -> p:string -> sAcc:string -> i:string -> sInternalItem:string -> noSizeMin:BigInteger option -> nSizeMax:BigInteger -> sExtFld:string -> bIsUnsigned:bool -> nAlignSize:BigInteger -> sErrCode:string -> nIntItemMinSize:BigInteger -> nIntItemMaxSize:BigInteger -> sChildInitExpr:string -> bIntroSnap:bool -> soPreSerde:string option -> soPostSerde:string option -> soPostInc:string option -> soInvariant:string option -> codec:Codec -> string;
abstract member sqf_external_field_fix_size : sTypeDefName:string -> p:string -> sAcc:string -> i:string -> sInternalItem:string -> noSizeMin:BigInteger option -> nSizeMax:BigInteger -> sExtFld:string -> bIsUnsigned:bool -> nAlignSize:BigInteger -> sErrCode:string -> nIntItemMinSize:BigInteger -> nIntItemMaxSize:BigInteger -> sChildInitExpr:string -> bIntroSnap:bool -> soPreSerde:string option -> soPostSerde:string option -> soPostInc:string option -> soInvariant:string option -> codec:Codec -> string;
abstract member oct_sqf_null_terminated : p:string -> sAcc:string -> i:string -> sInternalItem:string -> noSizeMin:BigInteger option -> nSizeMax:BigInteger -> arruNullBytes:seq<byte> -> nBitPatternLength:BigInteger -> sErrCode:string -> nIntItemMinSize:BigInteger -> nIntItemMaxSize:BigInteger -> codec:Codec -> string;
abstract member bit_string_external_field : sTypeDefName:string -> p:string -> sErrCode:string -> sAcc:string -> noSizeMin:BigInteger option -> nSizeMax:BigInteger -> sExtFld:string -> codec:Codec -> string;
abstract member bit_string_external_field_fixed_size : sTypeDefName:string -> p:string -> sErrCode:string -> sAcc:string -> noSizeMin:BigInteger option -> nSizeMax:BigInteger -> sExtFld:string -> codec:Codec -> string;
Expand Down
18 changes: 9 additions & 9 deletions FrontEndAst/AcnCreateFromAntlr.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -307,7 +307,7 @@ let private mergeReal (asn1: Asn1Ast.AstRoot) (loc: SrcLoc) (acnErrLoc: SrcLoc o
let private mergeObjectIdentifier (asn1: Asn1Ast.AstRoot) (relativeId: bool) (loc: SrcLoc) (acnErrLoc: SrcLoc option) (props: GenericAcnProperty list) cons withcons (tdarg: GetTypeDefinition_arg) (us: Asn1AcnMergeState) =
let acnErrLoc0 = match acnErrLoc with Some a -> a | None -> loc
let getRtlTypeName (l:ProgrammingLanguage) = (asn1.args.getBasicLang l).getObjectIdentifierRtlTypeName relativeId

//check for invalid properties
props |> Seq.iter(fun pr -> raise(SemanticError(acnErrLoc0, "Acn property cannot be applied to OBJECT IDENTIFIER types")))

Expand Down Expand Up @@ -423,9 +423,9 @@ let private mergeStringType (asn1: Asn1Ast.AstRoot) (t: Asn1Ast.Asn1Type option)
(l,itm), ns) us
lanDefs |> Map.ofList, us1

{StringType.acnProperties = acnProperties; cons = cons; withcons = withcons; minSize=minSize; maxSize =maxSize;
uperMaxSizeInBits = uperMaxSizeInBits; uperMinSizeInBits=uperMinSizeInBits; uperCharSet=uperCharSet;
acnEncodingClass = acnEncodingClass; acnMinSizeInBits=acnMinSizeInBits;
{StringType.acnProperties = acnProperties; cons = cons; withcons = withcons; minSize=minSize; maxSize =maxSize;
uperMaxSizeInBits = uperMaxSizeInBits; uperMinSizeInBits=uperMinSizeInBits; uperCharSet=uperCharSet;
acnEncodingClass = acnEncodingClass; acnMinSizeInBits=acnMinSizeInBits;
acnMaxSizeInBits = acnMaxSizeInBits;isNumeric=isNumeric; typeDef=typeDef}, us1

let private mergeOctetStringType (asn1: Asn1Ast.AstRoot) (loc: SrcLoc) (acnErrLoc: SrcLoc option) (props: GenericAcnProperty list) cons withcons (tdarg: GetTypeDefinition_arg) (us: Asn1AcnMergeState) =
Expand Down Expand Up @@ -542,7 +542,7 @@ let private mergeBooleanType (args: CommandLineSettings) (acnErrLoc: SrcLoc opti
{Boolean.acnProperties = acnProperties; cons = cons; withcons = withcons;uperMaxSizeInBits = 1I; uperMinSizeInBits=1I;
acnMinSizeInBits=acnMinSizeInBits; acnMaxSizeInBits = acnMaxSizeInBits; typeDef=typeDef; defaultInitVal="false"}, us1

let private mergeEnumerated (asn1: Asn1Ast.AstRoot) (items: Asn1Ast.NamedItem list) (originalLocation: SrcLoc option, loc: SrcLoc)
let private mergeEnumerated (asn1: Asn1Ast.AstRoot) (items: Asn1Ast.NamedItem list) (originalLocation: SrcLoc option, loc: SrcLoc)
(acnErrLoc: SrcLoc option) (acnType: AcnTypeEncodingSpec option) (props: GenericAcnProperty list) cons withcons (tdarg: EnmStrGetTypeDefinition_arg) (us: Asn1AcnMergeState) =
let loc =
match originalLocation with
Expand Down Expand Up @@ -775,8 +775,8 @@ let rec private mapAcnParamTypeToAcnAcnInsertedType (asn1:Asn1Ast.AstRoot) (acn:
let checkIntHasEnoughSpace asn1Min asn1Max =
checkIntHasEnoughSpace acnEncodingClass acnProperties.mappingFunction.IsSome acnErrLoc asn1Min asn1Max
let intClass = getIntEncodingClassByUperRange asn1.args uperRange
AcnInteger ({AcnInteger.acnProperties=acnProperties; acnAlignment=acnAlignment; acnEncodingClass = acnEncodingClass;
Location = acnErrLoc; acnMinSizeInBits=acnMinSizeInBits; acnMaxSizeInBits = acnMaxSizeInBits; cons=[]; withcons=[];isUnsigned=isUnsigned;
AcnInteger ({AcnInteger.acnProperties=acnProperties; acnAlignment=acnAlignment; acnEncodingClass = acnEncodingClass;
Location = acnErrLoc; acnMinSizeInBits=acnMinSizeInBits; acnMaxSizeInBits = acnMaxSizeInBits; cons=[]; withcons=[];isUnsigned=isUnsigned;
uperRange= uperRange; intClass=intClass; checkIntHasEnoughSpace=checkIntHasEnoughSpace; inheritInfo=None; defaultValue="0"}), us

| AcnPrmBoolean acnErrLoc ->
Expand Down Expand Up @@ -1041,7 +1041,7 @@ let rec private mergeType (asn1:Asn1Ast.AstRoot) (acn:AcnAst) (m:Asn1Ast.Asn1Mo

let newKind = {SequenceOf.child=newChType; acnProperties = acnProperties; cons = cons; withcons = wcons;minSize=minSize; maxSize =maxSize; uperMaxSizeInBits = uperMaxSizeInBits; uperMinSizeInBits=uperMinSizeInBits; acnEncodingClass = acnEncodingClass; acnMinSizeInBits = acnMinSizeInBits; acnMaxSizeInBits=acnMaxSizeInBits; typeDef=typeDef}
SequenceOf newKind, us2
| Asn1Ast.Sequence children ->
| Asn1Ast.Sequence children ->
let childrenNameConstraints = allCons |> List.choose(fun c -> match c with Asn1Ast.WithComponentsConstraint (_,w) -> Some w| _ -> None) |> List.collect id
let myVisibleConstraints = refTypeCons@t.Constraints //|> List.choose(fun c -> match c with Asn1Ast.WithComponentsConstraint _ -> None | _ -> Some c)
let myNonVisibleConstraints = withCons //|> List.choose(fun c -> match c with Asn1Ast.WithComponentsConstraint _ -> None | _ -> Some c)
Expand Down Expand Up @@ -1133,7 +1133,7 @@ let rec private mergeType (asn1:Asn1Ast.AstRoot) (acn:AcnAst) (m:Asn1Ast.Asn1Mo
| Some AlwaysAbsent
| Some (Optional _)
| Some AlwaysPresent -> true

match cc with
| None ->
let newChild, us1 = mergeType asn1 acn m c.Type (curPath@[SEQ_CHILD (c.Name.Value, isOptional)]) (typeDefPath@[SEQ_CHILD (c.Name.Value, isOptional)]) (enmItemTypeDefPath@[SEQ_CHILD (c.Name.Value, isOptional)]) None None [] childWithCons [] [] None None us
Expand Down
8 changes: 8 additions & 0 deletions FrontEndAst/Asn1AcnAst.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -351,6 +351,14 @@ type StringAcnEncodingClass =
| Acn_Enc_String_Ascii_Null_Terminated of BigInteger*(byte list) //char size in bits, byte = the null character
| Acn_Enc_String_Ascii_External_Field_Determinant of BigInteger*RelativePath //char size in bits, encode ascii, size is provided by an external length determinant
| Acn_Enc_String_CharIndex_External_Field_Determinant of BigInteger*RelativePath //char size in bits, encode char index, size is provided by an external length determinant
with
member this.charSizeInBits: bigint =
match this with
| Acn_Enc_String_uPER c
| Acn_Enc_String_uPER_Ascii c
| Acn_Enc_String_Ascii_Null_Terminated (c, _)
| Acn_Enc_String_Ascii_External_Field_Determinant (c, _)
| Acn_Enc_String_CharIndex_External_Field_Determinant (c, _) -> c

type SizeableAcnEncodingClass =
//| SZ_EC_uPER
Expand Down
35 changes: 18 additions & 17 deletions FrontEndAst/DAst.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -382,6 +382,22 @@ type TypeEncodingKind =
/////////////////////////////////////////////////////////////////////


type NestingScope = {
acnOuterMaxSize: bigint
uperOuterMaxSize: bigint
nestingLevel: int
nestingIx: int
acnOffset: bigint
uperOffset: bigint
acnRelativeOffset: bigint
uperRelativeOffset: bigint
acnSiblingMaxSize: bigint option
uperSiblingMaxSize: bigint option
} with
static member init (acnOuterMaxSize: bigint) (uperOuterMaxSize: bigint): NestingScope =
{acnOuterMaxSize = acnOuterMaxSize; uperOuterMaxSize = uperOuterMaxSize; nestingLevel = 0; nestingIx = 0; acnRelativeOffset = 0I; uperRelativeOffset = 0I; acnOffset = 0I; uperOffset = 0I; acnSiblingMaxSize = None; uperSiblingMaxSize = None}


type UPERFuncBodyResult = {
funcBody : string
errCodes : ErrorCode list
Expand All @@ -395,8 +411,8 @@ type UPerFunction = {
funcName : string option // the name of the function
func : string option // the body of the function
funcDef : string option // function definition in header file
funcBody : CallerScope -> (UPERFuncBodyResult option) // returns a list of validations statements
funcBody_e : ErrorCode -> CallerScope -> (UPERFuncBodyResult option)
funcBody : NestingScope -> CallerScope -> (UPERFuncBodyResult option) // returns a list of validations statements
funcBody_e : ErrorCode -> NestingScope -> CallerScope -> (UPERFuncBodyResult option)
}

type AcnFuncBodyResult = {
Expand Down Expand Up @@ -439,21 +455,6 @@ type IcdAux = {
typeAss : IcdTypeAss
}

type NestingScope = {
acnOuterMaxSize: bigint
uperOuterMaxSize: bigint
nestingLevel: int
nestingIx: int
acnOffset: bigint
uperOffset: bigint
acnRelativeOffset: bigint
uperRelativeOffset: bigint
acnSiblingMaxSize: bigint option
uperSiblingMaxSize: bigint option
} with
static member init (acnOuterMaxSize: bigint) (uperOuterMaxSize: bigint): NestingScope =
{acnOuterMaxSize = acnOuterMaxSize; uperOuterMaxSize = uperOuterMaxSize; nestingLevel = 0; nestingIx = 0; acnRelativeOffset = 0I; uperRelativeOffset = 0I; acnOffset = 0I; uperOffset = 0I; acnSiblingMaxSize = None; uperSiblingMaxSize = None}

type AcnFunction = {
funcName : string option // the name of the function. Valid only for TASes)
func : string option // the body of the function
Expand Down
Loading

0 comments on commit b6f7ab4

Please sign in to comment.