what4-1.0: Solver-agnostic symbolic values support for issuing queries

Copyright(c) Galois Inc 2015-2020
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

What4.Config

Contents

Description

This module provides access to persistent configuration settings, and is designed for access both by Haskell client code of the What4 library, and by users of the systems ultimately built using the library, for example, from within a user-facing REPL.

Configurations are defined dynamically by combining a collection of configuration option descriptions. This allows disparate modules to define their own configuration options, rather than having to define the options for all modules in a central place. Every configuration option has a name, which consists of a nonempty sequence of period-separated strings. The intention is that option names should conform to a namespace hierarchy both for organizational purposes and to avoid namespace conflicts. For example, the options for an "asdf" module might be named as:

  • asdf.widget
  • asdf.frob
  • asdf.max_bound

At runtime, a configuration consists of a collection of nested finite maps corresponding to the namespace tree of the existing options. A configuration option may be queried or set either by using a raw string representation of the name (see getOptionSettingFromText), or by using a ConfigOption value (using getOptionSetting), which provides a modicum of type-safety over the basic dynamically-typed configuration maps.

Each option is associated with an "option style", which describes the underlying type of the option (e.g., integer, boolean, string, etc.) as well as the allowed settings of that value. In addition, options can take arbitrary actions when their values are changed in the opt_onset callback.

Every configuration comes with the built-in verbosity configuration option pre-defined. A Config value is constructed using the initialConfig operation, which should be given the initial verbosity value and a collection of configuration options to install. A configuration may be later extended with additional options by using the extendConfig operation.

Example use (assuming the you wanted to use the z3 solver):

import What4.Solver

setupSolverConfig :: (IsExprBuilder sym) -> sym -> IO ()
setupSolverConfig sym = do
  let cfg = getConfiguration sym
  extendConfig (solver_adapter_config_options z3Adapter) cfg
  z3PathSetter <- getOptionSetting z3Path
  res <- setOpt z3PathSetter "/usr/bin/z3"
  assert (null res) (return ())

Developer's note: we might want to add the following operations:

  • a method for "unsetting" options to restore the default state of an option
  • a method for removing options from a configuration altogether (i.e., to undo extendConfig)
Synopsis

Names of properties

data ConfigOption (tp :: BaseType) Source #

A Haskell-land wrapper around the name of a configuration option. Developers are encouraged to define and use ConfigOption values to avoid two classes of errors: typos in configuration option names; and dynamic type-cast failures. Both classes of errors can be lifted to statically-checkable failures (missing symbols and type-checking, respectively) by consistently using ConfigOption values.

The following example indicates the suggested useage

  asdfFrob :: ConfigOption BaseRealType
  asdfFrob = configOption BaseRealRepr "asdf.frob"

  asdfMaxBound :: ConfigOption BaseIntegerType
  asdfMaxBound = configOption BaseIntegerRepr "asdf.max_bound"
Instances
Show (ConfigOption tp) Source # 
Instance details

Defined in What4.Config

configOption :: BaseTypeRepr tp -> String -> ConfigOption tp Source #

Construct a ConfigOption from a string name. Idomatic useage is to define a single top-level ConfigOption value in the module where the option is defined to consistently fix its name and type for all subsequent uses.

configOptionType :: ConfigOption tp -> BaseTypeRepr tp Source #

Retrieve the run-time type representation of tp.

configOptionName :: ConfigOption tp -> String Source #

Reconstruct the original string name of this option.

configOptionText :: ConfigOption tp -> Text Source #

Reconstruct the original string name of this option.

configOptionNameParts :: ConfigOption tp -> [Text] Source #

Get the individual dot-separated segments of an option's name.

Option settings

data OptionSetting (tp :: BaseType) Source #

An OptionSetting gives the direct ability to query or set the current value of an option. The getOption field is an action that, when executed, fetches the current value of the option, if it is set. The setOption method attempts to set the value of the option. If the associated opt_onset validation method rejects the option, it will retain its previous value; otherwise it will be set to the given value. In either case, the generated OptionSetResult will be returned.

class Opt (tp :: BaseType) (a :: Type) | tp -> a where Source #

A utility class for making working with option settings easier. The tp argument is a BaseType, and the a argument is an associcated Haskell type.

Minimal complete definition

getMaybeOpt, trySetOpt

Methods

getMaybeOpt :: OptionSetting tp -> IO (Maybe a) Source #

