private void TranslateTypeCast()

in Sources/SolToBoogie/ProcedureTranslator.cs [3378:3471]
76 lines of code
17 McCabe index (conditional complexity)

        private void TranslateTypeCast(FunctionCall node, BoogieExpr lhs, out bool isElemenentaryTypeCast)
        {
            isElemenentaryTypeCast = false; 

            VeriSolAssert(node.Kind.Equals("typeConversion"));
            VeriSolAssert(node.Arguments.Count == 1);
            //VeriSolAssert(node.Arguments[0] is Identifier || node.Arguments[0] is MemberAccess || node.Arguments[0] is Literal || node.Arguments[0] is IndexAccess,
            //    "Argument to a typecast has to be an identifier, memberAccess, indexAccess or Literal");

            // target: lhs := T(expr);
            BoogieExpr exprToCast = TranslateExpr(node.Arguments[0]);

            if (node.Expression is Identifier) // cast to user defined types
            {
                Identifier contractId = node.Expression as Identifier;
                ContractDefinition contract = context.GetASTNodeById(contractId.ReferencedDeclaration) as ContractDefinition;
                VeriSolAssert(contract != null);

                // assume (DType[var] == T);
                List<ContractDefinition> subtypes = new List<ContractDefinition>(context.GetSubTypesOfContract(contract));
                Debug.Assert(subtypes.Count > 0);

                BoogieExpr dtype = new BoogieMapSelect(new BoogieIdentifierExpr("DType"), exprToCast);
                BoogieExpr guard = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, dtype,
                    new BoogieIdentifierExpr(subtypes[0].Name));

                for (int i = 1; i < subtypes.Count; ++i)
                {
                    BoogieExpr subGuard = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.EQ, dtype, new BoogieIdentifierExpr(subtypes[i].Name));
                    guard = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.OR, guard, subGuard);
                }
                
                currentStmtList.AddStatement(new BoogieAssumeCmd(guard));
                // lhs := expr;
                currentStmtList.AddStatement(new BoogieAssignCmd(lhs, exprToCast));
            }
            else if (node.Expression is ElementaryTypeNameExpression elemType) // cast to elementary types
            {
                isElemenentaryTypeCast = true;
                BoogieExpr rhsExpr = exprToCast;
                // most casts are skips, except address and int cast
                if (elemType.TypeName.Equals("address") || elemType.TypeName.Equals("address payable"))
                {

                    // skip by default, unless we have an integer/hex constant
                    if (exprToCast is BoogieLiteralExpr blit)
                    {
                        if (blit.ToString().Equals("0"))
                        {
                            rhsExpr = (BoogieExpr)new BoogieIdentifierExpr("null");
                        }
                        else
                        {
                            rhsExpr = new BoogieFuncCallExpr("ConstantToRef", new List<BoogieExpr>() { exprToCast });
                        }
                    } else if (node.Arguments[0].TypeDescriptions.IsInt() || node.Arguments[0].TypeDescriptions.IsUint())
                    {
                        rhsExpr = new BoogieFuncCallExpr("ConstantToRef", new List<BoogieExpr>() { exprToCast });
                    }
                }
                var castToInt = Regex.Match(elemType.TypeName, @"[int,uint]\d*").Success;

                if (castToInt && node.Arguments[0].TypeDescriptions.IsAddress())
                {
                    // uint addrInt = uint(addr);
                    // for any other type conversion, make it uninterpreted 
                    rhsExpr = new BoogieFuncCallExpr("BoogieRefToInt", new List<BoogieExpr>() { exprToCast });
                }

                // We do not handle downcasts between unsigned integers, when /useModularArithmetic option is enabled:
                if (context.TranslateFlags.UseModularArithmetic)
                {
                    bool argTypeIsUint = node.Arguments[0].TypeDescriptions.IsUintWSize(node.Arguments[0], out uint argSz);
                    if (argTypeIsUint && elemType.ToString().StartsWith("uint"))
                    {
                        uint castSz = uint.Parse(Extensions.GetNumberFromEnd(elemType.ToString()));
                        if (argSz > castSz)
                        {
                            Console.WriteLine($"Warning: downcasts are not handled with /useModularArithmetic option");
                        }
                    }
                }
                
                // lets update currentExpr with rhsExpr. The caller may update it with the temporary
                currentExpr = rhsExpr; 
                // lhs := expr;
                currentStmtList.AddStatement(new BoogieAssignCmd(lhs, rhsExpr));
            } 
            else
            {
                VeriSolAssert(false, $"Unknown type cast: {node.Expression}");
            }
            return;
        }