public void Generate()

in Sources/SolToBoogie/RevertLogicGenerator.cs [271:439]
125 lines of code
25 McCabe index (conditional complexity)

        public void Generate()
        {
            // Collect Global Variables.
            HashSet<BoogieGlobalVariable> globals = new HashSet<BoogieGlobalVariable>();
            foreach (var decl in context.Program.Declarations)
            {
                if (decl is BoogieGlobalVariable)
                {
                    var g = (BoogieGlobalVariable)decl;
                    
                    if (mustHaveShadow(g.Name)) 
                        globals.Add(g);
                }
            }
            
            // Generate shadow state.
            foreach (var g in globals)
            {
                var varName = g.TypedIdent.Name;
                BoogieTypedIdent shadowGlobal = new BoogieTypedIdent("__tmp__" + varName, g.TypedIdent.Type);
                BoogieGlobalVariable shadowGlobalDecl = new BoogieGlobalVariable(shadowGlobal);
                
                context.Program.AddDeclaration(shadowGlobalDecl);
                shadowGlobals.Add(varName, shadowGlobalDecl);
            }
            
            // Duplicate and rename methods.
            Dictionary<string, BoogieImplementation> proceduresWithImpl = new Dictionary<string, BoogieImplementation>();
            procsWiltImplNames = proceduresWithImpl.Keys;
            foreach (var decl in context.Program.Declarations)
            {
                if (decl is BoogieImplementation)
                {
                    var boogieImpl = ((BoogieImplementation) decl);
                    if (proceduresInProgram.ContainsKey(boogieImpl.Name))
                    {
                        proceduresWithImpl.Add(boogieImpl.Name, boogieImpl);
                    }
                }
            }

            Dictionary<string, BoogieProcedure> failProcedures = new Dictionary<string, BoogieProcedure>();
            foreach (var implPair in proceduresWithImpl)
            {
                BoogieProcedure proc = proceduresInProgram[implPair.Key];

                if (isPublic(proc) || isConstructor(proc.Name))
                {
                    // If public maintain original definition as the wrapper.
                    BoogieProcedure successVersion = duplicateProcedure(proc, "success", true);
                    //BoogieImplementation successImpl = duplicateImplementation(implPair.Value, "success");
                    
                    context.Program.AddDeclaration(successVersion);
                    //context.Program.AddDeclaration(successImpl);
                    
                    BoogieProcedure failVersion = duplicateProcedure(proc, "fail", true);
                    
                    context.Program.AddDeclaration(failVersion);
                    
                    // Use original name of the procedure.
                    failProcedures.Add(implPair.Key, failVersion);
                }
                else if (!isHarnessProcudure(proc.Name))
                {
                    // Otherwise reuse original definition/impl as the "successful" method.
                    BoogieProcedure failVersion = duplicateProcedure(proc, "fail");
                    
                    context.Program.AddDeclaration(failVersion);

                    // Use original name of the procedure.
                    failProcedures.Add(implPair.Key, failVersion);
                    
                    // Reuse original node
                    proc.Name = proc.Name + "__success";
                    implPair.Value.Name = implPair.Value.Name + "__success";
                }
            }

            // Create implementations for failing methods.
            foreach (var failProcedurePair in failProcedures)
            {
                string originalProcName = failProcedurePair.Key;
                BoogieProcedure proc = failProcedurePair.Value;

                var originalImpl = proceduresWithImpl[originalProcName];
                if (!originalProcName.Equals("send"))
                {
                    context.Program.AddDeclaration(createFailImplementation(proc.Name, originalImpl));
                    context.Program.AddDeclaration(createSuccessImplementation(originalProcName + "__success", originalImpl));
                }
                else
                {
                    context.Program.AddDeclaration(CreateSendFail());
                    context.Program.AddDeclaration(CreateSendSucess());
                }

                // Remove original implementation for non-public methods
                if (!isPublic(proceduresInProgram[originalProcName]) && !isConstructor(originalProcName))
                {
                    context.Program.Declarations.Remove(originalImpl);
                }
            }

            foreach (var implPair in proceduresWithImpl)
            {
                // Update non-public methods in harness methods
                if (isHarnessProcudure(implPair.Key))
                {
                    context.Program.AddDeclaration(createSuccessImplementation(implPair.Key, implPair.Value));

                    context.Program.Declarations.Remove(implPair.Value);
                }
            }

            // Create wrappers for public methods.

            foreach (var proc in proceduresInProgram.Values)
            {
                if (proceduresWithImpl.ContainsKey(proc.Name) && (isPublic(proc) || isConstructor(proc.Name)))
                {
                    BoogieImplementation impl = proceduresWithImpl[proc.Name];
                    impl.StructuredStmts = new BoogieStmtList();
                    impl.LocalVars = new List<BoogieVariable>();

                    var exceptionVarName = "__exception";
                    var revertGlobalName = "revert";
                    impl.LocalVars.Add(new BoogieLocalVariable(new BoogieTypedIdent(exceptionVarName, BoogieType.Bool)));

                    var stmtList = impl.StructuredStmts;
                    stmtList.AddStatement(new BoogieHavocCmd(new BoogieIdentifierExpr(exceptionVarName)));
                    stmtList.AddStatement(new BoogieAssignCmd(new BoogieIdentifierExpr(revertGlobalName), new BoogieLiteralExpr(false)));
                    
                    // Call Successful version.
                    BoogieStmtList successCallStmtList = new BoogieStmtList();
                    successCallStmtList.AddStatement(new BoogieCallCmd(impl.Name + "__success", 
                                                                       impl.InParams.Select(inParam => (BoogieExpr)new BoogieIdentifierExpr(inParam.Name)).ToList(), 
                                                                       impl.OutParams.Select(outParam => new BoogieIdentifierExpr(outParam.Name)).ToList()));
                    BoogieExpr successAssumePred = new BoogieUnaryOperation(BoogieUnaryOperation.Opcode.NOT, new BoogieIdentifierExpr(revertGlobalName));

                    if (context.TranslateFlags.InstrumentGas)
                    {
                        successAssumePred = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.AND, successAssumePred, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.GE, new BoogieIdentifierExpr("gas"), new BoogieLiteralExpr(0)));
                    }
                    successCallStmtList.AddStatement(new BoogieAssumeCmd(successAssumePred));
                    
                    // Call fail version.
                    BoogieStmtList failCallStmtList = new BoogieStmtList();
                    // Write global variables to temps
                    foreach (var shadowGlobalPair in shadowGlobals)
                    {
                        string origVarName = shadowGlobalPair.Key;
                        string shadowName = shadowGlobalPair.Value.Name;
                        failCallStmtList.AddStatement(new BoogieAssignCmd(new BoogieIdentifierExpr(shadowName), new BoogieIdentifierExpr(origVarName)));
                    }
                    failCallStmtList.AddStatement(new BoogieCallCmd(impl.Name + "__fail", 
                                                 impl.InParams.Select(inParam => (BoogieExpr)new BoogieIdentifierExpr(inParam.Name)).ToList(), 
                                                impl.OutParams.Select(outParam => new BoogieIdentifierExpr(outParam.Name)).ToList()));
                    BoogieExpr failAssumePred = new BoogieIdentifierExpr(revertGlobalName);

                    if (context.TranslateFlags.InstrumentGas)
                    {
                        failAssumePred = new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.OR, failAssumePred, new BoogieBinaryOperation(BoogieBinaryOperation.Opcode.LT, new BoogieIdentifierExpr("gas"), new BoogieLiteralExpr(0)));
                    }
                    failCallStmtList.AddStatement(new BoogieAssumeCmd(failAssumePred));
                    
                    stmtList.AddStatement(new BoogieIfCmd(new BoogieIdentifierExpr(exceptionVarName), failCallStmtList, successCallStmtList));
                }
            }
        }