.. _configuration-label: ScEpTIC Configuration ********************* ``config.sample.py`` shows a sample configuration of ScEpTIC. Here we have various parameters that we can tune to configure ScEpTIC and the emulated architecture. We suggest you to create a copy of this file and customize it accordingly to your requirements. Here we describe the various configuration parameters. Logging ####### Theese two constants control the logging of ScEpTIC events, such as the execution of instructions:: LOGGING_ENABLED = False LOGGING_LEVEL = logging.CRITICAL These two constants control the logging of the LLVM IR parser:: LOG_SECTION_CONTENT = False PARSE_LOG_LEVEL = logging.CRITICAL Output ###### We can control ScEpTIC analysis outputs using these variables:: test_name = 'program' file = 'samples/base.ll' save_test_results = True save_llvmir_code = True save_vm_state = True save_dir = 'analysis_results' - ``test_name`` specifies the name of the test that is saved inside ScEpTIC output file. This may be useful if we need to run multiple analysis - ``file`` specifies the path of the program to analyze - ``save_test_results`` specifies whether to save the test results - ``save_llvmir_code`` specifies whether to save the parsed LLVM IR of the program - ``save_vm_state`` specifies whether to save the emulated architecture state at the end of the simulation - ``save_dir`` speecifies the directory where ScEpTIC saves its analysis results Once ScEpTIC terminates its analysis, it creates a new folder into ``save_dir`` and saves the sate, the LLVM IR, and the analysis results, if enabled. Analysis to execute ################### ScEpTIC supports various analysis technqiues. We can control the analysis to execute with these variables:: run_continuous = True run_locate_memory_test = True run_evaluate_memory_test = True run_input_consistency_test = True run_output_profiling = True run_profiling = True - ``run_continous`` controls whether to execute the program sequentially - ``run_locate_memory_test`` controls wheter to execute the analysis for locating memory-based anomalies - ``run_evaluate_memory_test`` controls wheter to execute the analysis for evaluating the effects of memory-based anomalies - ``run_input_consistency_test`` controles whether to execute the analysis for environment input interactions - ``run_output_profiling`` controls whether to execute the analysis for environment ouput interactions - ``run_profiling`` controls whether to execute the analysis for debugging specific intermittent executions .. _program-configuration-label: Program Configuration ##################### The ``program_configuration`` dictionary allows us to configure various program-related settings. :: program_configuration = { 'ir_function_prefix': '@', #llvm ir function name prefix 'main_function_name': 'main', 'before_restore_function_name': 'sceptic_before_restore', 'after_restore_function_name': 'sceptic_after_restore', 'before_checkpoint_function_name': 'sceptic_before_checkpoint', 'after_checkpoint_function_name': 'sceptic_after_checkpoint', } - ``ir_function_prefix`` is the LLVM IR function name prefix, which is usually ``@`` - ``main_function_name`` is the name of the main function to execute ScEpTIC abstracts checkpoint and restore operations. Hence, to model custom checkpoint and restore routines, we need to create a function that contains the additional operations that checkpoint or restore operations execute with respect to saving and restoring main memory and the register file. Then, ScEpTIC uses the function names specified in ``before_restore_function_name``, ``after_restore_function_name``, ``before_checkpoint_function_name``, and ``after_checkpoint_function_name`` to execute the corresponding function. Note that ScEpTIC executes the custom functions before/after checkpoint and restore operations only if it finds the corresponding function in the LLVM IR. Register File Configuration ########################### .. |linear-scan| raw:: html linear scan register allocation algorithm .. |msp430| raw:: html MSP430 The ``register_file_configuration`` dictionary allows us to configure the simulated register-file settings. :: register_file_configuration = { 'use_physical_registers': True, 'physical_registers_number': 10, 'allocator_module_location': 'ScEpTIC.AST.register_allocation', 'allocator_module_name': 'linear_scan', 'allocator_function_name': 'allocate_registers', # nb: must take those arguments: functions, registers_number, reg_prefix, spill_prefix, spill_type 'physical_registers_prefix': 'R', 'spill_virtual_registers_prefix': '%spill_', 'spill_virtual_registers_type': 'i32', 'param_regs_count': 4 # number of registers used for passing parameters to functions (in arm/msp430 is 4) } - ``use_physical_registers`` specifies whether ScEpTIC simulates a physical or a virtual register file. If it is set to ``false``, ScEpTIC ignores all the other parameters, as it simulates a virtual register file that has unlimited registers - ``physical_registers_numer`` specifies the number of registers in the register file - ``allocator_module_location`` specifies the python path of the register allocation module - ``allocator_module_name`` specifies the name of the module containing the register allocation functionality. ScEpTIC already implements the |linear-scan| - ``allocator_function_name`` specifies the name of the register allocation function that applies the program transformation. Note that to implement your own register allocation algorithm, you can check our implementation of the linear scan register allocation algorithm inside ``ScEpTIC/AST/register_allocation/linear_scan.py``. Note that the main function of a register allocation module must take those arguments: functions, registers_number, reg_prefix, spill_prefix, spill_type - ``physical_registers_prefix`` specifies the prefix of physycal registers, used for textual representation of the register file - ``spill_virtual_registers_prefix`` specifies the prefix of virtual registers that will contain the stack address of spilled registers, used for textual representation of the register file - ``spill_virtual_registers_type`` specifies the LLVM IR first-class type of the virtual registers used for spilling physical registers - ``param_regs_count`` specifies the number of physical registers reserved for passing parameters in function calls. In the ARM and |msp430| architecture it is usually 4 .. _configuration-ed-label: Execution Depth ############### Depending on our checkpoint mechanism configuration, we may need to set the execution depth parameter for locating memory-based anomalies or evaluating their effects. In such a case, we set the ``execution_depth`` variable to an integer value:: execution_depth = 10 Analysis Stop Condition ####################### If we want to stop the analysis when an intermittence anomaly of any kind is encountered, we need to set to ``true`` the ``stop_on_first_anomaly`` variable:: stop_on_first_anomaly = True Otherwise, ScEpTIC will execute the analysis until it reaches the program end. Target System ############# .. |mementos| raw:: html Mementos .. |hibernus| raw:: html Hibernus .. |dino| raw:: html DINO .. |ratchet| raw:: html Ratchet .. |quickrecall| raw:: html QuickRecall The ``system`` variable specifies the system configuration that ScEpTIC will emulate. ScEpTIC provides various pre-defined system configurations: - ``mementos``: uses the same configuration of |mementos| - ``hibernus``: uses the same configuration of |hibernus| - ``dino``: uses the same configuration of |dino| - ``ratchet``: uses the same configuration of |ratchet| - ``quickrecall``: uses the same configuration of |quickrecall| You can find these system configurations inside ``ScEpTIC/emulator/intermittent_executor/configurator``. To create a new configuration, you can simply add a new python file inside that folder, and specify the ``memory_configuration`` and ``checkpoint_mechanism_configuration`` dictionaries as we describe in the next sections. Then, you need to specify as ``system`` value the name of the created python file. Instead, to use a custom configuration, we need to set ``system`` to ``custom``, and then we need to specify the memory configuration of the system and the settings of the checkpoint mechanism, as we describe next. :: system = 'custom' Custom Memory Setup ################### The ``memory_configuration`` dictionary specifies the memory configuration of the system. If a pre-defined system configuration is used, re-defining the ``memory_configuration`` dictionary overwrites portions of the pre-configured system setup. The overall ``memory_configuration`` dictionary contains the following elements:: memory_configuration = { 'sram': { 'enabled': True, 'stack': True, 'heap': True, 'gst': True, 'gst_prefix': 'SGST', 'gst_base_address': 0 }, 'nvm': { 'enabled': True, 'stack': False, 'heap': False, 'gst': True, 'gst_prefix': 'FGST', 'gst_base_address': 0 }, 'base_addresses': { 'stack': 0, 'heap': 0 }, 'prefixes': { 'stack': 'S', 'heap': 'H' }, 'gst': { 'default_ram': 'SRAM', # SRAM or NVM 'other_ram_section': '.NVM' }, 'address_dimension': 32 # bit } The ``sram`` and ``nvm`` sub-dictionaries specify the configuration for the volatile and non-volatile memories: - ``enabled`` specifies whether the considered memory is enabled - ``stack`` specifies whether the stack is allocated onto the considered memory. Note that the stack portion of the main memory can be allocated either onto sram or nvm - ``heap`` specifies whether the heap is allocated onto the considered memory. Note that the heap portion of the main memory can be allocated either onto sram or nvm - ``gst`` specifies whether the global symbol table (i.e. global variables) are allocated onto the considered memory. Note that the GST can be allocated both onto sram and nvm - ``gst_prefix`` specifies the prefix for the addresses of the gst variables allocated onto the considered memory - ``gst_base_address`` specifies the starting address of the gst in the considered memory The ``base_addresses`` and ``prefixes`` sub-dictionaries specify the starting address and the prefixes of the addresses for the stack and the heap:: 'base_addresses': { 'stack': 0, 'heap': 0 }, 'prefixes': { 'stack': 'S', 'heap': 'H' }, The GST (i.e. global variables) can be allocated both onto SRAM or NVM. The ``gst`` sub-dictionary specifies the policy for allocating a variable onto NVM:: 'gst': { 'default_ram': 'SRAM', # SRAM or NVM 'other_ram_section': '.NVM' }, - ``default_ram`` specifies the default memory location for global variables. It can be either ``SRAM`` or ``NVM`` - ``other_ram_section`` specifies the section that we can use in the program source code to tell ScEpTIC that a global variable must be allocated onto the non-default ram Note that to assign a section to a variable, we must specify the attribute section when we declare it:: int my_nvm_var __attribute__((section(".NVM"))); Finally, ``address_dimension`` specifies the size in bit of addresses. Custom Checkpoint Mechanism Setup ################################# The ``checkpoint_mechanism_configuration`` dictionary specifies the checkpoint mechanism configuration. If a pre-defined system configuration is used, re-defining the ``checkpoint_mechanism_configuration`` dictionary overwrites portions of the pre-configured system setup. The overall ``checkpoint_mechanism_configuration`` dictionary contains the following elements:: checkpoint_mechanism_configuration = { 'checkpoint_placement': 'dynamic', 'checkpoint_routine_name': 'checkpoint', 'restore_routine_name': 'restore', 'on_dynamic_voltage_alert': 'continue', 'restore_register_file': True, 'sram': {'restore_stack': True, 'restore_heap': True, 'restore_gst': True}, 'nvm': {'restore_stack': False, 'restore_heap': False, 'restore_gst': False}, 'environment': False } - ``checkpoint_placement`` specifies whether the checkpoint mechanism uses checkpoints statically placed in the program or dynamically decides when to save checkpoint. Hence, it must be set either to ``static`` or ``dynamic`` - ``checkpoint_routine_name`` specifies the name of the checkpoint routine. Note that this parameter is considered only for static checkpoint mechanisms to identify where checkpoints should be saved. Moreover, note that ScEpTIC does not execute the checkpoint routine and instead uses its own abstraction - ``restore_routine_name`` specifies the name of the restore routine. Note that this parameter is considered only for static checkpoint mechanism and ScEpTIC uses its own restore abstraction - ``on_dynamic_voltage_alert`` specifies the behavior of dynamic checkpoint mechanism when a low-voltage alert is raised. This can be either set to ``continue`` (i.e. the system saves a checkpoint and then continues the execution) or ``stop`` (i.e. the sytem saves a checkpoint and enters a deep-sleep mode) The other keys of the dictionary allows us to set up the elements that the checkpoint mechanism saves and restores. - ``restore_register_file`` specifies whether the checkpoint mechanism saves and restores the register file Then, we have two sub-dictionaries that specifies which elements need to be restored in the volatile and non-volatile memories:: 'restore_stack': True, 'restore_heap': True, 'restore_gst': True - ``restore_stack`` specifies whether checkpoints include the stack - ``restore_heap`` specifies whether checkpoints include the heap - ``restore_gst`` specifies whether checkpoints include the GST allocated onto the specified memory. Note that if a checkpoint mechanism implicitly applies variable versioning, you may need to set this to ``True`` Finally, we have the ``environment`` key, which specifies whether checkpoints include the environment state (e.g. restoring a checkpoint restores the position of a servo). Custom Builtins ############### The LLVM IR of the program we need to analyze does not include builtin libraries code, such as mathematical or memory management functions. ScEpTIC provides an implementation of the most used C libraries, such as: - ``math.h``: ScEpTIC provides the functionalities of acos, asin, atan, atan2, ceil, cos, cosh, exp, fabs, floor, fmod, log, log10, pow, sin, sinh, sqrt, tan, and tanh - ``stdio.h``: ScEpTIC provides the functionalities of the printf and of a custom debug_print - ``stdlib.h``: ScEpTIC provides the functionalities of calloc, free, malloc, and realloc These functions are defined inside ``ScEpTIC/AST/builtins/libs/``. ScEpTIC automatically links the implemented functionalities to the corresponding function calls inside the LLVM IR. ScEpTIC provides a functionality to define custom builtins directly in our configuration file. Each new function is specified as a python class that extends the ``Builtin`` base class, which must have: - a parameter ``tick_count`` that specifies the amount of clock cycles the function takes - a method ``get_val(self)`` that returns the result of the function execution The builtin can access funtion parameters using ``self.args``. Then, we need to provide the function declaration, by calling the class method ``define_builtin(function_name, LLVM_IR_parameters, LLVM_IR_return_type)``. Note that ``LLVM_IR_parameters`` is the textual representation of the list of LLVM IR types for the parameters of the function. Similarly, ``LLVM_IR_return_type`` is the textual representation of the return type expressed in LLVM IR type. For example, let us suppose we want to define a new function whose C definition is ``int test_builtin(double x, int a, int b, int c);``, which prints all its parameters and returns the latest one. We can do that as follows:: from ScEpTIC.AST.builtins.builtin import Builtin class TestBuiltin(Builtin): tick_count = 10 def get_val(self): for i in self.args: print(i) return self.args[3] Prova.define_builtin('test_builtin', 'double, i32, i32, i32', 'i32') Note that now we can use ``test_builtin()`` inside the source code. ScEpTIC will link the builtin to the function call and execute it. .. _configuration-input-label: Inputs ###### ScEpTIC models input elements, such as sensors, as custom built-in functions. We can define simple input elements inside our configuration by calling the ``create_input(name, function_name, LLVM_IR_return_type)`` method of the ``InputManager`` class. Note that ``name`` is a string representing the sensor name and ``function_name`` is the name of the function we call in the C source code to access the sensor. Then, we can set the value that the input function returns using the ``set_input_value(name, val)`` method of the ``InputManager`` class. For example, if we want to model a sensor named ``PIR`` that always returns an integer (i.e. 10):: from ScEpTIC.emulator.io.input import InputManager InputManager.create_input('PIR', 'pir_input', 'i32') InputManager.set_input_value('PIR', '10') Now, we can retrieve the input value by calling the ``pir_input()`` function inside our C source code. Note that such function takes no parameter. ScEpTIC allows us also to define more complex input functions, which support function parameters. For doing so, we need to create a class that extends the ``InputSkeleton`` base class, and we need to implement a ``get_val()`` method. It must set the return value onto ``self.value`` and then return the ``super().get_val()`` Then, similarly to the definition of a custom built-in, we need to call the class method ``define_input(name, function_name, LLVM_IR_parameters, LLVM_IR_return_type)``. For example, we can define a distance sensor that returns the value of its second parameter as follows:: from ScEpTIC.emulator.io.input import InputSkeleton class PIR(InputSkeleton): def get_val(self): self.value = self.arg[1] return super().get_val() PIR.define_input('Distance', 'my_distance', 'i32, i32', 'float') Similarly to before, we can now use ``my_distance()`` function inside our C source code. .. _configuration-output-label: Outputs ####### Similarly to inputs, ScEpTIC models output elements, such as actuators, as custom built-in functions. We can define simple output elements inside our configuration by calling the ``create_output(name, function_name, LLVM_IR_parameters)`` method of the ``OutputManager`` class. Note that ``name`` is a string representing the actuator name and ``function_name`` is the name of the function we call in the C source code to access the actuator. For example, we can model an actuator named ``motor`` as follows:: from ScEpTIC.emulator.io.output import OutputManager OutputManager.create_output('motor', 'motor_run', 'i32') Now, we can call the ``motor_run()`` function inside our C source code to simulate the sending of a start signal to a motor. Note that such function returns no value. Similarly to inputs, ScEpTIC allows us also to define more complex output functions, which support return values and internal state. This is useful to model complex output functions whose state depends on their current state. For doing so, we need to create a class that extends the ``OutputSkeleton`` base class, and we need to implement a ``get_val()`` method. We must call the ``set_output_val(value)`` method to update the value that the represented actuator has (i.e. the environment state). If we want to model an actuator that incrementally update its state, we can retrieve its current state using the method ``get_output_value()``. Moreover, if we need to initialize the output state, we can do so by re-implementing the method ``output_init()``, which is called on object creation. Then, similarly to the definition of a custom built-in, we need to call the class method ``define_output(name, function_name, LLVM_IR_parameters, LLVM_IR_return_type)``. For example, we can define a servo as follows:: from ScEpTIC.emulator.io.output import OutputSkeleton class Servo(OutputSkeleton): # set initial servo position to 0 def output_init(self): self.set_output_val(0) def get_val(self): value = self.get_output_value() + self.args[0] self.set_output_val(value) return value Motor.define_output('servo', 'move_servo', 'i32', 'i32') Similarly to before, we can now use ``move_servo()`` function inside our C source code.