--[[
This is the main S2E configuration file
=======================================

This file was automatically generated by s2e-env at 2019-04-25 18:03:09.909337

Changes can be made by the user where appropriate.
]]--

-------------------------------------------------------------------------------
-- This section configures the S2E engine.
s2e = {
    logging = {
        -- Possible values include "all", "debug", "info", "warn" and "none".
        -- See Logging.h in libs2ecore.
        console = "debug",
        logLevel = "debug",
    },

    -- All the cl::opt options defined in the engine can be tweaked here.
    -- This can be left empty most of the time.
    -- Most of the options can be found in S2EExecutor.cpp and Executor.cpp.
    kleeArgs = {
        "--use-query-log=solver:kquery",
        "--use-end-query-pc-log",
        "--flush-tbs-on-state-switch=false",
        "--state-shared-memory=true",
        "--use-concolic-execution=true",
        "--use-dfs-search=false",
        --verbose-fork-info",
        --debug-log-state-merge=true",
    },
}

-- Declare empty plugin settings. They will be populated in the rest of
-- the configuration file.
plugins = {}
pluginsConfig = {}

-- Include various convenient functions
dofile('library.lua')

-------------------------------------------------------------------------------
-- This plugin contains the core custom instructions.
-- Some of these include s2e_make_symbolic, s2e_kill_state, etc.
-- You always want to have this plugin included.

add_plugin("BaseInstructions")

-------------------------------------------------------------------------------
-- This plugin implements "shared folders" between the host and the guest.
-- Use it in conjunction with s2eget and s2eput guest tools in order to
-- transfer files between the guest and the host.

add_plugin("HostFiles")
pluginsConfig.HostFiles = {
    baseDirs = {
        "/data/home/alan/Work/s2e/s2e/projects/tcp",

    },
    allowWrite = true,
}

-------------------------------------------------------------------------------
-- This plugin provides support for virtual machine introspection and binary
-- formats parsing. S2E plugins can use it when they need to extract
-- information from binary files that are either loaded in virtual memory
-- or stored on the host's file system.

add_plugin("Vmi")
pluginsConfig.Vmi = {
    baseDirs = {
        "/data/home/alan/Work/s2e/s2e/projects/tcp", "/data/home/alan/Work/s2e/s2e/projects/tcp/guest-tools",

        "/data/home/alan/Work/s2e/s2e/images/debian-9.2.1-x86_64/guestfs"

    },
}

-------------------------------------------------------------------------------
-- This plugin provides various utilities to read from process memory.
-- In case it is not possible to read from guest memory, the plugin tries
-- to read static data from binary files stored in guestfs.
add_plugin("MemUtils")

-------------------------------------------------------------------------------
-- This plugin collects various execution statistics and sends them to a QMP
-- server that listens on an address:port configured by the S2E_QMP_SERVER
-- environment variable.
--
-- The "s2e run None" command sets up such a server in order to display
-- stats on the dashboard.
--
-- You may also want to use this plugin to integrate S2E into a larger
-- system. The server could collect information about execution from different
-- S2E instances, filter them, and store them in a database.

add_plugin("WebServiceInterface")
pluginsConfig.WebServiceInterface = {
    statsUpdateInterval = 2
}

-------------------------------------------------------------------------------
-- This is the main execution tracing plugin.
-- It generates the ExecutionTracer.dat file in the s2e-last folder.
-- That files contains trace information in a binary format. Other plugins can
-- hook into ExecutionTracer in order to insert custom tracing data.
--
-- This is a core plugin, you most likely always want to have it.

add_plugin("ExecutionTracer")

-------------------------------------------------------------------------------
-- This plugin records events about module loads/unloads and stores them
-- in ExecutionTracer.dat.
-- This is useful in order to map raw program counters and pids to actual
-- module names.

add_plugin("ModuleTracer")

