<commit_before>﻿//===-----------------------------------------------------------------------==//
//
//                Lockpwn - a Static Lockset Analyser for Boogie
//
// Copyright (c) 2015 <NAME> (<EMAIL>)
//
// This file is distributed under the MIT License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//

using System;
using System.IO;
using System.Collections.Generic;
using System.Diagnostics.Contracts;

using Microsoft.Boogie;
using System.Diagnostics;

namespace Lockpwn
{
  internal class Program
  {
    internal static void Main(string[] args)
    {
      Contract.Requires(cce.NonNullElements(args));
      CommandLineOptions.Install(new ToolCommandLineOptions());

      Program.EnableBoogieOptions();

      var fileList = new List<string>();

      try
      {
        ToolCommandLineOptions.Get().RunningBoogieFromCommandLine = true;
        ToolCommandLineOptions.Get().PrintUnstructured = 2;

        if (!ToolCommandLineOptions.Get().Parse(args))
        {
          Environment.Exit((int)Outcome.FatalError);
        }

        if (ToolCommandLineOptions.Get().Files.Count == 0)
        {
          Lockpwn.IO.Reporter.ErrorWriteLine("lockpwn: error: no input files were specified");
          Environment.Exit((int)Outcome.FatalError);
        }

        foreach (string file in ToolCommandLineOptions.Get().Files)
        {
          string extension = Path.GetExtension(file);
          if (extension != null)
          {
            extension = extension.ToLower();
          }
          fileList.Add(file);
        }

        foreach (string file in fileList)
        {
          Contract.Assert(file != null);
          string extension = Path.GetExtension(file);
          if (extension != null)
          {
            extension = extension.ToLower();
          }
          if (extension != ".bpl")
          {
            Lockpwn.IO.Reporter.ErrorWriteLine("lockpwn: error: {0} is not a .bpl file", file);
            Environment.Exit((int)Outcome.FatalError);
          }
        }

        if (ToolCommandLineOptions.Get().NoInstrumentation)
        {
          Program.CheckAndSpitProgram(fileList);
        }

        var ac = new ParsingEngine(fileList).Run();

        new ThreadAnalysisEngine(ac).Run();
        new LocksetInstrumentationEngine(ac).Run();

        AnalysisContext postAc = null;
        new AnalysisContextParser(fileList[fileList.Count - 1], "bpl").TryParseNew(ref ac,
          new List<string> { "instrumented" });
        new AnalysisContextParser(fileList[fileList.Count - 1], "bpl").TryParseNew(ref postAc,
          new List<string> { "instrumented" });
        new Cruncher(ac, postAc).Run();

        new AnalysisContextParser(fileList[fileList.Count - 1], "bpl").TryParseNew(ref ac,
          new List<string> { "summarised" });
        new AnalysisContextParser(fileList[fileList.Count - 1], "bpl").TryParseNew(ref postAc);
        new StaticLocksetAnalyser(ac, postAc).Run();

        if (ToolCommandLineOptions.Get().VerboseMode)
          Console.WriteLine(". Done");

        Environment.Exit((int)Outcome.Done);
      }
      catch (Exception e)
      {
        Console.Error.Write("Exception thrown in lockpwn: ");
        Console.Error.WriteLine(e);
        Environment.Exit((int)Outcome.FatalError);
      }
    }

    internal static void EnableBoogieOptions()
    {
      CommandLineOptions.Clo.DoModSetAnalysis = true;
      CommandLineOptions.Clo.DontShowLogo = true;
      CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
      CommandLineOptions.Clo.ModelViewFile = "-";
      CommandLineOptions.Clo.UseLabels = false;
      CommandLineOptions.Clo.EnhancedErrorMessages = 1;
      CommandLineOptions.Clo.ContractInfer = true;
    }

    internal static void CheckAndSpitProgram(List<string> fileList)
    {
      AnalysisContext ac = null;
      AnalysisContext postAc = null;
      new AnalysisContextParser(fileList[fileList.Count - 1], "bpl").TryParseNew(ref ac,
        new List<string> { "instrumented" });
      new AnalysisContextParser(fileList[fileList.Count - 1], "bpl").TryParseNew(ref postAc);
      new StaticLocksetAnalyser(ac, postAc).Run();

      if (ToolCommandLineOptions.Get().VerboseMode)
        Console.WriteLine(". Done");

      Environment.Exit((int)Outcome.Done);
    }
  }
}<commit_msg>the error reporter is now properly shared between the analysis contexts<commit_after>﻿//===-----------------------------------------------------------------------==//
//
//                Lockpwn - a Static Lockset Analyser for Boogie
//
// Copyright (c) 2015 <NAME> (<EMAIL>)
//
// This file is distributed under the MIT License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//

