<commit_before>﻿using System;
using System.Collections.Generic;
using System.Collections;
using System.Linq;
using System.Text;
using System.Text.RegularExpressions;
using System.IO;
using System.Diagnostics;
using Microsoft.Boogie;
using Microsoft.Boogie.VCExprAST;
using VC;
using Microsoft.Basetypes;
using BType = Microsoft.Boogie.Type;


namespace CfiVerifier
{
    class CfiVerifierMain
    {
        static void Main(string[] args)
        {
            /* Command line parsing */
            if (!Options.ParseCommandLine(String.Join(" ", args))) return;

            foreach (var f in CommandLineOptions.Clo.Files.Where(x => x != ""))
            {
                Console.WriteLine("Processing file {0}", f);

                Program prog; Implementation impl;

                try
                {
                    if (!Utils.ParseProgram(f, out prog)) return;
                    impl = prog.TopLevelDeclarations.Where(x => x is Implementation &&
                        ((Implementation)x).Name.Contains("dll_func")).ElementAt(0) as Implementation;
                    Utils.Assert(impl != null, "Unable to find Boogie implementation named \"dll_func\"");

                    //Phase 0
                    (new Validator()).Visit(prog);

                    //Phase 1
                    Dictionary<Tuple<string, Cmd, AssertCmd>, bool> storeDB = null, loadDB = null;
                    if (Options.optimizeStoreITE) {
                        storeDB = DecideAddressRegions(prog, impl, true);
                    }

                    if (Options.optimizeLoadITE) {
                        loadDB = DecideAddressRegions(prog, impl, false);
                    }

                    //Phase 2
                    InstrumentEnclave(prog, impl, storeDB, loadDB);
                }
                catch (Exception e)
                {
                    Console.WriteLine("CfiVerifier terminated with an exception {0}", e);
                }
            }
        }

        private static Dictionary<Tuple<string, Cmd, AssertCmd>, bool> DecideAddressRegions(Program prog, Implementation impl, bool store)
        {
            Dictionary<Tuple<string, Cmd, AssertCmd>, bool> addressRegionDB;
            bool old_option = Options.splitMemoryModel;
            Options.splitMemoryModel = false;

            (new SpecialInstructionLifter()).Visit(prog);
            (new ModularVerificationSetup()).Visit(prog);
            (new EnvironmentSetup()).Visit(prog);
<commit_msg>bug fix: need to reparse the program after each phase of cfiverifier<commit_after>﻿using System;
using System.Collections.Generic;
using System.Collections;
using System.Linq;
using System.Text;
using System.Text.RegularExpressions;
using System.IO;
using System.Diagnostics;
using Microsoft.Boogie;
using Microsoft.Boogie.VCExprAST;
using VC;
using Microsoft.Basetypes;
using BType = Microsoft.Boogie.Type;


namespace CfiVerifier
{
    class CfiVerifierMain
    {
        static void ExtractProgAndImpl(string fname, out Program prog, out Implementation impl)
        {
            if (!Utils.ParseProgram(fname, out prog)) {
                Utils.Assert(false, "Unable to parse file " + fname);
            }
            
            impl = prog.TopLevelDeclarations.Where(x => x is Implementation &&
                ((Implementation)x).Name.Contains("dll_func")).ElementAt(0) as Implementation;

            Utils.Assert(impl != null, "Unable to find Boogie implementation named \"dll_func\"");

        }

        static void Main(string[] args)
        {
            /* Command line parsing */
            if (!Options.ParseCommandLine(String.Join(" ", args))) return;

            foreach (var f in CommandLineOptions.Clo.Files.Where(x => x != ""))
            {
                Console.WriteLine("Processing file {0}", f);

                Program prog; Implementation impl;

                try
                {
                    // NOTE: Below, we have to reextract prog and impl because we want to purge the instrumentation from the previous phase
                    //Phase 0
                    ExtractProgAndImpl(f, out prog, out impl);
                    (new Validator()).Visit(prog);

                    //Phase 1
                    Dictionary<Tuple<string, Cmd, AssertCmd>, bool> storeDB = null, loadDB = null;
                    if (Options.optimizeStoreITE) 
                    {
                        ExtractProgAndImpl(f, out prog, out impl);
                        storeDB = DecideAddressRegions(prog, impl, true);
                    }

                    if (Options.optimizeLoadITE) 
                    {
                        ExtractProgAndImpl(f, out prog, out impl);
                        loadDB = DecideAddressRegions(prog, impl, false);
                    }

                    //Phase 2
                    ExtractProgAndImpl(f, out prog, out impl);
                    InstrumentEnclave(prog, impl, storeDB, loadDB);
                }
                catch (Exception e)
                {
                    Console.WriteLine("CfiVerifier terminated with an exception {0}", e);
                }
            }
        }

        private static Dictionary<Tuple<string, Cmd, AssertCmd>, bool> DecideAddressRegions(Program prog, Implementation impl, bool store)
        {
            Dictionary<Tuple<string, Cmd, AssertCmd>, bool> addressRegionDB;
            bool old_option = Options.splitMemoryModel;
            Options.splitMemoryModel = false;

            (new SpecialInstructionLifter()).Visit(prog);
            (new ModularVerificationSetup()).Visit(prog);
            (new EnvironmentSetup()).Visit(prog);

{'fraction_non_alphanumeric': 0.09395973154362416, 'fraction_numerical': 0.0021193924408336277, 'mean_word_length': 1.7490291262135922, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 19, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3188926', 'n_tokens_mistral': 1507, 'n_tokens_neox': 1364, 'n_words': 364}