Return the current value of the option, as a Maybe value.

trySetOpt :: OptionSetting tp -> a -> IO OptionSetResult Source #

Attempt to set the value of an option. Return any errors or warnings.

setOpt :: OptionSetting tp -> a -> IO [Doc] Source #

Set the value of an option. Return any generated warnings. Throw an exception if a validation error occurs.

getOpt :: OptionSetting tp -> IO a Source #

Get the current value of an option. Throw an exception if the option is not currently set.

Instances
Opt BaseNatType Natural Source # 
Instance details

Defined in What4.Config

Opt BaseIntegerType Integer Source # 
Instance details

Defined in What4.Config

Opt BaseBoolType Bool Source # 
Instance details

Defined in What4.Config

Opt (BaseStringType Unicode) Text Source # 
Instance details

Defined in What4.Config

Defining option styles

data OptionStyle (tp :: BaseType) Source #

An option defines some metadata about how a configuration option behaves. It contains a base type representation, which defines the runtime type that is expected for setting and querying this option at runtime.

Constructors

OptionStyle 

Fields

  • opt_type :: BaseTypeRepr tp

    base type representation of this option

  • opt_onset :: Maybe (ConcreteVal tp) -> ConcreteVal tp -> IO OptionSetResult

    An operation for validating new option values. This action may also be used to take actions whenever an option setting is changed.

    The first argument is the current value of the option (if any). The second argument is the new value that is being set. If the validation fails, the operation should return a result describing why validation failed. Optionally, warnings may also be returned.

  • opt_help :: Doc

    Documentation for the option to be displayed in the event a user asks for information about this option. This message should contain information relevant to all options in this style (e.g., its type and range of expected values), not necessarily information about a specific option.

  • opt_default_value :: Maybe (ConcreteVal tp)

    This gives a default value for the option, if set.

set_opt_default :: ConcreteVal tp -> OptionStyle tp -> OptionStyle tp Source #

Update the opt_default_value field.

set_opt_onset :: (Maybe (ConcreteVal tp) -> ConcreteVal tp -> IO OptionSetResult) -> OptionStyle tp -> OptionStyle tp Source #

Update the opt_onset field.

OptionSetResult

data OptionSetResult Source #

When setting the value of an option, a validation function is called (as defined by the associated OptionStyle). The result of the validation function is an OptionSetResult. If the option value given is invalid for some reason, an error should be returned. Additionally, warning messages may be returned, which will be passed through to the eventuall call site attempting to alter the option setting.

Constructors

OptionSetResult 

optOK :: OptionSetResult Source #

Accept the new option value with no errors or warnings.

optWarn :: Doc -> OptionSetResult Source #

Accept the given option value, but report a warning message.

optErr :: Doc -> OptionSetResult Source #

Reject the new option value with an error message.

checkOptSetResult :: OptionSetResult -> IO [Doc] Source #

Throw an exception if the given OptionSetResult indidcates an error. Otherwise, return any generated warnings.

Option style templates

data Bound r Source #

An inclusive or exclusive bound.

Constructors

Exclusive r 
Inclusive r 
Unbounded 

boolOptSty :: OptionStyle BaseBoolType Source #

Standard option style for boolean-valued configuration options

integerOptSty :: OptionStyle BaseIntegerType Source #

Standard option style for integral-valued configuration options

realOptSty :: OptionStyle BaseRealType Source #

Standard option style for real-valued configuration options

realWithRangeOptSty :: Bound Rational -> Bound Rational -> OptionStyle BaseRealType Source #

Option style for real-valued options with upper and lower bounds

realWithMinOptSty :: Bound Rational -> OptionStyle BaseRealType Source #

Option style for real-valued options with a lower bound

realWithMaxOptSty :: Bound Rational -> OptionStyle BaseRealType Source #

Option style for real-valued options with an upper bound

integerWithRangeOptSty :: Bound Integer -> Bound Integer -> OptionStyle BaseIntegerType Source #

Option style for integer-valued options with upper and lower bounds

integerWithMinOptSty :: Bound Integer -> OptionStyle BaseIntegerType Source #

Option style for integer-valued options with a lower bound

integerWithMaxOptSty :: Bound Integer -> OptionStyle BaseIntegerType Source #

Option style for integer-valued options with an upper bound

enumOptSty :: Set Text -> OptionStyle (BaseStringType Unicode) Source #

