config.toml

#==================================================================================#
#  BSD 2-Clause License                                                            #
#                                                                                  #
#  Copyright (c) 2020-2021 Thibaut Pérami                                          #
#  Copyright (c) 2020-2021 Dhruv Makwana                                           #
#  Copyright (c) 2019-2021 Peter Sewell                                            #
#  All rights reserved.                                                            #
#                                                                                  #
#  This software was developed by the University of Cambridge Computer             #
#  Laboratory as part of the Rigorous Engineering of Mainstream Systems            #
#  (REMS) project.                                                                 #
#                                                                                  #
#  This project has been partly funded by EPSRC grant EP/K008528/1.                #
#  This project has received funding from the European Research Council            #
#  (ERC) under the European Union's Horizon 2020 research and innovation           #
#  programme (grant agreement No 789108, ERC Advanced Grant ELVER).                #
#  This project has been partly funded by an EPSRC Doctoral Training studentship.  #
#  This project has been partly funded by Google.                                  #
#                                                                                  #
#  Redistribution and use in source and binary forms, with or without              #
#  modification, are permitted provided that the following conditions              #
#  are met:                                                                        #
#  1. Redistributions of source code must retain the above copyright               #
#     notice, this list of conditions and the following disclaimer.                #
#  2. Redistributions in binary form must reproduce the above copyright            #
#     notice, this list of conditions and the following disclaimer in              #
#     the documentation and/or other materials provided with the                   #
#     distribution.                                                                #
#                                                                                  #
#  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''              #
#  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED               #
#  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A                 #
#  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR             #
#  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,                    #
#  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT                #
#  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF                #
#  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND             #
#  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,              #
#  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT              #
#  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF              #
#  SUCH DAMAGE.                                                                    #
#                                                                                  #
#==================================================================================#

# The config format is unstable while read-dwarf is in developement, but it is simpler to add
# options here than on the command line

# Default achitecture to use when no ELF is provided (for text instruction commands)
# Optional. The default_arch option of compile-time config.ml will decide then.
default-arch = "aarch64"

[archs.aarch64]
toolchain = "aarch64-linux-gnu"

    [archs.aarch64.isla]
    ignored-regs = ["SEE",
                    "__unconditional",
                    "DBGEN",
                    "__v81_implemented",
                    "__v82_implemented",
                    "__v83_implemented",
                    "__v84_implemented",
                    "__v85_implemented",
                    # Vector registers are held in a vector, not yet fully supported
                     "_V"]
    arch-file = "../../aarch64.ir" # relative to the toml file
    arch-toml = "isla_aarch64.toml" # relative to the toml file
    linearize = ["ConditionHolds", "integer_conditional_select", "InterruptPending"]
    other-opts = []

[archs.riscv64]
toolchain = "riscv64-linux-gnu"

    [archs.riscv64.isla]
    # The TLB registers get None written to them during init, read-dwarf doesn't know what to do with them
    ignored-regs = ["tlb39",
                    "tlb48",
                    # Enum registers don't appear to translate to Z3 yet
                    "cur_privilege"]
    arch-file = "../../../isla-snapshots/riscv64.ir" # relative to the toml file
    arch-toml = "isla_riscv64.toml" # relative to the toml file
    linearize = []
    other-opts = []


[z3]
timeout = 1000 # ms, optional
# memory = 2000 # MB, optional

    [z3.simplify-opts]
    # Use the same name as given by (help simplify) in Z3. Only booleans are supported for now
    pull_cheap_ite = true
    elim_sign_ext = false