Changes between Version 32 and Version 33 of Language
- Timestamp:
- 05/20/23 11:11:30 (3 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
Language
v32 v33 3 3 [[PageOutline(2-3)]] 4 4 5 == Types 6 7 === The Boolean type 5 == Types #sec:types 6 7 === The Boolean type #boolean-type 8 8 9 9 The boolean type is denoted `_Bool`, as in C. Its values are 0 and 1, which are also denoted by `$false` and `$true`, respectively. … … 11 11 `bool` to be an alias for `_Bool`. 12 12 13 === The integer type 13 === The integer type #int-types 14 14 15 15 There is one integer type, corresponding to the mathematical integers. … … 17 17 [This is expected to change.] 18 18 19 === The real type 19 === The real type #real-types 20 20 21 21 There is one real type, corresponding to the mathematical real numbers. Currently, all of the C real types `double`, `float`, etc., are mapped to the CIVL real type. [This is expected to change.] 22 22 23 === The process type `$proc` 23 === The process type `$proc` #proc-type 24 24 25 25 This is a primitive object type and functions like any other primitive C type (e.g., `int`). An object of this type refers to a process. It can be thought of as a process ID, but it is not an integer and cannot be cast to one. Certain expressions take an argument of `$proc` type and some return something of `$proc` type. The operators `==` and `!=` may be used with two arguments of type `$proc` to determine whether the two arguments refer to the same process. The constant `$self` has `$proc` type and refers to the process evaluating this expression; constant `$proc_null` has `$proc` type and refers to no process. 26 26 27 === The scope type `$scope` 27 === The scope type `$scope` #scope-type 28 28 29 29 An object of this type is a reference to a dynamic scope. … … 34 34 Two different variables of type `$scope` may be aliased, i.e., they may refer to the same dynamic scope. 35 35 36 === Domain types: `$domain` and `$domain(n)` 36 === Domain types: `$domain` and `$domain(n)` #domain-type 37 37 38 38 A domain type is used to represent a set of tuples of integer values. … … 45 45 Certain statements use domains, such as the “CIVL-for” loop `$for`. 46 46 47 === The range type `$range` 47 === The range type `$range` #range-type 48 48 49 49 An object of this type represents an ordered set of integers. … … 51 51 They can also be used in quantified expressions to specify the domain of a bound variable (see `$forall` and `$exists`). 52 52 53 == Type qualifiers 54 55 === Declaring input and output variables: `$input` and `$output` 53 == Type qualifiers #qualifiers 54 55 === Declaring input and output variables: `$input` and `$output` #input-output 56 56 57 57 The declaration of a variable in the root scope may include the type qualifier `$input`, e.g., … … 87 87 end up with the same values at termination). 88 88 89 === Abstract (uninterpreted) functions: `$abstract` 89 === Abstract (uninterpreted) functions: `$abstract` #abstract 90 90 91 91 An abstract function declares a function without a body. An abstract function is declared using a standard function prototype with the function qualifier `$abstract`, e.g., … … 95 95 An abstract function must have a non-void return type and take at least one parameter. An invocation of an abstract function is an expression and can be used anywhere an expression is allowed. The interpretation is an "uninterpreted function". A unique symbolic constant of function type will be created, corresponding to the abstract function, and invocations are represented as applications of the uninterpreted function to the arguments. 96 96 97 === Atomic functions: `$atomic_f` 97 === Atomic functions: `$atomic_f` #atomic_f 98 98 99 99 A function is declared atomic using the function qualifier `$atomic_f`, e.g., … … 107 107 An atomic function must have a definition; in particular, neither a system function nor an abstract function may be declared using `$atomic_f`. 108 108 109 === System functions: `$system` 109 === System functions: `$system` #system 110 110 111 111 A system function is one in which the definition of the function is not provided in CIVL-C code, but is implemented instead in a certain Java class. A system function is declared by adding the function qualifier `$system` to a function prototype. Invocation of a system function always takes place in a single atomic step. … … 113 113 A system function may have a guard, which is specified in the function contract using a `$executes_when` clause. Unless constrained by its contract or other qualifiers, a system function may modify the stay in an arbitrary way. 114 114 115 === Pure functions: `$pure` 115 === Pure functions: `$pure` #pure 116 116 117 117 A system or atomic function may be declared to be `$pure`, e.g., … … 124 124 This means that the function is a mathematical function of its arguments only. I.e., an invocation of the function has no side-effects and the return value depends on the arguments only (if called twice with the same arguments, it will return the same value, regardless of any differences in the state). The user is responsible for ensuring that a function declared pure actually is pure. If this is not the case, the model checker may produce incorrect results. 125 125 126 == Expressions 127 128 === Boolean expressions, `=>`, `$forall`, `$exists` 126 == Expressions #expressions 127 128 === Boolean expressions, `=>`, `$forall`, `$exists` #boolean-expressions 129 129 130 130 CIVL-C provides the boolean constants`$true` and `$false`, which are simply defined as 1 and 0, respectively. … … 170 170 }}} 171 171 172 === Domain literals 172 === Domain literals #domain-literals 173 173 174 174 An expression of the form … … 187 187 }}} 188 188 189 === This scope: the `$here` scope expression 189 === This scope: the `$here` scope expression #here 190 190 Expression of type `$scope`, evaluating to the dynamic scope in which the evaluation takes place. 191 191 192 === The null process reference: `$proc_null` 192 === The null process reference: `$proc_null` #proc_null 193 193 The null process constant. Similar to the NULL pointer, this gives an object of `$proc` type a defined value, and can be used in `==` and `!=` expressions. 194 194 It cannot be used as the argument to `$wait` or `$waitall`. 195 195 196 === The root scope constant: `$root` 196 === The root scope constant: `$root` #root 197 197 Constant of type `$scope`, the root dynamic scope. 198 198 199 === Range literals: `lo .. hi` 199 === Range literals: `lo .. hi` #range-literals 200 200 201 201 An expression of the form `lo .. hi` where `lo` and `hi` are integer expressions, represents the range consisting of the integers `lo`, `lo` + 1, ..., `hi` (in that order). … … 206 206 Precisely, the infinite sequence is intersected with the set of integers greater than or equal to `lo`. 207 207 208 === The scope of an expression: `$scopeof` 208 === The scope of an expression: `$scopeof` #scopeof 209 209 210 210 Given any left-hand-side expression ''expr'', the expression `$scopeof(`''expr''`)` evaluates to the dynamic scope containing the object specified by ''expr''. … … 230 230 }}} 231 231 232 === Scope relational expressions 232 === Scope relational expressions #scope-expressions 233 233 234 234 Let `s1` and `s2` be expressions of type `$scope`. The following are all CIVL-C expressions of boolean type: … … 243 243 Each of these expressions is erroneous if `s1` or `s2` is undefined. This error is reported by the model checker. 244 244 245 === This process: `$self` 245 === This process: `$self` #self 246 246 247 247 This expression of `$proc` type returns a reference to the process which is evaluating this expression. 248 248 It provides a way for code to obtain the identity of the process executing the code. 249 249 250 === Spawning a new process: `$spawn` 250 === Spawning a new process: `$spawn` #spawn 251 251 252 252 A spawn expression is an expression with side-effects. … … 262 262 If the function `f` returns a value, that value is simply ignored. 263 263 264 == Statements 265 266 === Atomic blocks: `$atomic` 264 == Statements #statements 265 266 === Atomic blocks: `$atomic` #atomic 267 267 268 268 An ''atomic block'' is a statement of the form … … 303 303 so that when the lock is re-obtained, the original multiplicity is still in place. 304 304 305 === Nondeterministic selection statement `$choose` 305 === Nondeterministic selection statement `$choose` #choose 306 306 307 307 A `$choose` statement has the form … … 341 341 }}} 342 342 343 === Domain iteration statement: `$for` 343 === Domain iteration statement: `$for` #for 344 344 345 345 A domain statement has the form … … 364 364 There is a also a parallel version of this construct, `$parfor`. 365 365 366 === Parallel for loop: `$parfor` 366 === Parallel for loop: `$parfor` #parfor 367 367 368 368 A parallel for loop statement has the form … … 379 379 In particular, there is an effective barrier at the end of the loop, and all the spawned processes disappear after this point. 380 380 381 === Guarded commands: `$when` 381 === Guarded commands: `$when` #when 382 382 383 383 A guarded command is encoded in CIVL-C using a `$when` statement: … … 438 438 439 439 440 == Functions 441 442 === Assertions: `$assert` 440 == Functions #functions 441 442 === Assertions: `$assert` #assert 443 443 444 444 The system function `$assert` has the signature … … 458 458 If x=3 and B=2, the assertion is violated and CIVL prints the error message “x-coordinate 3 exceeds bound 2”. 459 459 460 === Assumptions: `$assume` 460 === Assumptions: `$assume` #assume 461 461 462 462 The system function `$assume` has signature … … 472 472 declares `N` and `B` to be integer inputs and restricts consideration to inputs satisfying 1 ≤ `N` ≤ `B`. 473 473 474 === Temporary assumptions: `$assume_push` and `$assume_pop` 474 === Temporary assumptions: `$assume_push` and `$assume_pop` #temp-assumptions 475 475 476 476 These functions have signatures: … … 491 491 This mechanism serves as a "widening operator" (in the sense of abstract interpretation), which enables symbolic execution to converge. 492 492 493 === Nondeterministic choice of integer: `$choose_int` 493 === Nondeterministic choice of integer: `$choose_int` #choose_int 494 494 495 495 This function has signature … … 499 499 and returns an arbitrary integer in [0.''n''-1]. In verification mode, all possible choices are enumerated and explored. 500 500 501 === Initialization by default value: `$default_value` 501 === Initialization by default value: `$default_value` #default_value 502 502 503 503 Assigns an object the default value of its type. Signature: … … 510 510 For example, 0 is the default value for a numeric type. 511 511 512 === Explicit elaboration of a domain: `$elaborate_domain` 512 === Explicit elaboration of a domain: `$elaborate_domain` #elaborate_domain 513 513 514 514 Forces explicit enumeration of the elements of a finite domain. Signature … … 518 518 In the concrete semantics, this is a no-op. 519 519 520 === Process exit: `$exit` 520 === Process exit: `$exit` #exit 521 521 522 522 Terminates the calling process. Signature: … … 525 525 }}} 526 526 527 === Assignment of arbitrary value: `$havoc` 527 === Assignment of arbitrary value: `$havoc` #havoc 528 528 529 529 Assigns an arbitrary value of the object's type to an object. Signature: … … 535 535 In the symbolic semantics, this function assigns a fresh symbolic constant of the appropriate type to the object pointed to by `ptr`. 536 536 537 === Hiding pointers: `$hide`, `$reveal`, and `$hidden` 537 === Hiding pointers: `$hide`, `$reveal`, and `$hidden` #hide-reveal-hidden 538 538 539 539 The partial order reduction algorithm used by the CIVL Model Checker computes the set of memory locations that a process ''p'' can reach. … … 556 556 The function `$hidden` tells whether its argument is a value returned by `$hide`. 557 557 558 === Checking pointer safety: `$is_derefable` 558 === Checking pointer safety: `$is_derefable` #is_derefable 559 559 560 560 This function has signature … … 565 565 This means `ptr` points to a memory location that is capable of and is currently holding a value of type T, where T is the type of `*ptr`. 566 566 567 === Checking process termination: `$is_terminated` 567 === Checking process termination: `$is_terminated` #is_terminated 568 568 569 569 Signature: … … 574 574 If `p` is undefined or `$proc_null`, returns 0. 575 575 576 === Specifying local regions: `$local_start` and `$local_end` 576 === Specifying local regions: `$local_start` and `$local_end` #local 577 577 578 578 {{{ … … 655 655 }}} 656 656 657 ==== Use of `$yield` within a local region 657 ==== Use of `$yield` within a local region #local-yield 658 658 659 659 Local blocks can also be broken up at specified points using function `$yield`. … … 665 665 Only `$local_start` grants a thread a special priority. 666 666 667 === Heap memory allocation: `$malloc` and `$free` 667 === Heap memory allocation: `$malloc` and `$free` #malloc-free 668 668 669 669 Allocate and deallocate heap memory. Signatures: … … 681 681 An error is generated if the pointer is not one that was returned by $malloc, or if it was already freed. 682 682 683 === Print the path condition: `$pathCondition` 683 === Print the path condition: `$pathCondition` #print-path-condition 684 684 685 685 Prints the current effective path condition. … … 688 688 }}} 689 689 690 === Power function: `$pow` 690 === Power function: `$pow` #pow 691 691 692 692 Computes ''x^y^''. … … 695 695 }}} 696 696 697 === Waiting for process termination: `$wait` and `$waitall` 697 === Waiting for process termination: `$wait` and `$waitall` #wait 698 698 699 699 {{{ … … 707 707 It is OK if a process argument refers to a process that has already terminated. 708 708 709 === Yielding atomicity: `$yield` 709 === Yielding atomicity: `$yield` #yield 710 710 711 711 {{{ … … 723 723 In particular, if the lock is available and there is a process at a `$local_start()` call (and the first statement following the call is enabled), one such a process is guaranteed to obtain the lock. 724 724 725 == Macros 726 727 === Elaboration of integer value: `$elaborate` 728 729 == Contract Annotations 725 == Macros #macros 726 727 === Elaboration of integer value: `$elaborate` #elaborate 728 729 == Contract Annotations #contracts 730 730 731 731 clauses 732 732 733 === The `depends_on` clause 733 === The `depends_on` clause #depends_on 734 734 735 735 `\nothing` 736 736 737 === The `executes_when` clause 737 === The `executes_when` clause #executes_when