-------------------------------------------------------------------------------
-- This is a generic plugin that let other plugins communicate with each other.
-- It is a simple key-value store.
--
-- The plugin has several modes of operation:
--
-- 1. local: runs an internal store private to each instance (default)
-- 2. distributed: the plugin interfaces with an actual key-value store server.
-- This allows different instances of S2E to communicate with each other.

add_plugin("KeyValueStore")

-------------------------------------------------------------------------------
-- Records the program counter of executed translation blocks.
-- Generates a json coverage file. This file can be later processed by other
-- tools to generate line coverage information. Please refer to the S2E
-- documentation for more details.

add_plugin("TranslationBlockCoverage")
pluginsConfig.TranslationBlockCoverage = {
    writeCoverageOnStateKill = true,
    writeCoverageOnStateSwitch = true,
}

-------------------------------------------------------------------------------
-- Tracks execution of specific modules.
-- Analysis plugins are often interested only in small portions of the system,
-- typically the modules under analysis. This plugin filters out all core
-- events that do not concern the modules under analysis. This simplifies
-- code instrumentation.
-- Instead of listing individual modules, you can also track all modules by
-- setting configureAllModules = true

add_plugin("ModuleExecutionDetector")
pluginsConfig.ModuleExecutionDetector = {

    logLevel="info"
}

-------------------------------------------------------------------------------
-- This plugin controls the forking behavior of S2E.

add_plugin("ForkLimiter")
pluginsConfig.ForkLimiter = {
    -- How many times each program counter is allowed to fork.
    -- -1 for unlimited.
    maxForkCount = -1,

    -- How many seconds to wait before allowing an S2E process
    -- to spawn a child. When there are many states, S2E may
    -- spawn itself into multiple processes in order to leverage
    -- multiple cores on the host machine. When an S2E process A spawns
    -- a process B, A and B each get half of the states.
    --
    -- In some cases, when states fork and terminate very rapidly,
    -- one can see flash crowds of S2E instances. This decreases
    -- execution efficiency. This parameter forces S2E to wait a few
    -- seconds so that more states can accumulate in an instance
    -- before spawning a process.
    processForkDelay = 5,
}

-------------------------------------------------------------------------------
-- This plugin tracks execution of processes.
-- This is the preferred way of tracking execution and will eventually replace
-- ModuleExecutionDetector.

add_plugin("ProcessExecutionDetector")
pluginsConfig.ProcessExecutionDetector = {
    moduleNames = {

    },
}

-------------------------------------------------------------------------------
-- Keeps for each state/process an updated map of all the loaded modules.
add_plugin("ModuleMap")


-------------------------------------------------------------------------------
-- Keeps for each process in ProcessExecutionDetector an updated map
-- of memory regions.
add_plugin("MemoryMap")



-------------------------------------------------------------------------------
-- MultiSearcher is a top-level searcher that allows switching between
-- different sub-searchers.
add_plugin("MultiSearcher")

-- CUPA stands for Class-Uniform Path Analysis. It is a searcher that groups
-- states into classes. Each time the searcher needs to pick a state, it first
-- chooses a class, then picks a state in that class. Classes can further be
-- subdivided into subclasses.
--
-- The advantage of CUPA over other searchers is that it gives similar weights
-- to different parts of the program. If one part forks a lot, a random searcher
-- would most likely pick a state from that hotspot, decreasing the probability
-- of choosing another state that may have better chance of covering new code.
-- CUPA avoids this problem by grouping similar states together.

