Skip to content

Commit

Permalink
Merge pull request #28 from epfl-lara/catchup
Browse files Browse the repository at this point in the history
Merge with the latest changes
  • Loading branch information
mario-bucev authored Sep 9, 2024
2 parents 4158bcc + c44f2b4 commit 5ccc56f
Show file tree
Hide file tree
Showing 11 changed files with 276 additions and 246 deletions.
233 changes: 106 additions & 127 deletions BackendAst/DAstACN.fs

Large diffs are not rendered by default.

73 changes: 29 additions & 44 deletions BackendAst/DAstUPer.fs

Large diffs are not rendered by default.

73 changes: 73 additions & 0 deletions BackendAst/DAstUtilFunctions.fs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,9 @@ open Asn1AcnAst
open Asn1AcnAstUtilFunctions
open DAst
open Language
open System.Xml.Serialization
open System.IO
//open Newtonsoft.Json

let getAccessFromScopeNodeList (ReferenceToType nodes) (childTypeIsString: bool) (lm:LanguageMacros) (pVal : CallerScope) =
let handleNode zeroBasedSequenceOfLevel (pVal : CallerScope) (n:ScopeNode) (childTypeIsString: bool) =
Expand Down Expand Up @@ -1061,3 +1064,73 @@ let getBaseFuncName (lm:LanguageMacros) (typeDefinition:TypeDefinitionOrReferenc
| true -> typeDefinitionName0
| false -> moduleName + "." + typeDefinitionName0
baseTypeDefinitionName, baseTypeDefinitionName + methodSuffix + codec.suffix


let serializeIcdTasToXml (icdTypeAss: IcdTypeAss) =
let serializer = XmlSerializer(typeof<IcdTypeAss>)
use stringWriter = new StringWriter()
serializer.Serialize(stringWriter, icdTypeAss)
stringWriter.ToString()

//let serializeIcdTasToJson (icdTypeAss: IcdTypeAss) =
// JsonConvert.SerializeObject(icdTypeAss)

(*
and IcdTypeAss = {
linkId : ReferenceToType
tasInfo : TypeAssignmentInfo option
asn1Link : string option
acnLink : string option
name : string
kind : string
comments : string list
rows : IcdRow list
compositeChildren : IcdTypeAss list
minLengthInBytes : BigInteger
maxLengthInBytes : BigInteger
hash : string
canBeEmbedded : bool
hasAcnDefinition : bool
*)

let md5 = System.Security.Cryptography.MD5.Create()
let calcIcdTypeAssHash (t1:IcdTypeAss) =
let rec calcIcdTypeAssHash_aux (t1:IcdTypeAss) =
let rws =
t1.rows |>
Seq.map(fun r -> sprintf "%A%A%A%A%A%A%A%A%A%A" r.idxOffset r.fieldName r.comments r.sPresent r.sType r.sConstraint r.minLengthInBits r.maxLengthInBits r.sUnits r.rowType) |>
Seq.StrJoin ""
let aa = sprintf"%A%A%A%A%A%A%A%A%A" t1.acnLink t1.asn1Link t1.name t1.kind t1.comments t1.minLengthInBytes t1.maxLengthInBytes (rws) ("")
let bytes = md5.ComputeHash(System.Text.Encoding.UTF8.GetBytes aa)
Convert.ToHexString bytes
calcIcdTypeAssHash_aux t1

let serializeIcdTasToText (icdTypeAss: IcdTypeAss) =
let printRow (r:IcdRow) =
sprintf """
idxOffset = %A
fieldName = %A
comments = %A
sPresent = %A
sType = %A
sConstraint = %A
minLengthInBits = %A
maxLengthInBits = %A
sUnits = %A
rowType = %A
""" r.idxOffset r.fieldName r.comments r.sPresent r.sType r.sConstraint r.minLengthInBits r.maxLengthInBits r.sUnits r.rowType

//let aa = sprintf"%A%A%A%A%A%A%A%A%A" t1.acnLink t1.asn1Link t1.name t1.kind t1.comments t1.minLengthInBytes t1.maxLengthInBytes (rws) ("")
let rws = icdTypeAss.rows |> Seq.map printRow |> Seq.StrJoin "\n"
sprintf """
acnLink = %A
asn1Link = %A
name = %A
kind = %A
comments = %A
minLengthInBytes = %A
maxLengthInBytes = %A
rows =
%A
""" icdTypeAss.acnLink icdTypeAss.asn1Link icdTypeAss.name icdTypeAss.kind icdTypeAss.comments icdTypeAss.minLengthInBytes icdTypeAss.maxLengthInBytes rws
89 changes: 58 additions & 31 deletions BackendAst/GenerateAcnIcd.fs
Original file line number Diff line number Diff line change
Expand Up @@ -625,11 +625,12 @@ let emitIcdRow stgFileName (r:AstRoot) _i (rw:IcdRow) =
| _ -> icd_acn.EmitSeqOrChoiceRow stgFileName sClass (BigInteger i) rw.fieldName sComment rw.sPresent (emitTypeCol stgFileName r rw.sType) sConstraint (rw.minLengthInBits.ToString()) (rw.maxLengthInBits.ToString()) None rw.sUnits

let emitTas2 stgFileName (r:AstRoot) myParams (icdTas:IcdTypeAss) =
let sCommentLine = icdTas.hash::icdTas.comments |> Seq.StrJoin (icd_uper.NewLine stgFileName ())
let sCommentLine = icdTas.comments |> Seq.StrJoin (icd_uper.NewLine stgFileName ())
let arRows =
icdTas.rows |> List.mapi (fun i rw -> emitIcdRow stgFileName r (i+1) rw)
let bHasAcnDef = icdTas.hasAcnDefinition
icd_acn.EmitSequenceOrChoice stgFileName false icdTas.name icdTas.hash bHasAcnDef (icdTas.kind) (icdTas.minLengthInBytes.ToString()) (icdTas.maxLengthInBytes.ToString()) "sMaxBitsExplained" sCommentLine arRows (myParams 4I) (sCommentLine.Split [|'\n'|])
let sMaxBitsExplained = ""
icd_acn.EmitSequenceOrChoice stgFileName false icdTas.name icdTas.hash bHasAcnDef (icdTas.kind) (icdTas.minLengthInBytes.ToString()) (icdTas.maxLengthInBytes.ToString()) sMaxBitsExplained sCommentLine arRows (myParams 4I) (sCommentLine.Split [|'\n'|])

(*
let rec PrintType2 stgFileName (r:AstRoot) acnParams (icdTas:IcdTypeAss): string list =
Expand Down Expand Up @@ -717,17 +718,31 @@ let printTasses3 stgFileName (r:DAst.AstRoot) : (string list)*(string list) =
(files, icdHashesToPrint)

let PrintAsn1FileInColorizedHtml (stgFileName:string) (r:AstRoot) (icdHashesToPrint:string list) (f:Asn1File) =
let debug (tsName:string) =
r.icdHashes.Values |>
Seq.collect id |>
Seq.filter(fun ts -> ts.name = tsName) |>
Seq.iter(fun ts ->
let content = DAstUtilFunctions.serializeIcdTasToText ts
let fileName = sprintf "%s_%s.txt" tsName ts.hash
File.WriteAllText(fileName, content))
//debug("ALPHA-TC-SECONDARY-HEADER")
//let tryCreateRefType = CreateAsn1AstFromAntlrTree.CreateRefTypeContent
let icdHashesToPrintSet = icdHashesToPrint |> Set.ofList
let fileModules = f.Modules |> List.map(fun m -> m.Name.Value) |> Set.ofList
let fileTypeAssignments =
r.icdHashes.Values |>
Seq.collect id |>
Seq.choose(fun z ->
match z.tasInfo with
| None -> None
| Some ts when icdHashesToPrintSet.Contains z.hash && fileModules.Contains ts.modName -> Some (ts.tasName, z.hash)
| Some _ -> None ) |> Seq.toList
//match z.tasInfo with
//| None -> None
//| Some ts when icdHashesToPrintSet.Contains z.hash && fileModules.Contains ts.modName -> Some (ts.tasName, z.hash)
//| Some _ -> None ) |>
match icdHashesToPrintSet.Contains z.hash with
| true -> Some (z.name, z.hash)
| false -> None ) |>
Seq.distinct |>
Seq.toList


//let blueTasses = f.Modules |> Seq.collect(fun m -> getModuleBlueTasses m)
Expand All @@ -749,45 +764,57 @@ let PrintAsn1FileInColorizedHtml (stgFileName:string) (r:AstRoot) (icdHashesToPr
let isAsn1Token = GenerateUperIcd.asn1Tokens.Contains t.Text
//let isType = containedIn tasses
let safeText = t.Text.Replace("<",lt).Replace(">",gt)
let checkWsCmt (tok: IToken) =
match tok.Type with
|asn1Lexer.WS
|asn1Lexer.COMMENT
|asn1Lexer.COMMENT2 -> false
|_ -> true
let findToken = Array.tryFind(fun tok -> checkWsCmt tok)
let findNextToken = f.Tokens.[idx+1..] |> findToken
let findPrevToken = Array.rev f.Tokens.[0..idx-1] |> findToken
let nextToken =
let size = Seq.length(f.Tokens) - 1
match findNextToken with
|Some(tok) -> tok
|None -> if idx = size then t else f.Tokens.[idx+1]
let prevToken =
match findPrevToken with
|Some(tok) -> tok
|None -> if idx = 0 then t else f.Tokens.[idx-1]
let uid =
//match fileTypeAssignments.TryFind t.Text with
match fileTypeAssignments |> List.filter(fun (tasName,_) -> tasName = t.Text) with
let uid () =
let checkWsCmt (tok: IToken) =
match tok.Type with
|asn1Lexer.WS
|asn1Lexer.COMMENT
|asn1Lexer.COMMENT2 -> false
|_ -> true
let findToken = Array.tryFind(fun tok -> checkWsCmt tok)
let findNextToken = f.Tokens.[idx+1..] |> findToken
let findPrevToken = Array.rev f.Tokens.[0..idx-1] |> findToken
let nextToken =
let size = Seq.length(f.Tokens) - 1
match findNextToken with
|Some(tok) -> tok
|None -> if idx = size then t else f.Tokens.[idx+1]
let prevToken =
match findPrevToken with
|Some(tok) -> tok
|None -> if idx = 0 then t else f.Tokens.[idx-1]
let tasfileTypeAssignments = fileTypeAssignments |> List.filter(fun (tasName,_) -> tasName = t.Text)
match tasfileTypeAssignments with
| [] -> safeText
//|Some tasHash ->
| (_,tasHash)::[] ->
if nextToken.Type = asn1Lexer.ASSIG_OP && prevToken.Type <> asn1Lexer.LID then
icd_uper.TasName stgFileName safeText tasHash
else
icd_uper.TasName2 stgFileName safeText tasHash
| _ ->
//printfn "Warning: %s is not unique" t.Text
//printfn "Warning: %A" (fileTypeAssignments |> List.filter(fun (tasName,_) -> tasName = t.Text))
let debug () =
printfn "Warning: %s is not unique. %d" t.Text tasfileTypeAssignments.Length

printfn "Warning: %A" tasfileTypeAssignments
//print to jso the type assignments that are not unique
tasfileTypeAssignments |>
Seq.iter (fun (tasName, tasHash) ->
let icdTas = r.icdHashes.[tasHash]
icdTas |>
Seq.iter(fun icdTas ->
let content = DAstUtilFunctions.serializeIcdTasToText icdTas
let fileName = sprintf "%s_%s.txt" tasName icdTas.hash
File.WriteAllText(fileName, content)))

//debug ()
safeText
//|None -> safeText
let colored =
match t.Type with
|asn1Lexer.StringLiteral
|asn1Lexer.OctectStringLiteral
|asn1Lexer.BitStringLiteral -> icd_uper.StringLiteral stgFileName safeText
|asn1Lexer.UID -> uid
|asn1Lexer.UID -> uid ()
|asn1Lexer.COMMENT
|asn1Lexer.COMMENT2 -> icd_uper.Comment stgFileName safeText
|_ -> safeText
Expand Down
4 changes: 2 additions & 2 deletions CommonTypes/FsUtils.fs
Original file line number Diff line number Diff line change
Expand Up @@ -393,8 +393,8 @@ module List =
match xs with
| [] -> None
| x :: xs ->
match f(x) with
| Some(b) -> Some(b)
match f x with
| Some b -> Some b
| None -> tryFindMap f xs

let foldBackWith (f: 'a -> 's -> 's) (init: 'a -> 's) (xs: 'a list): 's =
Expand Down
6 changes: 6 additions & 0 deletions FrontEndAst/AcnCreateFromAntlr.fs
Original file line number Diff line number Diff line change
Expand Up @@ -983,6 +983,12 @@ let rec private mergeType (asn1:Asn1Ast.AstRoot) (acn:AcnAst) (m:Asn1Ast.Asn1Mo
let acnErrLoc = acnType |> Option.map(fun x -> x.loc)
let combinedProperties = acnProps
let allCons = t.Constraints@refTypeCons@withCons
let debug = ReferenceToType curPath
//if debug.AsString.EndsWith "ALPHA-DELETE-DIAGNOSTIC-PARAMETER-REPORT-STRUCTURES-GENERIC" then
// printfn "%s" debug.AsString
//if debug.AsString = "RW90-DATAVIEW.UART-Config.timeout" then
// printfn "%s" debug.AsString

let tfdArg = {GetTypeDefinition_arg.asn1TypeKind = t.Kind; loc = t.Location; curPath = curPath; typeDefPath = typeDefPath; enmItemTypeDefPath = enmItemTypeDefPath; inheritInfo = inheritInfo; typeAssignmentInfo = typeAssignmentInfo; rtlFnc = None; blm=asn1.args.blm}
let fixConstraint = fixConstraint asn1

Expand Down
22 changes: 0 additions & 22 deletions FrontEndAst/DAst.fs
Original file line number Diff line number Diff line change
Expand Up @@ -382,26 +382,8 @@ type Asn1IntegerEncodingType =
| UnconstrainedMax of bigint
| Unconstrained

type TypeEncodingKind = // TODO: Alignment???
| Asn1IntegerEncodingType of Asn1IntegerEncodingType option // None if range min = max
| Asn1RealEncodingType of Asn1AcnAst.RealClass
| AcnIntegerEncodingType of AcnIntegerEncodingType
| AcnRealEncodingType of AcnRealEncodingType
| AcnBooleanEncodingType of AcnBooleanEncoding option
| AcnNullEncodingType of PATTERN_PROP_VALUE option
| AcnStringEncodingType of Asn1AcnAst.StringAcnEncodingClass
| AcnOctetStringEncodingType of Asn1AcnAst.SizeableAcnEncodingClass
| AcnBitStringEncodingType of Asn1AcnAst.SizeableAcnEncodingClass
| SequenceOfEncodingType of TypeEncodingKind * Asn1AcnAst.SizeableAcnEncodingClass
| SequenceEncodingType of TypeEncodingKind option list
| ChoiceEncodingType of TypeEncodingKind option list
| ReferenceEncodingType of string
| OptionEncodingType of TypeEncodingKind
| Placeholder

/////////////////////////////////////////////////////////////////////


type NestingScope = {
acnOuterMaxSize: bigint
uperOuterMaxSize: bigint
Expand Down Expand Up @@ -429,7 +411,6 @@ type UPERFuncBodyResult = {
bValIsUnReferenced : bool
bBsIsUnReferenced : bool
resultExpr : string option
typeEncodingKind : TypeEncodingKind option
auxiliaries : string list
}
type UPerFunction = {
Expand Down Expand Up @@ -457,7 +438,6 @@ type AcnFuncBodyResult = {
bValIsUnReferenced : bool
bBsIsUnReferenced : bool
resultExpr : string option
typeEncodingKind : TypeEncodingKind option
auxiliaries : string list
icdResult : IcdArgAux option
}
Expand Down Expand Up @@ -843,7 +823,6 @@ and Asn1Child = {
isEqualBodyStats : CallerScope -> CallerScope -> (string*(LocalVariable list)) option
Type : Asn1Type
Optionality : Asn1AcnAst.Asn1Optionality option
// acnArgs : RelativePath list
Comments : string array
} with
member this.toAsn1AcnAst: Asn1AcnAst.Asn1Child =
Expand All @@ -854,7 +833,6 @@ and Asn1Child = {
_ada_name = this._ada_name
Type = this.Type.toAsn1AcnAst
Optionality = this.Optionality
// acnArgs = this.acnArgs
asn1Comments = this.Comments |> Array.toList
acnComments = []
}
Expand Down
16 changes: 0 additions & 16 deletions FrontEndAst/Language.fs
Original file line number Diff line number Diff line change
Expand Up @@ -55,18 +55,6 @@ type UncheckedAccessKind =
| FullAccess // unwrap all selection, including the last one
| PartialAccess // unwrap all but the last selection

// TODO: Remove?
type TypeInfo = {
uperMaxSizeBits: bigint
acnMaxSizeBits: bigint
typeKind: TypeEncodingKind option
} with
member this.maxSize (enc: Asn1Encoding): bigint =
match enc with
| ACN -> this.acnMaxSizeBits
| UPER -> this.uperMaxSizeBits
| _ -> raise (BugErrorException $"Unexpected encoding: {enc}")

type SequenceChildProps = {
info: Asn1AcnAst.SeqChildInfo
sel: Selection
Expand Down Expand Up @@ -100,9 +88,6 @@ type SequenceProofGen = {
| UPER -> this.uperSiblingMaxSize
| _ -> raise (BugErrorException $"Unexpected encoding: {enc}")

// member this.maxSize (enc: Asn1Encoding): BigInteger =
// this.children |> List.map (fun c -> c.typeInfo.maxSize enc) |> List.sum

member this.outerMaxSize (enc: Asn1Encoding): bigint =
match enc with
| ACN -> this.acnOuterMaxSize
Expand Down Expand Up @@ -183,7 +168,6 @@ type SequenceOfLikeProofGen = {
nestingIx: bigint
acnMaxOffset: bigint
uperMaxOffset: bigint
typeInfo: TypeInfo
nestingScope: NestingScope
cs: CallerScope
encDec: string option
Expand Down
2 changes: 0 additions & 2 deletions StgScala/acn_scala.stg
Original file line number Diff line number Diff line change
Expand Up @@ -554,7 +554,6 @@ locally {
assert(codec.base.bitStream.bitIndex \<= oldCodec.base.bitStream.bitIndex + <nSizeInBits>L)
BitStream.validateOffsetBitsIneqLemma(oldCodec.base.bitStream, codec.base.bitStream, <nRemainingMinBits>, <nSizeInBits>L)
check(codec.base.bitStream.bitIndex \<= codec_0_1.base.bitStream.bitIndex + <nAbsOffset>L + <nSizeInBits>L)
//check(codec.base.bitStream.bitIndex \<= codec_<nLevel>_<nIx>.base.bitStream.bitIndex + <nOffset>L + <nSizeInBits>L)
}
}
<soCallAux>
Expand All @@ -575,7 +574,6 @@ val <p>_nCount = locally {
assert(codec.base.bitStream.bitIndex \<= oldCodec.base.bitStream.bitIndex + <nSizeInBits>L)
BitStream.validateOffsetBitsIneqLemma(oldCodec.base.bitStream, codec.base.bitStream, <nRemainingMinBits>, <nSizeInBits>L)
check(codec.base.bitStream.bitIndex \<= codec_0_1.base.bitStream.bitIndex + <nAbsOffset>L + <nSizeInBits>L)
//check(codec.base.bitStream.bitIndex \<= codec_<nLevel>_<nIx>.base.bitStream.bitIndex + <nOffset>L + <nSizeInBits>L)
}
<p>_nCount
}
Expand Down
2 changes: 1 addition & 1 deletion StgVarious/icdtemplate_acn.stg
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ RelativeOid() ::= "RELATIVE-OID"

EmitRowWith3Dots() ::= <<
<tr class="CommentRow">
<td class="threeDots" colspan="8"> <p>. . .</p> </td>
<td class="threeDots" colspan="9"> <p>. . .</p> </td>
</tr>
>>

Expand Down
2 changes: 1 addition & 1 deletion asn1scc/Program.fs
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ let printVersion () =
//let fvi = System.Diagnostics.FileVersionInfo.GetVersionInfo(assembly.Location);
//let version = fvi.FileVersion;

let version = "4.5.2.1"
let version = "4.5.2.2"
printfn "asn1scc version %s\n" version
()

Expand Down

0 comments on commit 5ccc56f

Please sign in to comment.