what4-1.5.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2015-2020
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Stabilityprovisional
Safe HaskellSafe-Inferred
LanguageHaskell2010

What4.Config

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 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)

Note regarding concurrency: the configuration data structures in this module are implemented using MVars, and may safely be used in a multithreaded way; configuration changes made in one thread will be visible to others in a properly synchronized way. Of course, if one desires to isolate configuration changes in different threads from each other, separate configuration objects are required. The splitConfig operation may be useful to partially isolate configuration objects. As noted in the documentation for opt_onset, the validation procedures for options should not look up the value of other options, or deadlock may occur.

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 usage

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

  asdfMaxBound :: ConfigOption BaseIntegerType
  asdfMaxBound = configOption BaseIntegerRepr "asdf.max_bound"

Instances

Instances details
Show (ConfigOption tp) Source # 
Instance details

Defined in What4.Config

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

Construct a ConfigOption from a string name. Idiomatic usage 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.

Instances

Instances details
ShowF OptionSetting Source # 
Instance details

Defined in What4.Config

Methods

withShow :: forall p q (tp :: k) a. p OptionSetting -> q tp -> (Show (OptionSetting tp) => a) -> a #

showF :: forall (tp :: k). OptionSetting tp -> String #

showsPrecF :: forall (tp :: k). Int -> OptionSetting tp -> String -> String #

Show (OptionSetting tp) Source # 
Instance details

Defined in What4.Config

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 Void] Source #

Set the value of an option. Return any generated warnings. Throws an OptSetFailure 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

Instances details
Opt BaseBoolType Bool Source # 
Instance details

Defined in What4.Config

Opt BaseIntegerType Integer Source # 
Instance details

Defined in What4.Config

Opt BaseRealType Rational Source # 
Instance details

Defined in What4.Config

Opt (BaseStringType Unicode) Text Source # 
Instance details

Defined in What4.Config

setUnicodeOpt :: Some OptionSetting -> Text -> IO [Doc Void] Source #

Given a unicode text value, set the named option to that value or generate an OptSetFailure exception if the option is not a unicode text valued option.

setIntegerOpt :: Some OptionSetting -> Integer -> IO [Doc Void] Source #

Given an integer value, set the named option to that value or generate an OptSetFailure exception if the option is not an integer valued option.

setBoolOpt :: Some OptionSetting -> Bool -> IO [Doc Void] Source #

Given a boolean value, set the named option to that value or generate an OptSetFailure exception if the option is not a boolean valued option.

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. NOTE! the onset action should not attempt to look up the values of other configuration settings, or deadlock may occur.

    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 Void

    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 eventual 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 Void -> OptionSetResult Source #

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

optErr :: Doc Void -> OptionSetResult Source #

Reject the new option value with an error message.

checkOptSetResult :: OptionSetting tp -> OptionSetResult -> IO [Doc Void] Source #

Throw an exception if the given OptionSetResult indicates 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.

Instances

Instances details
Show ConfigDesc Source # 
Instance details

Defined in What4.Config

mkOpt Source #

Arguments

:: ConfigOption tp

Fixes the name and the type of this option

-> OptionStyle tp

Define the style of this option

-> Maybe (Doc Void)

Help text

-> Maybe (ConcreteVal tp)

A default value for this option

-> ConfigDesc 

The most general method for constructing 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

:: forall tp help. 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

:: forall help tp. 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.

copyOpt :: (Text -> Text) -> ConfigDesc -> ConfigDesc Source #

The copyOpt creates a duplicate ConfigDesc under a different name. This is typically used to taking a common operation and modify the prefix to apply it to a more specialized role (e.g. solver.strict_parsing --> solver.z3.strict_parsing). The style and help text of the input ConfigDesc are preserved, but any deprecation is discarded.

deprecatedOpt :: [ConfigDesc] -> ConfigDesc -> ConfigDesc Source #

Used as a wrapper for an option that has been deprecated. If the option is actually set (as opposed to just using the default value) then this will emit an OptionSetResult warning that time, optionally mentioning the replacement option (if specified).

There are three cases of deprecation: 1. Removing an option that no longer applies 2. Changing the name or heirarchical position of an option. 3. #2 and also changing the type. 4. Replacing an option by multiple new options (e.g. split url option into hostname and port options)

In the case of #1, the option will presumably be ignored by the code and the warnings are provided to allow the user to clean the option from their configurations.

In the case of #2, the old option and the new option will share the same value storage: changes to one can be seen via the other and vice versa. The code can be switched over to reference the new option entirely, and user configurations setting the old option will still work until they have been updated and the definition of the old option is removed entirely.

NOTE: in order to support #2, the newer option should be declared (via insertOption) *before* the option it deprecates.

In the case of #3, it is not possible to share storage space, so during the deprecation period, the code using the option config value must check both locations and decide which value to utilize.

Case #4 is an enhanced form of #3 and #2, and is generally treated as #3, but adds the consideration that deprecation warnings will need to advise about multiple new options. The inverse of #4 (multiple options being combined to a single newer option) is just treated as separate deprecations.

NOTE: in order to support #4, the newer options should all be declared (via insertOption) *before* the options they deprecate.

Nested deprecations are valid, and replacement warnings are automatically transitive to the newest options.

Any user-supplied value for the old option will result in warnings emitted to the OptionSetResult for all four cases. Code should ensure that these warnings are appropriately communicated to the user to allow configuration updates to occur.

Note that for #1 and #2, the overhead burden of continuing to define the deprecated option is very small, so actual removal of the older config can be delayed indefinitely.

Building and manipulating configurations

data Config Source #

The main configuration datatype. It consists of a Read/Write var containing 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 OptCreateFailure exception will be raised if any of the given options clash with options that already exists.

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

Extend an existing configuration with new options. If any of the given options are already present in the configuration, nothing is done for that option and it is silently skipped.

splitConfig :: Config -> IO Config Source #

Create a new configuration object that shares the option settings currently in the given input config. However, any options added to either configuration using extendConfig will not be propagated to the other.

Option settings that already exist in the input configuration will be shared between both; changes to those options will be visible in both configurations.

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 

Instances

Instances details
Pretty ConfigValue Source # 
Instance details

Defined in What4.Config

Methods

pretty :: ConfigValue -> Doc ann #

prettyList :: [ConfigValue] -> Doc ann #

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

Given the name of a subtree, return all the currently-set configuration 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 Void] Source #

Given the name of a subtree, compute help text for all the options available 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.