add_plugin("CUPASearcher")
pluginsConfig.CUPASearcher = {
    -- The order of classes is important, please refer to the plugin
    -- source code and documentation for details on how CUPA works.
    classes = {


        -- This ensures that states run for a certain amount of time.
        -- Otherwise too frequent state switching may decrease performance.
        "batch",

        -- Prioritize the states based on target pc.
        "targeted",

        -- A program under test may be composed of several binaries.
        -- We want to give equal chance to all binaries, even if some of them
        -- fork a lot more than others.
        "pagedir",

        -- Finally, group states by program counter at fork.
        "pc",
    },
    logLevel="info",
    enabled = true,

    -- Delay (in seconds) before switching states (when used with the "batch" class).
    -- A very large delay becomes similar to DFS (current state keeps running
    -- until it is terminated).
    batchTime = 5,

--[[
    criticalPcs = {
        --0xffffffff8177d73f,
        --0xffffffff8177d86c,
        --0xffffffff8177d875,
        --0xffffffff8177d883,
        --0xffffffff8177d92a,
        0xffffffff8178fffd,
        0xffffffff81790014,
        0xffffffff8177c66c,
        0xffffffff8178f13c,
        0xffffffff81785467,
        0xffffffff8178546f,
        0xffffffff8178547f,
        0xffffffff8177d6de,
        0xffffffff8177d6f2,
        0xffffffff8177d6f6,
        0xffffffff8177d71f,
        0xffffffff8177d725,
        0xffffffff8177d729,
        0xffffffff8177d72f,
        0xffffffff8177d733,
        0xffffffff8177d73b,
        0xffffffff8177d73f,
        0xffffffff8177d86c,
        0xffffffff8177d6f2,
        0xffffffff8177d6f6,
        0xffffffff8177d71f,
        0xffffffff81780628,

        0xffffffff8178fffd,
        0xffffffff81790014,
        0xffffffff8177c66c,
        0xffffffff817913a5,
        0xffffffff8177d6f2,
        0xffffffff8177d6f6,
        0xffffffff8177d71f,
        0xffffffff8177d725,
        0xffffffff8177d729,
        0xffffffff8177d72f,
        0xffffffff8177d74f,
        0xffffffff8177d755,
        0xffffffff8177d763,
        0xffffffff8177d703,
        0xffffffff8177d6ed,
        0xffffffff8177d6f2,
        0xffffffff8177d6f6,
        0xffffffff8177d71f,
        0xffffffff8177d725,
        0xffffffff8177d729,
        0xffffffff8177d72f,
        0xffffffff8177d74f,
        0xffffffff8177d755,
        0xffffffff8177d7ec,
        0xffffffff8177d7f7,
        0xffffffff8177d6f2,
        0xffffffff8177d6f6,
        0xffffffff8177d71f,
        0xffffffff8177d725,
        0xffffffff8177d729,
        0xffffffff8177d72f,
        0xffffffff8177d733,
        0xffffffff8177d73b,
        0xffffffff8177d73f,
        0xffffffff8177d86c,
        0xffffffff8177d6f2,
        0xffffffff8177d6f6,
        0xffffffff8177d71f,
        0xffffffff81791496,
        0xffffffff817914d0,
        0xffffffff817914d9,
        0xffffffff817914e6,
        0xffffffff818f5436,
    },
--]]
    
    threshold1 = 1000,
    threshold2 = 100000,
}





-------------------------------------------------------------------------------
-- Function models help drastically reduce path explosion. A model is an
-- expression that efficiently encodes the behavior of a function. In imperative
-- languages, functions often have if-then-else branches and loops, which
-- may cause path explosion. A model compresses this into a single large
-- expression. Models are most suitable for side-effect-free functions that
-- fork a lot. Please refer to models.lua and the documentation for more details.

add_plugin("StaticFunctionModels")

pluginsConfig.StaticFunctionModels = {
  modules = {}
}

g_function_models = {}
safe_load('models.lua')
pluginsConfig.StaticFunctionModels.modules = g_function_models


-------------------------------------------------------------------------------
-- This generates test cases when a state crashes or terminates.
-- If symbolic inputs consist of symbolic files, the test case generator writes
-- concrete files in the S2E output folder. These files can be used to
-- demonstrate the crash in a program, added to a test suite, etc.

add_plugin("TestCaseGenerator")
pluginsConfig.TestCaseGenerator = {
    generateOnStateKill = true,
    generateOnSegfault = true
}





-- ========================================================================= --
-- ============== Target-specific configuration begins here. =============== --
-- ========================================================================= --

