From b90cc19a1dd0313b8b8af228fd9deac826e8d1e2 Mon Sep 17 00:00:00 2001 From: George Mamais Date: Mon, 6 Jan 2025 12:37:53 +0200 Subject: [PATCH] calculate maxAlignment --- FrontEndAst/AcnCreateFromAntlr.fs | 37 +++++++++++++++++++++---------- FrontEndAst/Asn1AcnAst.fs | 13 +++++++++++ FrontEndAst/DAstTypeDefinition.fs | 12 +++++----- FrontEndAst/Language.fs | 12 +++++----- StgScala/LangGeneric_scala.fs | 12 +++++----- StgScala/ProofGen.fs | 33 +++++++++++++-------------- 6 files changed, 71 insertions(+), 48 deletions(-) diff --git a/FrontEndAst/AcnCreateFromAntlr.fs b/FrontEndAst/AcnCreateFromAntlr.fs index 0a74d211..b415fcba 100644 --- a/FrontEndAst/AcnCreateFromAntlr.fs +++ b/FrontEndAst/AcnCreateFromAntlr.fs @@ -1027,12 +1027,17 @@ let rec private mergeType (asn1:Asn1Ast.AstRoot) (acn:AcnAst) (typeIdsSet : Map (inheritInfo : InheritanceInfo option) (typeAssignmentInfo : AssignmentInfo option) (us:Asn1AcnMergeState) : (Asn1Type*Asn1AcnMergeState)= + + let maxAlignmentOf (aligns: AcnAlignment option list): AcnAlignment option = + aligns |> List.maxBy (fun a -> a |> Option.map (fun a -> a.nbBits) |> Option.defaultValue 0I) + let acnProps = match acnType with | None -> [] | Some x -> x.acnProperties let acnErrLoc = acnType |> Option.map(fun x -> x.loc) let combinedProperties = acnProps + let alignment = tryGetProp combinedProperties (fun x -> match x with ALIGNTONEXT e -> Some e | _ -> None) let allCons = t.Constraints@refTypeCons@withCons let debug = ReferenceToType curPath //if debug.AsString.EndsWith "ALPHA-DELETE-DIAGNOSTIC-PARAMETER-REPORT-STRUCTURES-GENERIC" then @@ -1147,14 +1152,15 @@ let rec private mergeType (asn1:Asn1Ast.AstRoot) (acn:AcnAst) (typeIdsSet : Map let uperMinSizeInBits, _ = uPER.getSizeableTypeSize minSize.uper maxSize.uper newChType.uperMinSizeInBits let _, uperMaxSizeInBits = uPER.getSizeableTypeSize minSize.uper maxSize.uper newChType.uperMaxSizeInBits - let alignment = tryGetProp combinedProperties (fun x -> match x with ALIGNTONEXT e -> Some e | _ -> None) let acnEncodingClass, acnMinSizeInBits, acnMaxSizeInBits= AcnEncodingClasses.GetSequenceOfEncodingClass alignment loc acnProperties uperMinSizeInBits uperMaxSizeInBits minSize.acn maxSize.acn newChType.acnMinSizeInBits newChType.acnMaxSizeInBits hasNCount // (acnAlignment : AcnGenericTypes.AcnAlignment option) (child : Asn1AcnAst.Asn1Type) (childType: DAst.Asn1Type) + let maxAlignment = maxAlignmentOf [alignment; newChType.maxAlignment] + let definitionOrRef = lms |> List.map(fun (l,lm) -> - (l, DAstTypeDefinition.createSequenceOf_u lm (ReferenceToType curPath) typeDef acnMinSizeInBits acnMaxSizeInBits minSize maxSize acnEncodingClass alignment newChType)) |> Map.ofList + (l, DAstTypeDefinition.createSequenceOf_u lm (ReferenceToType curPath) typeDef acnMinSizeInBits acnMaxSizeInBits minSize maxSize acnEncodingClass alignment maxAlignment newChType)) |> Map.ofList - 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; acnArgs=acnArgsSubsted; typeDef=typeDef; definitionOrRef=definitionOrRef} + 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; acnArgs=acnArgsSubsted; typeDef=typeDef; definitionOrRef=definitionOrRef; maxAlignment=maxAlignment} SequenceOf newKind, us2 | Asn1Ast.Sequence children -> let childrenNameConstraints = allCons |> List.choose(fun c -> match c with Asn1Ast.WithComponentsConstraint (_,w) -> Some w| _ -> None) |> List.collect id @@ -1326,13 +1332,16 @@ let rec private mergeType (asn1:Asn1Ast.AstRoot) (acn:AcnAst) (typeIdsSet : Map } let acnArgsSubsted = substAcnArgs acnParamSubst acnArgs - // (acnProperties : AcnGenericTypes.SequenceAcnProperties) (acnMaxSizeInBits : BigInteger) (children:SeqChildInfo list) = + + let childrenAlignemts = mergedChildren |> List.map(fun c -> match c with Asn1Child c -> c.Type.maxAlignment | AcnChild c -> c.Type.acnAlignment) + let maxAlignment = maxAlignmentOf (alignment::childrenAlignemts) + let definitionOrRef = lms |> List.map(fun (l,lm) -> let acnAlignment = tryGetProp combinedProperties (fun x -> match x with ALIGNTONEXT e -> Some e | _ -> None) - (l, DAstTypeDefinition.createSequence_u asn1.args lm typeDef (ReferenceToType curPath) acnAlignment acnProperties acnMinSizeInBits acnMaxSizeInBits mergedChildren)) |> Map.ofList + (l, DAstTypeDefinition.createSequence_u asn1.args lm typeDef (ReferenceToType curPath) acnAlignment maxAlignment acnProperties acnMinSizeInBits acnMaxSizeInBits mergedChildren)) |> Map.ofList - Sequence ({Sequence.children = mergedChildren; acnProperties=acnProperties; cons=cons; withcons = wcons;uperMaxSizeInBits=uperBitMaskSize+uperMaxChildrenSize; uperMinSizeInBits=uperBitMaskSize+uperMinChildrenSize;acnMaxSizeInBits=acnMaxSizeInBits;acnMinSizeInBits=acnMinSizeInBits; acnArgs=acnArgsSubsted; typeDef=typeDef; definitionOrRef=definitionOrRef}), chus + Sequence ({Sequence.children = mergedChildren; acnProperties=acnProperties; cons=cons; withcons = wcons;uperMaxSizeInBits=uperBitMaskSize+uperMaxChildrenSize; uperMinSizeInBits=uperBitMaskSize+uperMinChildrenSize;acnMaxSizeInBits=acnMaxSizeInBits;acnMinSizeInBits=acnMinSizeInBits; acnArgs=acnArgsSubsted; typeDef=typeDef; definitionOrRef=definitionOrRef; maxAlignment=maxAlignment}), chus | Asn1Ast.Choice children -> let childrenNameConstraints = t.Constraints@refTypeCons |> List.choose(fun c -> match c with Asn1Ast.WithComponentsConstraint (_,w) -> Some w| _ -> None) |> List.collect id let myVisibleConstraints = t.Constraints@refTypeCons @@ -1447,7 +1456,6 @@ let rec private mergeType (asn1:Asn1Ast.AstRoot) (acn:AcnAst) (typeIdsSet : Map let minChildSize = mergedChildren |> List.map(fun x -> x.Type.uperMinSizeInBits) |> Seq.min let maxChildSize = mergedChildren |> List.map(fun x -> x.Type.uperMaxSizeInBits) |> Seq.max - let alignment = tryGetProp combinedProperties (fun x -> match x with ALIGNTONEXT e -> Some e | _ -> None) let acnMinSizeInBits, acnMaxSizeInBits = AcnEncodingClasses.GetChoiceEncodingClass mergedChildren alignment t.Location acnProperties // TODO: Voir si cela ne prove pas de dup? + SequenceOf // let detArg = acnType |> Option.bind (fun acnType -> acnType.acnProperties |> List.tryFindMap (fun prop -> @@ -1456,15 +1464,18 @@ let rec private mergeType (asn1:Asn1Ast.AstRoot) (acn:AcnAst) (typeIdsSet : Map // | _ -> None)) // let detArgSubsted = detArg |> Option.map (fun detArg -> substAcnArg acnParamSubst detArg) let allAcnArgsSubsted = substAcnArgs acnParamSubst acnArgs - // let allAcnArgsSubsted = acnArgsSubsted @ (detArgSubsted |> Option.toList) + + let childrenAlignemts = mergedChildren |> List.map(fun c -> c.Type.maxAlignment) + let maxAlignment = maxAlignmentOf (alignment::childrenAlignemts) + let definitionOrRef = lms |> List.map(fun (l,lm) -> let acnAlignment = tryGetProp combinedProperties (fun x -> match x with ALIGNTONEXT e -> Some e | _ -> None) - (l, DAstTypeDefinition.createChoice_u asn1.args typeIdsSet lm typeDef (ReferenceToType curPath) acnProperties acnAlignment acnMinSizeInBits acnMaxSizeInBits mergedChildren)) |> Map.ofList + (l, DAstTypeDefinition.createChoice_u asn1.args typeIdsSet lm typeDef (ReferenceToType curPath) acnProperties acnAlignment maxAlignment acnMinSizeInBits acnMaxSizeInBits mergedChildren)) |> Map.ofList Choice ({Choice.children = mergedChildren; acnProperties = acnProperties; cons=cons; withcons = wcons; uperMaxSizeInBits=indexSize+maxChildSize; uperMinSizeInBits=indexSize+minChildSize; acnMinSizeInBits =acnMinSizeInBits; - acnMaxSizeInBits=acnMaxSizeInBits; acnParameters = acnParameters; acnArgs = allAcnArgsSubsted; acnLoc = acnLoc; typeDef=typeDef; definitionOrRef=definitionOrRef}), chus + acnMaxSizeInBits=acnMaxSizeInBits; acnParameters = acnParameters; acnArgs = allAcnArgsSubsted; acnLoc = acnLoc; typeDef=typeDef; definitionOrRef=definitionOrRef; maxAlignment=maxAlignment}), chus | Asn1Ast.ReferenceType rf -> let acnArguments = acnArgs @@ -1522,7 +1533,6 @@ let rec private mergeType (asn1:Asn1Ast.AstRoot) (acn:AcnAst) (typeIdsSet : Map let toByte sizeInBits = sizeInBits/8I + (if sizeInBits % 8I = 0I then 0I else 1I) - let alignment = tryGetProp combinedProperties (fun x -> match x with ALIGNTONEXT e -> Some e | _ -> None) let uperMinSizeInBits, uperMaxSizeInBits, acnMinSizeInBits, acnMaxSizeInBits, encodingOptions = match rf.refEnc with @@ -1555,8 +1565,11 @@ let rec private mergeType (asn1:Asn1Ast.AstRoot) (acn:AcnAst) (typeIdsSet : Map let acnEncodingClass, acnMinSizeInBits, acnMaxSizeInBits= AcnEncodingClasses.GetOctetStringEncodingClass alignment loc acnProperties uperMinSizeInBits uperMaxSizeInBits minSize.acn maxSize.acn hasNCount uperMinSizeInBits, uperMaxSizeInBits, acnMinSizeInBits, acnMaxSizeInBits, (Some {EncodeWithinOctetOrBitStringProperties.acnEncodingClass = acnEncodingClass; octOrBitStr = ContainedInOctString; minSize = minSize; maxSize=maxSize}) + + let maxAlignment = maxAlignmentOf [alignment; resolvedType.maxAlignment] + let definitionOrRef = resolvedType.typeDefinitionOrReference - let newRef = {ReferenceType.modName = rf.modName; tasName = rf.tasName; tabularized = rf.tabularized; acnArguments = acnArguments; resolvedType=resolvedType; hasConstraints = hasAdditionalConstraints; typeDef=typeDef; uperMaxSizeInBits = uperMaxSizeInBits; uperMinSizeInBits = uperMinSizeInBits; acnMaxSizeInBits = acnMaxSizeInBits; acnMinSizeInBits = acnMinSizeInBits; encodingOptions=encodingOptions; hasExtraConstrainsOrChildrenOrAcnArgs=hasExtraConstrainsOrChildrenOrAcnArgs; refCons = refCons;definitionOrRef=definitionOrRef} + let newRef = {ReferenceType.modName = rf.modName; tasName = rf.tasName; tabularized = rf.tabularized; acnArguments = acnArguments; resolvedType=resolvedType; hasConstraints = hasAdditionalConstraints; typeDef=typeDef; uperMaxSizeInBits = uperMaxSizeInBits; uperMinSizeInBits = uperMinSizeInBits; acnMaxSizeInBits = acnMaxSizeInBits; acnMinSizeInBits = acnMinSizeInBits; encodingOptions=encodingOptions; hasExtraConstrainsOrChildrenOrAcnArgs=hasExtraConstrainsOrChildrenOrAcnArgs; refCons = refCons;definitionOrRef=definitionOrRef; maxAlignment=maxAlignment} ReferenceType newRef, us2 { diff --git a/FrontEndAst/Asn1AcnAst.fs b/FrontEndAst/Asn1AcnAst.fs index ab7820d1..7c297f65 100644 --- a/FrontEndAst/Asn1AcnAst.fs +++ b/FrontEndAst/Asn1AcnAst.fs @@ -699,6 +699,15 @@ type Asn1Type = { | OctetString os -> os.acnArgs | BitString bs -> bs.acnArgs | _ -> [] + + member this.maxAlignment = + match this.Kind with + | Sequence sq -> sq.maxAlignment + | SequenceOf sqf -> sqf.maxAlignment + | Choice ch -> ch.maxAlignment + | ReferenceType tp -> tp.maxAlignment + | _ -> this.acnAlignment + and Asn1TypeKind = | Integer of Integer @@ -733,6 +742,7 @@ and SequenceOf = { acnArgs : RelativePath list typeDef : Map definitionOrRef : Map + maxAlignment : AcnAlignment option } @@ -748,6 +758,7 @@ and Sequence = { acnArgs : RelativePath list typeDef : Map definitionOrRef : Map + maxAlignment : AcnAlignment option } and AcnChild = { @@ -796,6 +807,7 @@ and Choice = { acnLoc : SrcLoc option typeDef : Map definitionOrRef : Map + maxAlignment : AcnAlignment option } and ChChildInfo = { @@ -837,6 +849,7 @@ and ReferenceType = { encodingOptions : EncodeWithinOctetOrBitStringProperties option refCons : AnyConstraint list definitionOrRef : Map + maxAlignment : AcnAlignment option } type Asn1AcnType = diff --git a/FrontEndAst/DAstTypeDefinition.fs b/FrontEndAst/DAstTypeDefinition.fs index 2ad2d8a9..f5a381f4 100644 --- a/FrontEndAst/DAstTypeDefinition.fs +++ b/FrontEndAst/DAstTypeDefinition.fs @@ -438,7 +438,7 @@ let createEnumerated_u (args:CommandLineSettings) (lm:LanguageMacros) (id:Refer | NonPrimitiveReference2OtherType -> ReferenceToExistingDefinition {ReferenceToExistingDefinition.programUnit = (if td.programUnit = programUnit then None else Some td.programUnit); typedefName= td.typeName; definedInRtl = false} -let createSequenceOf_u (lm:LanguageMacros) (id:ReferenceToType) (typeDef : Map) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (minSize : SIZE) (maxSize : SIZE) (acnEncodingClass : Asn1AcnAst.SizeableAcnEncodingClass) (acnAlignment : AcnGenericTypes.AcnAlignment option) (child : Asn1AcnAst.Asn1Type) = +let createSequenceOf_u (lm:LanguageMacros) (id:ReferenceToType) (typeDef : Map) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (minSize : SIZE) (maxSize : SIZE) (acnEncodingClass : Asn1AcnAst.SizeableAcnEncodingClass) (acnAlignment : AcnGenericTypes.AcnAlignment option) (maxAlignment: AcnGenericTypes.AcnAlignment option) (child : Asn1AcnAst.Asn1Type) = let childTypeDefinitionOrReference = lm.lg.definitionOrRef child.typeDefinitionOrReference let createSequenceOf () = let define_new_sequence_of = lm.typeDef.Define_new_sequence_of @@ -448,7 +448,7 @@ let createSequenceOf_u (lm:LanguageMacros) (id:ReferenceToType) (typeDef : Map< match td.kind with | NonPrimitiveNewTypeDefinition -> let invariants = lm.lg.generateSequenceOfInvariants minSize maxSize - let sizeClsDefinitions, sizeObjDefinitions = lm.lg.generateSequenceOfSizeDefinitions typeDef acnMinSizeInBits acnMaxSizeInBits maxSize acnEncodingClass acnAlignment child + let sizeClsDefinitions, sizeObjDefinitions = lm.lg.generateSequenceOfSizeDefinitions typeDef acnMinSizeInBits acnMaxSizeInBits maxSize acnEncodingClass acnAlignment maxAlignment child let completeDefinition = define_new_sequence_of td minSize.uper maxSize.uper (minSize.uper = maxSize.uper) (childTypeDefinitionOrReference.longTypedefName2 lm.lg.hasModules) (getChildDefinition childTypeDefinitionOrReference) sizeClsDefinitions sizeObjDefinitions invariants let privateDefinition = match childTypeDefinitionOrReference with @@ -481,7 +481,7 @@ let createSequenceOf_u (lm:LanguageMacros) (id:ReferenceToType) (typeDef : Map< ReferenceToExistingDefinition {ReferenceToExistingDefinition.programUnit = (if td.programUnit = programUnit then None else Some td.programUnit); typedefName= td.typeName; definedInRtl = false} -let createSequence_u (args:CommandLineSettings) (lm:LanguageMacros) (typeDef:Map) (id: ReferenceToType) (acnAlignment : AcnGenericTypes.AcnAlignment option) (acnProperties : AcnGenericTypes.SequenceAcnProperties) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (children:Asn1AcnAst.SeqChildInfo list) = +let createSequence_u (args:CommandLineSettings) (lm:LanguageMacros) (typeDef:Map) (id: ReferenceToType) (acnAlignment : AcnGenericTypes.AcnAlignment option) (maxAlignment: AcnGenericTypes.AcnAlignment option) (acnProperties : AcnGenericTypes.SequenceAcnProperties) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (children:Asn1AcnAst.SeqChildInfo list) = let createSequence (allchildren: Asn1AcnAst.SeqChildInfo list) = let define_new_sequence = lm.typeDef.Define_new_sequence let define_new_sequence_child = lm.typeDef.Define_new_sequence_child @@ -525,7 +525,7 @@ let createSequence_u (args:CommandLineSettings) (lm:LanguageMacros) (typeDef:Map match td.kind with | NonPrimitiveNewTypeDefinition -> let invariants = lm.lg.generateSequenceInvariants children - let sizeDefinitions = lm.lg.generateSequenceSizeDefinitions acnAlignment acnMinSizeInBits acnMaxSizeInBits allchildren + let sizeDefinitions = lm.lg.generateSequenceSizeDefinitions acnAlignment maxAlignment acnMinSizeInBits acnMaxSizeInBits allchildren let completeDefinition = define_new_sequence td arrsChildren arrsOptionalChildren childrenCompleteDefinitions arrsNullFieldsSavePos sizeDefinitions invariants let privateDef = match childrenPrivatePart with @@ -553,7 +553,7 @@ let createSequence_u (args:CommandLineSettings) (lm:LanguageMacros) (typeDef:Map | NonPrimitiveReference2OtherType -> ReferenceToExistingDefinition {ReferenceToExistingDefinition.programUnit = (if td.programUnit = programUnit then None else Some td.programUnit); typedefName= td.typeName; definedInRtl = false} -let createChoice_u (args:CommandLineSettings) (typeIdsSet : Map) (lm:LanguageMacros) (typeDef:Map) (id: ReferenceToType) (acnProperties : AcnGenericTypes.ChoiceAcnProperties) (acnAlignment : AcnGenericTypes.AcnAlignment option) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (children:Asn1AcnAst.ChChildInfo list) = +let createChoice_u (args:CommandLineSettings) (typeIdsSet : Map) (lm:LanguageMacros) (typeDef:Map) (id: ReferenceToType) (acnProperties : AcnGenericTypes.ChoiceAcnProperties) (acnAlignment : AcnGenericTypes.AcnAlignment option) (maxAlignment: AcnGenericTypes.AcnAlignment option) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (children:Asn1AcnAst.ChChildInfo list) = let createChoice (children:Asn1AcnAst.ChChildInfo list) = let define_new_choice = lm.typeDef.Define_new_choice let define_new_choice_child = lm.typeDef.Define_new_choice_child @@ -580,7 +580,7 @@ let createChoice_u (args:CommandLineSettings) (typeIdsSet : Map) (lm match td.kind with | NonPrimitiveNewTypeDefinition -> - let sizeDefinitions = lm.lg.generateChoiceSizeDefinitions acnAlignment acnMinSizeInBits acnMaxSizeInBits typeDef children + let sizeDefinitions = lm.lg.generateChoiceSizeDefinitions acnAlignment maxAlignment acnMinSizeInBits acnMaxSizeInBits typeDef children let completeDefinition = define_new_choice td (lm.lg.choiceIDForNone typeIdsSet id) (lm.lg.presentWhenName0 None children.Head) arrsChildren arrsPresent arrsCombined nIndexMax childrenCompleteDefinitions sizeDefinitions Some (completeDefinition, privatePart) | NonPrimitiveNewSubTypeDefinition subDef -> diff --git a/FrontEndAst/Language.fs b/FrontEndAst/Language.fs index c61a2da4..6c7133c2 100644 --- a/FrontEndAst/Language.fs +++ b/FrontEndAst/Language.fs @@ -350,10 +350,10 @@ type ILangGeneric () = abstract member generateSequenceInvariants: Asn1AcnAst.Asn1Child list-> string list abstract member generateSequenceOfInvariants: SIZE -> SIZE -> string list - abstract member generateSequenceSizeDefinitions: (AcnGenericTypes.AcnAlignment option)-> (BigInteger)->(BigInteger)-> (Asn1AcnAst.SeqChildInfo list) -> string list - abstract member generateChoiceSizeDefinitions: AcnGenericTypes.AcnAlignment option -> BigInteger->BigInteger->Map->Asn1AcnAst.ChChildInfo list-> string list + abstract member generateSequenceSizeDefinitions: (AcnGenericTypes.AcnAlignment option)-> (AcnGenericTypes.AcnAlignment option)-> (BigInteger)->(BigInteger)-> (Asn1AcnAst.SeqChildInfo list) -> string list + abstract member generateChoiceSizeDefinitions: AcnGenericTypes.AcnAlignment option ->AcnGenericTypes.AcnAlignment option-> BigInteger->BigInteger->Map->Asn1AcnAst.ChChildInfo list-> string list //(typeDef : Map) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (maxSize : SIZE) (acnEncodingClass : SizeableAcnEncodingClass) (acnAlignment : AcnAlignment option) (child : Asn1AcnAst.Asn1Type) - abstract member generateSequenceOfSizeDefinitions: Map -> BigInteger -> BigInteger-> SIZE -> Asn1AcnAst.SizeableAcnEncodingClass -> AcnGenericTypes.AcnAlignment option -> Asn1AcnAst.Asn1Type -> string list * string list + abstract member generateSequenceOfSizeDefinitions: Map -> BigInteger -> BigInteger-> SIZE -> Asn1AcnAst.SizeableAcnEncodingClass -> AcnGenericTypes.AcnAlignment option -> AcnGenericTypes.AcnAlignment option -> Asn1AcnAst.Asn1Type -> string list * string list abstract member generateSequenceSubtypeDefinitions: dealiased: string -> Map -> Asn1AcnAst.Asn1Child list -> string list abstract member real_annotations : string list @@ -398,9 +398,9 @@ type ILangGeneric () = default this.generateSequenceInvariants _ = [] default this.generateSequenceOfInvariants _ _ = [] - default this.generateSequenceSizeDefinitions _ _ _ _ = [] - default this.generateChoiceSizeDefinitions _ _ _ _ _ = [] - default this.generateSequenceOfSizeDefinitions _ _ _ _ _ _ _ = [], [] + default this.generateSequenceSizeDefinitions _ _ _ _ _ = [] + default this.generateChoiceSizeDefinitions _ _ _ _ _ _ = [] + default this.generateSequenceOfSizeDefinitions _ _ _ _ _ _ _ _ = [], [] default this.generateSequenceSubtypeDefinitions _ _ _ = [] //most programming languages are case sensitive diff --git a/StgScala/LangGeneric_scala.fs b/StgScala/LangGeneric_scala.fs index ba083bad..4102c66c 100644 --- a/StgScala/LangGeneric_scala.fs +++ b/StgScala/LangGeneric_scala.fs @@ -467,18 +467,18 @@ type LangGeneric_scala() = let inv = sequenceOfInvariants minSize maxSize This [$"require({show (ExprTree inv)})"] - override this.generateSequenceSizeDefinitions (acnAlignment : AcnGenericTypes.AcnAlignment option) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (children : Asn1AcnAst.SeqChildInfo list): string list = - generateSequenceSizeDefinitions acnAlignment acnMinSizeInBits acnMaxSizeInBits children + override this.generateSequenceSizeDefinitions (acnAlignment : AcnGenericTypes.AcnAlignment option) (maxAlignment: AcnGenericTypes.AcnAlignment option) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (children : Asn1AcnAst.SeqChildInfo list): string list = + generateSequenceSizeDefinitions acnAlignment maxAlignment acnMinSizeInBits acnMaxSizeInBits children - override this.generateChoiceSizeDefinitions (acnAlignment : AcnGenericTypes.AcnAlignment option) + override this.generateChoiceSizeDefinitions (acnAlignment : AcnGenericTypes.AcnAlignment option) (maxAlignment: AcnGenericTypes.AcnAlignment option) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (typeDef : Map) (children : Asn1AcnAst.ChChildInfo list): string list = - generateChoiceSizeDefinitions acnAlignment acnMinSizeInBits acnMaxSizeInBits typeDef children + generateChoiceSizeDefinitions acnAlignment maxAlignment acnMinSizeInBits acnMaxSizeInBits typeDef children - override this.generateSequenceOfSizeDefinitions (typeDef : Map) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (maxSize : SIZE) (acnEncodingClass : Asn1AcnAst.SizeableAcnEncodingClass) (acnAlignment : AcnGenericTypes.AcnAlignment option) (child : Asn1AcnAst.Asn1Type): string list * string list = - generateSequenceOfSizeDefinitions typeDef acnMinSizeInBits acnMaxSizeInBits maxSize acnEncodingClass acnAlignment child + override this.generateSequenceOfSizeDefinitions (typeDef : Map) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (maxSize : SIZE) (acnEncodingClass : Asn1AcnAst.SizeableAcnEncodingClass) (acnAlignment : AcnGenericTypes.AcnAlignment option) (maxAlignment: AcnGenericTypes.AcnAlignment option) (child : Asn1AcnAst.Asn1Type): string list * string list = + generateSequenceOfSizeDefinitions typeDef acnMinSizeInBits acnMaxSizeInBits maxSize acnEncodingClass acnAlignment maxAlignment child override this.generateSequenceSubtypeDefinitions (dealiased: string) (typeDef:Map) (children: Asn1AcnAst.Asn1Child list): string list = generateSequenceSubtypeDefinitions dealiased typeDef children diff --git a/StgScala/ProofGen.fs b/StgScala/ProofGen.fs index bb6be032..42eefa78 100644 --- a/StgScala/ProofGen.fs +++ b/StgScala/ProofGen.fs @@ -126,7 +126,7 @@ let acnTypeSizeExpr (acn: AcnInsertedType): Expr = | AcnReferenceToIA5String s -> if s.str.acnMinSizeInBits <> s.str.acnMaxSizeInBits then failwith "TODO" else longlit s.str.acnMaxSizeInBits - +(* let maxAlignmentOf (aligns: AcnAlignment option list): AcnAlignment option = assert (not aligns.IsEmpty) aligns |> List.maxBy (fun a -> a |> Option.map (fun a -> a.nbBits) |> Option.defaultValue 0I) @@ -144,7 +144,7 @@ let rec maxAlignment (tp: Asn1AcnAst.Asn1Type): AcnAlignment option = | SequenceOf sqf -> maxAlignmentOf [tp.acnAlignment; maxAlignment sqf.child] | _ -> tp.acnAlignment - +*) let sizeLemmaId(align: AcnAlignment option): string = match align with | None -> "sizeLemmaAnyOffset" @@ -458,7 +458,7 @@ let optionalSizeExpr (child: Asn1AcnAst.Asn1Child) -let seqSizeFunDefs (acnAlignment : AcnAlignment option) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (children : SeqChildInfo list) : FunDef list = +let seqSizeFunDefs (acnAlignment : AcnAlignment option) (maxAlignment: AcnAlignment option) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (children : SeqChildInfo list) : FunDef list = // TODO: Pour les int, on peut ajouter une assertion GetBitUnsignedCount(...) == resultat (ici et/ou ailleurs) let offset = {Var.name = "offset"; tpe = IntegerType Long} let res = seqSizeExpr children acnAlignment This (Var offset) 0I 0I @@ -522,14 +522,13 @@ let seqSizeFunDefs (acnAlignment : AcnAlignment option) (acnMinSizeInBits : B returnTpe = IntegerType Long body = finalSize } - //SOS: We need to calculate the max alignment of the sequence to generate the lemmas - //currently we are assuming that the max alignment is the same as the alignment of the sequence - let maxAlign = acnAlignment // maxAlignment t + let maxAlign = maxAlignment let implyingAligns = implyingAlignments maxAlign let lemmas = implyingAligns |> List.map sizeLemmas sizeFd :: lemmas let choiceSizeFunDefs (acnAlignment : AcnAlignment option) + (maxAlignment: AcnAlignment option) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (typeDef : Map) @@ -565,13 +564,12 @@ let choiceSizeFunDefs (acnAlignment : AcnAlignment option) returnTpe = IntegerType Long body = sizeRes.resSize } - //SOS: We need to calculate the max alignment of the choice to generate the lemmas - let maxAlign = acnAlignment //maxAlignment t + let maxAlign = maxAlignment let implyingAligns = implyingAlignments maxAlign let lemmas = implyingAligns |> List.map sizeLemmas sizeFd :: lemmas -let seqOfSizeFunDefs (typeDef : Map) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (maxSize : SIZE) (acnEncodingClass : SizeableAcnEncodingClass) (acnAlignment : AcnAlignment option) (child : Asn1AcnAst.Asn1Type) : FunDef list * FunDef list = +let seqOfSizeFunDefs (typeDef : Map) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (maxSize : SIZE) (acnEncodingClass : SizeableAcnEncodingClass) (acnAlignment : AcnAlignment option) (maxAlignment: AcnAlignment option) (child : Asn1AcnAst.Asn1Type) : FunDef list * FunDef list = let td = typeDef.[Scala].typeName let elemTpe = fromAsn1TypeKind child.Kind let lsTpe = vecTpe elemTpe @@ -749,29 +747,28 @@ let seqOfSizeFunDefs (typeDef : Map List.map sizeLemmas |> List.unzip sizeClsFd :: clsLemmas, sizeRangeObjFd :: objLemmas -let generateSequenceSizeDefinitions (acnAlignment : AcnAlignment option) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (children : SeqChildInfo list): string list = - let fds = seqSizeFunDefs acnAlignment acnMinSizeInBits acnMaxSizeInBits children +let generateSequenceSizeDefinitions (acnAlignment : AcnAlignment option) (maxAlignment: AcnAlignment option) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (children : SeqChildInfo list): string list = + let fds = seqSizeFunDefs acnAlignment maxAlignment acnMinSizeInBits acnMaxSizeInBits children fds |> List.map (fun fd -> show (FunDefTree fd)) let generateChoiceSizeDefinitions (acnAlignment : AcnAlignment option) + (maxAlignment: AcnAlignment option) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (typeDef : Map) (children : Asn1AcnAst.ChChildInfo list) : string list = - let fds = choiceSizeFunDefs acnAlignment acnMinSizeInBits acnMaxSizeInBits typeDef children + let fds = choiceSizeFunDefs acnAlignment maxAlignment acnMinSizeInBits acnMaxSizeInBits typeDef children fds |> List.map (fun fd -> show (FunDefTree fd)) -let generateSequenceOfSizeDefinitions (typeDef : Map) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (maxSize : SIZE) (acnEncodingClass : SizeableAcnEncodingClass) (acnAlignment : AcnAlignment option) (child : Asn1AcnAst.Asn1Type): string list * string list = - let fdsCls, fdsObj = seqOfSizeFunDefs typeDef acnMinSizeInBits acnMaxSizeInBits maxSize acnEncodingClass acnAlignment child +let generateSequenceOfSizeDefinitions (typeDef : Map) (acnMinSizeInBits : BigInteger) (acnMaxSizeInBits : BigInteger) (maxSize : SIZE) (acnEncodingClass : SizeableAcnEncodingClass) (acnAlignment : AcnAlignment option) (maxAlignment: AcnAlignment option) (child : Asn1AcnAst.Asn1Type): string list * string list = + let fdsCls, fdsObj = seqOfSizeFunDefs typeDef acnMinSizeInBits acnMaxSizeInBits maxSize acnEncodingClass acnAlignment maxAlignment child fdsCls |> List.map (fun fd -> show (FunDefTree fd)), fdsObj |> List.map (fun fd -> show (FunDefTree fd)) let generateSequenceSubtypeDefinitions (dealiased: string) (typeDef:Map) (children: Asn1AcnAst.Asn1Child list): string list =