Merge pull request #27 from epfl-lara/sequence-invertibility

Sequence invertibility

BackendAst/DAstUPer.fs

@@ -100,8 +100,8 @@ let internal createUperFunction (r:Asn1AcnAst.AstRoot)
                         emptyStatement, [], [], true, isValidFuncName.IsNone, []
                     | Some bodyResult   -> bodyResult.funcBody, bodyResult.errCodes, bodyResult.localVariables, bodyResult.bBsIsUnReferenced, bodyResult.bValIsUnReferenced, bodyResult.auxiliaries
                 let lvars = bodyResult_localVariables |> List.map(fun (lv:LocalVariable) -> lm.lg.getLocalVariableDeclaration lv) |> Seq.distinct
-                let precondAnnots = lm.lg.generatePrecond UPER t codec
-                let postcondAnnots = lm.lg.generatePostcond UPER typeDef.typeName p t codec
+                let precondAnnots = lm.lg.generatePrecond r UPER t codec
+                let postcondAnnots = lm.lg.generatePostcond r UPER typeDef.typeName p t codec
                 let func = Some(EmitTypeAssignment varName sStar funcName isValidFuncName  (lm.lg.getLongTypedefName typeDefinition) lvars  bodyResult_funcBody soSparkAnnotations sInitialExp (t.uperMaxSizeInBits = 0I) bBsIsUnreferenced bVarNameIsUnreferenced soInitFuncName funcDefAnnots precondAnnots postcondAnnots codec)
 
                 let errCodStr = errCodes |> List.map(fun x -> (EmitTypeAssignment_def_err_code x.errCodeName) (BigInteger x.errCodeValue))