-------------------------------------------------------------------------------
-- LinuxMonitor is a plugin that monitors Linux events and exposes them
-- to other plugins in a generic way. Events include process load/termination,
-- thread events, signals, etc.
--
-- LinuxMonitor requires a custom Linux kernel with S2E extensions. This kernel
-- (and corresponding VM image) can be built with S2E tools. Please refer to
-- the documentation for more details.

add_plugin("LinuxMonitor")
pluginsConfig.LinuxMonitor = {
    -- Kill the execution state when it encounters a segfault
    terminateOnSegfault = true,

    -- Kill the execution state when it encounters a trap
    terminateOnTrap = true,
}



-- ========================================================================= --
-- ============== User-specific scripts begin here ========================= --
-- ========================================================================= --


-------------------------------------------------------------------------------
-- This plugin exposes core S2E engine functionality to LUA scripts.
-- In particular, it provides the g_s2e global variable, which works similarly
-- to C++ plugins.
-------------------------------------------------------------------------------
add_plugin("LuaBindings")

-------------------------------------------------------------------------------
-- Exposes S2E engine's core event.
-- These are similar to events in CorePlugin.h. Please refer to
-- the LuaCoreEvents.cpp source file for a list of availble events.
-------------------------------------------------------------------------------
add_plugin("LuaCoreEvents")

-- This configuration shows an example that kills states if they fork in
-- a specific module.
-- [[
pluginsConfig.LuaCoreEvents = {
    -- This annotation is called in case of a fork. It should return true
    -- to allow the fork and false to prevent it.
    onStateForkDecide = "onStateForkDecide"
}

function onStateForkDecide(state)
   mmap = g_s2e:getPlugin("ModuleMap")
   mod = mmap:getModule(state)
   if mod ~= nil then
      name = mod:getName()
      if name == "mymodule" then
          state:kill(0, "forked in mymodule")
      end

      if name == "myothermodule" then
          return false
      end
   end
   return true
end
-- ]]


add_plugin("FunctionMonitor")

add_plugin("MemRangeDetector") 
pluginsConfig.MemRangeDetector = {
    net_ipv4 = {
        startAddr = 0xffffffff817659c0,
        endAddr = 0xffffffff8205353b,
        isBlacklist = false,
    },
--[[
    __ip_local_out = {
        startAddr = 0xffffffff81770000,
        endAddr = 0xffffffff817700d9,
        isBlacklist = true,
    },
    tcp_v4_send_ack = {
        startAddr = 0xffffffff8178cf90,
        endAddr = 0xffffffff8178d1ba,
        isBlacklist = true,
    },
    csum_partial_copy_generic = {
        startAddr = 0xffffffff818f5370,
        endAddr = 0xffffffff818f54b5,
        isBlacklist = true,
    },
    tcp_sync_mss = {
        startAddr = 0xffffffff81786f60,
        endAddr = 0xffffffff81787089,
        isBlacklist = true,
    },
    tcp_parse_fastopen_option = {
        startAddr = 0xffffffff8177d5d0,
        endAddr = 0xffffffff8177d690,
        isBlacklist = true,
    },
    tcp_may_update_window_partial = {
        startAddr = 0xffffffff81781d2a,
        endAddr = 0xffffffff81781d4b,
        isBlacklist = true,
    },
    tcp_may_update_window_partial2 = {
        startAddr = 0xffffffff81782a56,
        endAddr = 0xffffffff81782a56,
        isBlacklist = true,
    },
    tcp_ecn_create_request_partial = {
        startAddr = 0xffffffff81780628,
        endAddr = 0xffffffff81780628,
        isBlacklist = true,
    },
    tcp_ecn_accept_cwr_partial = {
        startAddr = 0xffffffff81783d31,
        endAddr = 0xffffffff81783d31,
        isBlacklist = true,
    },
    tcp_ecn_rcv_ecn_echo_partial = {
        startAddr = 0xffffffff81781d9a,
        endAddr = 0xffffffff81781d9a,
        isBlacklist = true,
    },
--]]
}