A configuration style for options that must be one of a fixed set of text values

listOptSty :: Map Text (IO OptionSetResult) -> OptionStyle (BaseStringType Unicode) Source #

A configuration syle for options that must be one of a fixed set of text values. Associated with each string is a validation/callback action that will be run whenever the named string option is selected.

executablePathOptSty :: OptionStyle (BaseStringType Unicode) Source #

A configuration style for options that are expected to be paths to an executable image. Configuration options with this style generate a warning message if set to a value that cannot be resolved to an absolute path to an executable file in the current OS environment.

Describing configuration options

data ConfigDesc Source #

A ConfigDesc describes a configuration option before it is installed into a Config object. It consists of a ConfigOption name for the option, an OptionStyle describing the sort of option it is, and an optional help message describing the semantics of this option.

mkOpt Source #

Arguments

:: ConfigOption tp

Fixes the name and the type of this option

-> OptionStyle tp

Define the style of this option

-> Maybe Doc

Help text

-> Maybe (ConcreteVal tp)

A default value for this option

-> ConfigDesc 

The most general method for construcing a normal ConfigDesc.

opt Source #

Arguments

:: Pretty help 
=> ConfigOption tp

Fixes the name and the type of this option

-> ConcreteVal tp

Default value for the option

-> help

An informational message describing this option

-> ConfigDesc 

Construct an option using a default style with a given initial value

optV Source #

Arguments

:: Pretty help 
=> ConfigOption tp

Fixes the name and the type of this option

-> ConcreteVal tp

Default value for the option

-> (ConcreteVal tp -> Maybe help)

Validation function. Return `Just err` if the value to set is not valid.

-> help

An informational message describing this option

-> ConfigDesc 

Construct an option using a default style with a given initial value. Also provide a validation function to check new values as they are set.

optU Source #

Arguments

:: Pretty help 
=> ConfigOption tp

Fixes the name and the type of this option

-> help

An informational message describing this option

-> ConfigDesc 

Construct an option using a default style with no initial value.

optUV Source #

Arguments

:: Pretty help 
=> ConfigOption tp

Fixes the name and the type of this option

-> (ConcreteVal tp -> Maybe help)

Validation function. Return `Just err` if the value to set is not valid.

-> help

An informational message describing this option

-> ConfigDesc 

Construct an option using a default style with no initial value. Also provide a validation function to check new values as they are set.

Building and manipulating configurations

data Config Source #

The main configuration datatype. It consists of an IORef continaing the actual configuration data.

initialConfig Source #

Arguments

:: Integer

Initial value for the verbosity option

-> [ConfigDesc]

Option descriptions to install

-> IO Config 

Construct a new configuration from the given configuration descriptions.

extendConfig :: [ConfigDesc] -> Config -> IO () Source #

Extend an existing configuration with new options. An error will be raised if any of the given options clash with options that already exists.

getOptionSetting :: ConfigOption tp -> Config -> IO (OptionSetting tp) Source #

Given a ConfigOption name, produce an OptionSetting object for accessing and setting the value of that option.

An exception is thrown if the named option cannot be found the Config object, or if a type mismatch occurs.

getOptionSettingFromText :: Text -> Config -> IO (Some OptionSetting) Source #

Given a text name, produce an OptionSetting object for accessing and setting the value of that option.

An exception is thrown if the named option cannot be found.

Extracting entire subtrees of the current configuration

data ConfigValue where Source #

A ConfigValue bundles together the name of an option with its current value.

Constructors

ConfigValue :: ConfigOption tp -> ConcreteVal tp -> ConfigValue 

getConfigValues :: Text -> Config -> IO [ConfigValue] Source #

Given the name of a subtree, return all the currently-set configurtion values in that subtree.

If the subtree name is empty, the entire tree will be traversed.

Printing help messages for configuration options

configHelp :: Text -> Config -> IO [Doc] Source #

Given the name of a subtree, compute help text for all the options avaliable in that subtree.

If the subtree name is empty, the entire tree will be traversed.

Verbosity

verbosity :: ConfigOption BaseIntegerType Source #

Verbosity of the simulator. This option controls how much informational and debugging output is generated. 0 yields low information output; 5 is extremely chatty.

verbosityLogger :: Config -> Handle -> IO (Int -> String -> IO ()) Source #

Return an operation that will consult the current value of the verbosity option, and will print a string to the given Handle if the provided int is smaller than the current verbosity setting.