using System;
using System.IO;
using System.Collections.Generic;
using System.Diagnostics.Contracts;

using Microsoft.Boogie;
using System.Diagnostics;

namespace Lockpwn
{
  internal class Program
  {
    internal static void Main(string[] args)
    {
      Contract.Requires(cce.NonNullElements(args));
      CommandLineOptions.Install(new ToolCommandLineOptions());

      Program.EnableBoogieOptions();

      var fileList = new List<string>();

      try
      {
        ToolCommandLineOptions.Get().RunningBoogieFromCommandLine = true;
        ToolCommandLineOptions.Get().PrintUnstructured = 2;

        if (!ToolCommandLineOptions.Get().Parse(args))
        {
          Environment.Exit((int)Outcome.FatalError);
        }

        if (ToolCommandLineOptions.Get().Files.Count == 0)
        {
          Lockpwn.IO.Reporter.ErrorWriteLine("lockpwn: error: no input files were specified");
          Environment.Exit((int)Outcome.FatalError);
        }

        foreach (string file in ToolCommandLineOptions.Get().Files)
        {
          string extension = Path.GetExtension(file);
          if (extension != null)
          {
            extension = extension.ToLower();
          }
          fileList.Add(file);
        }

        foreach (string file in fileList)
        {
          Contract.Assert(file != null);
          string extension = Path.GetExtension(file);
          if (extension != null)
          {
            extension = extension.ToLower();
          }
          if (extension != ".bpl")
          {
            Lockpwn.IO.Reporter.ErrorWriteLine("lockpwn: error: {0} is not a .bpl file", file);
            Environment.Exit((int)Outcome.FatalError);
          }
        }

        if (ToolCommandLineOptions.Get().NoInstrumentation)
        {
          Program.CheckAndSpitProgram(fileList);
        }

        var ac = new ParsingEngine(fileList).Run();

        new ThreadAnalysisEngine(ac).Run();
        new LocksetInstrumentationEngine(ac).Run();

        AnalysisContext postAc = null;
        new AnalysisContextParser(fileList[fileList.Count - 1], "bpl").TryParseNew(ref ac,
          new List<string> { "instrumented" });
        new AnalysisContextParser(fileList[fileList.Count - 1], "bpl").TryParseNew(ref postAc,
          new List<string> { "instrumented" });
        postAc.ErrorReporter = ac.ErrorReporter;

        new Cruncher(ac, postAc).Run();

        new AnalysisContextParser(fileList[fileList.Count - 1], "bpl").TryParseNew(ref ac,
          new List<string> { "summarised" });
        new AnalysisContextParser(fileList[fileList.Count - 1], "bpl").TryParseNew(ref postAc);
        postAc.ErrorReporter = ac.ErrorReporter;

        new StaticLocksetAnalyser(ac, postAc).Run();

        if (ToolCommandLineOptions.Get().VerboseMode)
          Console.WriteLine(". Done");

        Environment.Exit((int)Outcome.Done);
      }
      catch (Exception e)
      {
        Console.Error.Write("Exception thrown in lockpwn: ");
        Console.Error.WriteLine(e);
        Environment.Exit((int)Outcome.FatalError);
      }
    }

    internal static void EnableBoogieOptions()
    {
      CommandLineOptions.Clo.DoModSetAnalysis = true;
      CommandLineOptions.Clo.DontShowLogo = true;
      CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
      CommandLineOptions.Clo.ModelViewFile = "-";
      CommandLineOptions.Clo.UseLabels = false;
      CommandLineOptions.Clo.EnhancedErrorMessages = 1;
      CommandLineOptions.Clo.ContractInfer = true;
    }

    internal static void CheckAndSpitProgram(List<string> fileList)
    {
      AnalysisContext ac = null;
      AnalysisContext postAc = null;
      new AnalysisContextParser(fileList[fileList.Count - 1], "bpl").TryParseNew(ref ac,
        new List<string> { "instrumented" });
      new AnalysisContextParser(fileList[fileList.Count - 1], "bpl").TryParseNew(ref postAc);
      postAc.ErrorReporter = ac.ErrorReporter;

      new StaticLocksetAnalyser(ac, postAc).Run();

      if (ToolCommandLineOptions.Get().VerboseMode)
        Console.WriteLine(". Done");

      Environment.Exit((int)Outcome.Done);
    }
  }
}
{'fraction_non_alphanumeric': 0.1459351399378054, 'fraction_numerical': 0.003109729009329187, 'mean_word_length': 2.3265607683782785, 'pattern_counts': {'":': 0, '<': 19, '<?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': '6678758', 'n_tokens_mistral': 2550, 'n_tokens_neox': 2472, 'n_words': 472}