add_plugin("TCPSymbolizer")
pluginsConfig.TCPSymbolizer = {
    logLevel="debug",
    concretePacketCounter = 0,
    symbolicPacketCounter = 3,
    TCPOptionsLength = 20,
    concolicOptions = true,
    generateBadChecksumCases = true,
}

--add_plugin("TranslationBlockTracer")
--pluginsConfig.TranslationBlockTracer = {
--    manualTrigger = true,
--    flushTbCache = true,
--}

--add_plugin("MemoryTracer")
--pluginsConfig.MemoryTracer = {
--    monitorStack = false,
--    manualTrigger = true,
--    monitorMemory = true,
--    monitorPageFaults = false,
--    monitorTlbMisses = false,
--}

add_plugin("BranchCoverage") 
pluginsConfig.BranchCoverage = {
    branchCoverageInfoFile = "./bc_info",
    optParseLoopCountLimit = 5,
    optWindowCountLimit = 1,
    optMSSCountLimit = 1,
    optTimestampCountLimit = 1,
    optSACKPermCountLimit = 1,
    optSACKCountLimit = 1,
    optFastopenCountLimit = 1,
    optExpFastopenCountLimit = 1,
    optNopCountLimit = 3,
    optEOLCountLimit = 1,
    optOtherCountLimit = 1,
    optWindowEdgeSrc = 0xffffffff8177d74f,
    optWindowEdgeDst = 0xffffffff8177d8a5,
    optMSSEdgeSrc = 0xffffffff8177d75d,
    optMSSEdgeDst = 0xffffffff8177d75f,
    optTimestampEdgeSrc = 0xffffffff8177d73f,
    optTimestampEdgeDst = 0xffffffff8177d868,
    optSACKPermEdgeSrc = 0xffffffff8177d755,
    optSACKPermEdgeDst = 0xffffffff8177d7e8,
    optSACKEdgeSrc = 0xffffffff8177d729,
    optSACKEdgeDst = 0xffffffff8177d8f5,
    optFastopenEdgeSrc = 0xffffffff8177d733,
    optFastopenEdgeDst = 0xffffffff8177d82d,
    optExpFastopenEdgeSrc = 0xffffffff8177d73b,
    optExpFastopenEdgeDst = 0xffffffff8177d79c,
    optNopEdgeSrc = 0xffffffff8177d6f6,
    optNopEdgeDst = 0xffffffff8177d6f8,
    optEOLEdgeSrc = 0xffffffff8177d6f2,
    optEOLEdgeDst = 0xffffffff8177d705,
}