@@ -455,7 +455,8 @@ let createIA5StringFunction (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (codec:Co
         let pp, resultExpr = joinedOrAsIdentifier lm codec p
 
         let sqfProofGen = {
-            SequenceOfLikeProofGen.acnOuterMaxSize = nestingScope.acnOuterMaxSize
+            SequenceOfLikeProofGen.t = Asn1TypeOrAcnRefIA5.Asn1 t
+            acnOuterMaxSize = nestingScope.acnOuterMaxSize
             uperOuterMaxSize = nestingScope.uperOuterMaxSize
             nestingLevel = nestingScope.nestingLevel
             nestingIx = nestingScope.nestingIx
@@ -473,7 +474,7 @@ let createIA5StringFunction (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (codec:Co
             ixVariable = i
         }
         let introSnap = nestingScope.nestingLevel = 0I
-        let auxiliaries, callAux = lm.lg.generateSequenceOfLikeAuxiliaries (if fromACN then ACN else UPER) (StrType o) sqfProofGen codec
+        let auxiliaries, callAux = lm.lg.generateSequenceOfLikeAuxiliaries r (if fromACN then ACN else UPER) (StrType o) sqfProofGen codec
 
         let funcBodyContent,localVariables =
             match o.minSize with
@@ -616,7 +617,8 @@ let createSequenceOfFunction (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (codec:C
             let internalItem = chFunc.funcBody childNestingScope chp fromACN
 
             let sqfProofGen = {
-                SequenceOfLikeProofGen.acnOuterMaxSize = nestingScope.acnOuterMaxSize
+                SequenceOfLikeProofGen.t = Asn1TypeOrAcnRefIA5.Asn1 t
+                acnOuterMaxSize = nestingScope.acnOuterMaxSize
                 uperOuterMaxSize = nestingScope.uperOuterMaxSize
                 nestingLevel = nestingScope.nestingLevel
                 nestingIx = nestingScope.nestingIx
@@ -633,7 +635,7 @@ let createSequenceOfFunction (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (codec:C
                 elemDecodeFn = None // TODO: elemDecodeFn
                 ixVariable = i
             }
-            let auxiliaries, callAux = lm.lg.generateSequenceOfLikeAuxiliaries (if fromACN then ACN else UPER) (SqOf o) sqfProofGen codec
+            let auxiliaries, callAux = lm.lg.generateSequenceOfLikeAuxiliaries r (if fromACN then ACN else UPER) (SqOf o) sqfProofGen codec
 
             let absOffset = nestingScope.uperOffset
             let remBits = nestingScope.uperOuterMaxSize - nestingScope.uperOffset
@@ -753,8 +755,7 @@ let createSequenceFunction (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (codec:Com
                 | Decode, Copy -> Some (ToC (child._c_name + "_exist"))
                 | _ -> None
 
-            let typeInfo = {uperMaxSizeBits=child.uperMaxSizeInBits; acnMaxSizeBits=child.acnMaxSizeInBits; typeKind=childContentResult |> Option.bind (fun c -> c.typeEncodingKind)}
-            let props = {info = Some (Asn1Child child).toAsn1AcnAst; sel=Some childSel; uperMaxOffset=s.uperAccBits; acnMaxOffset=s.acnAccBits; typeInfo=typeInfo; typeKind = Asn1AcnTypeKind.Asn1 child.Type.Kind.baseKind}
+            let props = {info=(Asn1Child child).toAsn1AcnAst; sel=childSel; uperMaxOffset=s.uperAccBits; acnMaxOffset=s.acnAccBits}
             let newAcc = {childIx=s.childIx + 1I; uperAccBits=s.uperAccBits + child.uperMaxSizeInBits; acnAccBits=s.acnAccBits + child.acnMaxSizeInBits}
 
             match childContentResult with
@@ -803,19 +804,16 @@ let createSequenceFunction (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (codec:Com
         let childrenStatements00, _ = nonAcnChildren |> foldMap handleChild {childIx=nbPresenceBits; uperAccBits=nbPresenceBits; acnAccBits=nbPresenceBits}
 
         let seqProofGen =
-            let presenceBitsInfo = presenceBits |> List.mapi (fun i _ ->
-                {info = None; sel=None; uperMaxOffset = bigint i; acnMaxOffset = bigint i;
-                typeInfo = {uperMaxSizeBits = 1I; acnMaxSizeBits = 1I; typeKind = Some (AcnBooleanEncodingType None)}; typeKind = Asn1AcnTypeKind.Asn1 t.Kind})
             let children = childrenStatements00 |> List.map (fun xs -> xs.props)
-            {t = t; sel = p.arg; acnOuterMaxSize = nestingScope.acnOuterMaxSize; uperOuterMaxSize = nestingScope.uperOuterMaxSize;
+            {SequenceProofGen.t = t; sq = o; sel = p.arg; acnOuterMaxSize = nestingScope.acnOuterMaxSize; uperOuterMaxSize = nestingScope.uperOuterMaxSize;
             nestingLevel = nestingScope.nestingLevel; nestingIx = nestingScope.nestingIx;
             uperMaxOffset = nestingScope.uperOffset; acnMaxOffset = nestingScope.acnOffset;
             acnSiblingMaxSize = nestingScope.acnSiblingMaxSize; uperSiblingMaxSize = nestingScope.uperSiblingMaxSize;
-            children = presenceBitsInfo @ children}
+            children = children}
         let allStmts =
             let children = childrenStatements00 |> List.map (fun s -> s.stmt |> Option.bind (fun stmt -> stmt.body))
             presenceBits @ children
-        let childrenStatements = lm.lg.generateSequenceChildProof UPER allStmts seqProofGen codec
+        let childrenStatements = lm.lg.generateSequenceChildProof r UPER allStmts seqProofGen codec
 
         let childrenStatements0 = childrenStatements00 |> List.choose(fun s -> s.stmt)
         let childrenLocalVars = childrenStatements0 |> List.collect(fun s -> s.lvs)
@@ -908,12 +906,12 @@ let createChoiceFunction (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (codec:Commo
             let introSnap = nestingScope.nestingLevel = 0I
             let pp, resultExpr = joinedOrAsIdentifier lm codec p
             let ret = choice pp (lm.lg.getAccess p.arg) childrenContent (BigInteger (children.Length - 1)) sChoiceIndexName errCode.errCodeName td nIndexSizeInBits introSnap codec
-            let ret = lm.lg.generateChoiceProof ACN t o ret p.arg codec
+            let ret = lm.lg.generateChoiceProof r ACN t o ret p.arg codec
             Some ({UPERFuncBodyResult.funcBody = ret; errCodes = errCode::childrenErrCodes; localVariables = localVariables@childrenLocalvars; bValIsUnReferenced=false; bBsIsUnReferenced=false; resultExpr=resultExpr; typeEncodingKind=Some (ChoiceEncodingType childrenTypeKindEncoding); auxiliaries=childrenAuxiliaries})
         | Some baseFuncName ->
             let pp, resultExpr = adaptArgumentPtr lm codec p
             let funcBodyContent = callBaseTypeFunc lm pp baseFuncName codec
-            let ret = lm.lg.generateChoiceProof ACN t o funcBodyContent p.arg codec
+            let ret = lm.lg.generateChoiceProof r ACN t o funcBodyContent p.arg codec
             Some ({UPERFuncBodyResult.funcBody = funcBodyContent; errCodes = [errCode]; localVariables = []; bValIsUnReferenced=false; bBsIsUnReferenced=false; resultExpr=resultExpr; typeEncodingKind=None; auxiliaries=[]})
 
     let soSparkAnnotations = Some(sparkAnnotations lm (lm.lg.getLongTypedefName typeDefinition) codec)

BackendAst/DAstUtilFunctions.fs

@@ -919,12 +919,12 @@ type SeqChildInfo with
         | ACN -> this.acnMaxSizeInBits
         | _ -> raise (BugErrorException $"Unexpected encoding: {enc}")
 
-let hasAcnEncodeFunction (encFunc : AcnFunction option) acnParameters  =
+let hasAcnEncodeFunction (encFunc: AcnFunction option) acnParameters (tasInfo: TypeAssignmentInfo option) =
     match encFunc with
     | None  -> false
     | Some fnc ->
-        match acnParameters with
-        | [] ->
+        match acnParameters, tasInfo with
+        | [], Some _ ->
             let p = {CallerScope.modName = ""; arg = Selection.valueEmptyPath "dummy"}
             let ret,_ = fnc.funcBody emptyState [] (NestingScope.init 0I 0I []) p
             match ret with

BackendAst/DastTestCaseCreation.fs

@@ -195,7 +195,7 @@ let printAllTestCasesAndTestCaseRunner (r:DAst.AstRoot) (lm:LanguageMacros) outD
                         let encDecTestFunc = t.Type.getEncDecTestFunc e
                         match encDecTestFunc with
                         | Some _    ->
-                            let hasEncodeFunc = e <> Asn1Encoding.ACN ||  hasAcnEncodeFunction t.Type.acnEncFunction t.Type.acnParameters
+                            let hasEncodeFunc = e <> Asn1Encoding.ACN ||  hasAcnEncodeFunction t.Type.acnEncFunction t.Type.acnParameters t.Type.id.tasInfo
                             if hasEncodeFunc   then
                                 let isTestCaseValid atc =
                                     match t.Type.acnEncFunction with

BackendAst/EncodeDecodeTestCase.fs

@@ -153,7 +153,7 @@ let _createAcnEncDecFunction (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1A
     let sAmberDecode = getAmberDecode t
     let sAmberIsValid = getAmberDecode t
 
-    match hasAcnEncodeFunction encFunc t.acnParameters  with
+    match hasAcnEncodeFunction encFunc t.acnParameters t.id.tasInfo with
     | false -> None, us
     | true  ->
         match funcName  with
@@ -189,7 +189,7 @@ let _createAcnEncDecFunction (r:Asn1AcnAst.AstRoot) (lm:LanguageMacros) (t:Asn1A
                                                 }
                 joinItems (content.orElse "") sNestedContent
 
-            match hasAcnEncodeFunction encFunc t.acnParameters with
+            match hasAcnEncodeFunction encFunc t.acnParameters t.id.tasInfo with
             | true  ->
                 let sNestedStatements =
                     let rec printStatements statements : string option =
@@ -484,4 +484,3 @@ let BitStringAutomaticTestCaseValues (r:Asn1AcnAst.AstRoot)  (t:Asn1AcnAst.Asn1T
                 let s2 = System.String('0', int o.maxSize.uper)
                 [s1;s2]
     | _     -> valsFromSingleValueConstraints
-

BackendAst/GenerateAcnIcd.fs

@@ -64,14 +64,15 @@ let PrintAcnAsHTML stgFileName (r:AstRoot)  =
             icd_acn.EmitFilePart2  stgFileName (Path.GetFileName fName) (content |> Seq.StrJoin "")
     )
 
-let PrintAcnAsHTML2 stgFileName (r:AstRoot)  =
+let PrintAcnAsHTML2 stgFileName (r:AstRoot)  (icdHashesToPrint:string list) =
+    let icdHashesToPrintSet = icdHashesToPrint |> Set.ofList
     let fileTypeAssignments =
         r.icdHashes.Values |>
         Seq.collect id |>
         Seq.choose(fun z ->
             match z.tasInfo with
-            | None -> None
-            | Some ts -> Some (ts.tasName, z.hash)) |>
+            | Some ts when icdHashesToPrintSet.Contains z.hash  -> Some (ts.tasName, z.hash)
+            | _ -> None) |>
         Map.ofSeq
 
     let colorize (t: IToken) =
@@ -81,7 +82,7 @@ let PrintAcnAsHTML2 stgFileName (r:AstRoot)  =
             let safeText = t.Text.Replace("<",lt).Replace(">",gt)
             let uid =
                 match fileTypeAssignments.TryFind t.Text with
-                |Some hash -> icd_acn.TasName stgFileName safeText hash
+                |Some hash (*when icdHashesToPrintSet.Contains hash*) -> icd_acn.TasName stgFileName safeText hash
                 |None -> safeText
             let colored =
                 match t.Type with
@@ -627,7 +628,8 @@ let emitTas2 stgFileName (r:AstRoot) myParams (icdTas:IcdTypeAss)  =
     let sCommentLine = icdTas.hash::icdTas.comments |> Seq.StrJoin (icd_uper.NewLine stgFileName ())
     let arRows =
         icdTas.rows |> List.mapi (fun i rw -> emitIcdRow stgFileName r (i+1) rw)
-    icd_acn.EmitSequenceOrChoice stgFileName false icdTas.name icdTas.hash false (icdTas.kind) (icdTas.minLengthInBytes.ToString()) (icdTas.maxLengthInBytes.ToString()) "sMaxBitsExplained" sCommentLine arRows (myParams 4I) (sCommentLine.Split [|'\n'|])
+    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 rec PrintType2 stgFileName (r:AstRoot)  acnParams (icdTas:IcdTypeAss): string list =
@@ -690,20 +692,42 @@ let PrintTasses2 stgFileName (r:AstRoot) : string list =
         | None -> None) |>
     Seq.toList
 
-
-
-let PrintAsn1FileInColorizedHtml (stgFileName:string) (r:AstRoot) (f:Asn1File) =
+let printTasses3 stgFileName (r:DAst.AstRoot) : (string list)*(string list) =
+    let pdus = r.args.icdPdus |> Option.map Set.ofList
+    let icdHashesToPrint =
+        seq {
+            for f in r.Files do
+                for m in f.Modules do
+                    for tas in m.TypeAssignments do
+                        match pdus.IsNone || pdus.Value.Contains tas.Name.Value with
+                        | true  -> 
+                            match tas.Type.icdTas with
+                            | Some icdTas -> 
+                                let icdTassesHash = getMySelfAndChildren r icdTas
+                                yield! icdTassesHash
+                            | None -> ()
+                        | false -> ()
+        } |> Seq.distinct |> Seq.toList
+    let files =
+        icdHashesToPrint
+        |> Seq.choose(fun hash ->
+            match r.icdHashes.TryFind hash with
+            | Some chIcdTas -> Some (emitTas2 stgFileName r (fun _ -> []) (selectTypeWithSameHash chIcdTas))
+            | None -> None) |> Seq.toList
+    (files, icdHashesToPrint)
+
+let PrintAsn1FileInColorizedHtml (stgFileName:string) (r:AstRoot) (icdHashesToPrint:string list) (f:Asn1File) =
     //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 fileModules.Contains ts.modName -> Some (ts.tasName, z.hash)
-            | Some _ -> None ) |>
-        Map.ofSeq
+            | Some ts when icdHashesToPrintSet.Contains z.hash &&  fileModules.Contains ts.modName -> Some (ts.tasName, z.hash)
+            | Some _ -> None ) |> Seq.toList
 
 
     //let blueTasses = f.Modules |> Seq.collect(fun m -> getModuleBlueTasses m)
@@ -744,13 +768,20 @@ let PrintAsn1FileInColorizedHtml (stgFileName:string) (r:AstRoot) (f:Asn1File) =
                 |Some(tok) -> tok
                 |None -> if idx = 0 then t else f.Tokens.[idx-1]
             let uid =
-                match fileTypeAssignments.TryFind t.Text with
-                |Some tasHash ->
+                //match fileTypeAssignments.TryFind t.Text with
+                match fileTypeAssignments |> List.filter(fun (tasName,_) -> tasName = t.Text) 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
-                |None -> safeText
+                | _ ->
+                    //printfn "Warning: %s is not unique" t.Text
+                    //printfn "Warning: %A" (fileTypeAssignments |> List.filter(fun (tasName,_) -> tasName = t.Text))
+                    safeText
+                //|None -> safeText
             let colored =
                 match t.Type with
                 |asn1Lexer.StringLiteral
@@ -769,14 +800,14 @@ let PrintAsn1FileInColorizedHtml (stgFileName:string) (r:AstRoot) (f:Asn1File) =
 
 let DoWork (r:AstRoot) (deps:Asn1AcnAst.AcnInsertedFieldDependencies) (stgFileName:string) (asn1HtmlStgFileMacros:string option)   outFileName =
     let files1 = r.Files |> Seq.map (fun f -> PrintTasses stgFileName f r )
-    let files1b = PrintTasses2 stgFileName r
+    let (files1b, icdHashesToPrint) = printTasses3 stgFileName r
     let bAcnParamsMustBeExplained = true
     let asn1HtmlMacros =
         match asn1HtmlStgFileMacros with
         | None  -> stgFileName
         | Some x -> x
-    let files2 = r.Files |> Seq.map (PrintAsn1FileInColorizedHtml asn1HtmlMacros r)
-    let files3 = PrintAcnAsHTML2 stgFileName r
+    let files2 = r.Files |> Seq.map (PrintAsn1FileInColorizedHtml asn1HtmlMacros r icdHashesToPrint)
+    let files3 = PrintAcnAsHTML2 stgFileName r icdHashesToPrint
     let cssFileName = Path.ChangeExtension(outFileName, ".css")
     let htmlContent = icd_acn.RootHtml stgFileName files1 files2 bAcnParamsMustBeExplained files3 (Path.GetFileName(cssFileName))
     let htmlContentb = icd_acn.RootHtml stgFileName files1b files2 bAcnParamsMustBeExplained files3 (Path.GetFileName(cssFileName))