add_plugin("MyDebugger") 
pluginsConfig.MyDebugger = {
    addressToTrack = {
    },
    edgeToTrack = {
    },
    functionToTrack = {
        0xffffffff8178bba0, --tcp_retransmit_timer
    },
    acceptPoints = {
        "0xffffffff8178453b", --tcp_data_queue():tcp_input.c:4663
        "0xffffffff81783e66", --tcp_data_queue():tcp_input.c:4684
        "0xffffffff817845cb", --tcp_data_queue_ofo():tcp_input.c:4461
        "0xffffffff81784629", --tcp_data_queue_ofo():tcp_input.c:4477
        "0xffffffff817843f9", --tcp_data_queue_ofo():tcp_input.c:4533
        "0xffffffff8178062e", --tcp_conn_request():tcp_input.c:6408
        "0xffffffff817916d3", --tcp_check_req():tcp_minisocks.c:773
    },
    dropPoints = {
        "0xffffffff817830eb", --tcp_input.c:3615
        "0xffffffff81781e37", --tcp_input.c:3735
        "0xffffffff81781e72", --tcp_input.c:3742
        --"0xffffffff817841d6", --tcp_input.c:4386
        "0xffffffff81784924", --tcp_input.c:4501
        --"0xffffffff817848e5", --tcp_input.c:4515
        --"0xffffffff8178442f", --tcp_input.c:4547
        "0xffffffff81784128", --tcp_input.c:4641
        "0xffffffff81783d5d", --tcp_input.c:4716
        "0xffffffff8177e0d7", --tcp_input.c:5194
        "0xffffffff81783ae6", --tcp_input.c:5265
        "0xffffffff817908b6", --tcp_ipv4.c:1653
        "0xffffffff8179152f", --tcp_minisocks.c:620
        "0xffffffff81791418", --tcp_minisocks.c:709(1)
        "0xffffffff817914f1", --tcp_minisocks.c:709(2)
        "0xffffffff8179167a", --tcp_minisocks.c:756
        "0xffffffff81791601", --tcp_minisocks.c:734
        "0xffffffff81783e2c:0xffffffff81783d96",    --tcp_input.c:4657
        "0xffffffff8178404a:0xffffffff81783d96",    --tcp_input.c:4729
        "0xffffffff817840f0:0xffffffff81783d96",    --tcp_input.c:4745
        "0xffffffff817839de:0xffffffff817839e0",    --tcp_input.c:5284
        "0xffffffff817839d9:0xffffffff81783a00",    --tcp_input.c:5291(1)
        "0xffffffff81783a51:0xffffffff81783a00",    --tcp_input.c:5291(2)
        "0xffffffff81783a5e:0xffffffff81783a00",    --tcp_input.c:5291(3)
        "0xffffffff817838e1:0xffffffff81783a00",    --tcp_input.c:5291(4)
        "0xffffffff81783985:0xffffffff817839f8",    --tcp_input.c:5325(1)
        "0xffffffff81783990:0xffffffff817839f8",    --tcp_input.c:5325(2)
        "0xffffffff81783a62:0xffffffff817839f8",    --tcp_input.c:5325(3)
        "0xffffffff81783a1e:0xffffffff81783a20",    --tcp_input.c:5333
        "0xffffffff81784aa2:0xffffffff81784a40",    --tcp_input.c:5453
        "0xffffffff81784cfa:0xffffffff81784a30",    --tcp_input.c:5487
        "0xffffffff81784a2a:0xffffffff81784a30",    --tcp_input.c:5531(1)
        "0xffffffff81784b29:0xffffffff81784a30",    --tcp_input.c:5531(2)
        "0xffffffff81784b34:0xffffffff81784a50",    --tcp_input.c:5534
        "0xffffffff81785467:0xffffffff81785543",    --tcp_input.c:5911
        "0xffffffff8178546f:0xffffffff8178538f",    --tcp_input.c:5914
        "0xffffffff8178547f:0xffffffff8178538f",    --tcp_input.c:5918
        "0xffffffff81785477:0xffffffff8178538f",    --tcp_input.c:5925
        "0xffffffff81785382:0xffffffff8178538f",    --tcp_input.c:5947
        "0xffffffff81785389:0xffffffff8178538f",    --tcp_input.c:5951
        "0xffffffff81785675:0xffffffff8178538f",    --tcp_input.c:6141
        "0xffffffff8178f011:0xffffffff8178f013",    --tcp_ipv4.c:1404
        "0xffffffff8178fffd:0xffffffff817900d1",    --tcp_ipv4.c:1607
        "0xffffffff817902d6:0xffffffff817900de",    --tcp_ipv4.c:1609(1)
        "0xffffffff817902e9:0xffffffff817900de",    --tcp_ipv4.c:1609(2)
        "0xffffffff81790082:0xffffffff817900c4",    --tcp_ipv4.c:1617(1)
        "0xffffffff817900be:0xffffffff817900c4",    --tcp_ipv4.c:1617(2)
        "0xffffffff817904af:0xffffffff81790721",    --tcp_ipv4.c:1672
        "0xffffffff81790776:0xffffffff817904ed",    --tcp_ipv4.c:1690
        "0xffffffff81791650:0xffffffff81791425",    --tcp_minisocks.c:745
    },
    terminateAtAcceptPoint = false,
    terminateAtDropPoint = false,
}

add_plugin("MyVmi") 

pluginsConfig.BranchCoverage.CriticalBranches = {
}


