3

首先，我希望这个问题不要太开放。作为用于编码标准/策略、库/API 比较等的成分。我希望为形容词“库安全”建立一个正式的或至少半正式的定义。为了不将我自己的观点或其他任意观点强加于最佳实践作为定义的一部分，我想避免过于严格的定义。作为我的意思的一个例子，将任何访问静态存储持续时间的非 const 限定对象或更改其他进程全局状态（例如信号处置）的代码视为库不安全的可能是一个工作定义，但是它比它需要的要严格得多。

我希望捕获的基本属性是：

  1. 能够在同一进程中拥有库代码的多个“用户”，无论这意味着使用库代码的同一代码的多个实例（递归或线程），还是使用库代码完全分离程序的部分，没有这些用户踩着对方的脚趾。

  2. 不修改“属于”调用者的状态，除非接口合同中记录。

我认为对这个问题有好处的答案类型是参考过去类似的定义这个概念的尝试，将定义放在一起的强烈想法，或者令人信服的论点，即试图精确定义这个概念是徒劳的。

顺便说一句，我标记了这个 C、C++ 和 POSIX，因为这些是我最感兴趣的应用这种定义的上下文。在其他语言的上下文中它可能不那么有趣；例如，在一种非常纯粹的函数式语言中，所有代码可能都应该被认为是“库安全的”。

建议的定义：

如果存在程序 A 和 B，则库 L 是库不安全的：

  • A 和 B 不接受任何输入。
  • A 和 B 除了退出状态外不产生任何输出。
  • A 和 B 不会调用未定义的行为。
  • A 和 B 不包含 L 之外的任何更改全局状态的代码。
  • 将 A 和 B 组合到一个程序中，必要时重命名 L 之外的函数或对象以避免冲突，这样 A 和 B 的主要函数都在各自的线程中运行，导致程序调用未定义的行为或输出不同从分别运行 A 和 B 的输出。
4

2 回答 2

1

我同意您不访问非常量合格全局状态的标准可能过于严格。特别是，对库中的 C 代码进行修改errno以让更高级别的代码知道发生故障的原因可能是完全合理的。

许多要求（无论如何我都会看到）可能更多地适用于文档而不是代码本身。修改errno很好，但肯定需要记录在案。

对于 C++ 代码，异常安全性有些相似。显然，您希望大多数代码能够（合理地）提供最强的异常安全性，但是所提供的确切级别远不如提供的文档重要。

于 2013-04-28T04:58:08.017 回答
0

ACSL是 C 函数的规范语言。它遵循按合同设计的理念。但是，它不打算编译为运行时断言，这是在其他受合同设计启发的框架中使用前置条件和后置条件的最常用方式。

这似乎是一个题外话的答案，因为如果我理解正确，您要问的是关于正确库函数做什么的共同概念，而 ACSL 用于指定单个函数的作用。但我确实认为两者必须一起去。“适当的库函数”的唯一定义是“按照它所说的做的函数”。任何不那么通用的东西都会过于严格。例如，一个适当的库函数通常不应该取消分配内存……除非它free()被指定为或被指定为取消分配内存。

因此，至少，查看 ACSL 的预期以及某些 ACSL 子句的默认值可以建议适当的库函数应具有的属性，除非另有说明：

  • ACSL 契约在前置条件中描述了函数的期望，在后置条件中描述了它提供的保证。
  • ACSL 契约意味着函数对于满足前提条件的所有输入都终止，尽管可以另外指定。函数不终止的两种方法是永远循环或导致程序退出。
  • 除非在前置条件中另有说明，否则传递给函数的内存位置可以使用别名。
  • ACSL 合约描述了函数可能修改的所有内存位置。任何未列出的内存位置都不能通过调用该函数来修改。
  • 可选地，它描述了为计算每个输出而读取的内存位置。对放置在内存中的函数的两次调用表明仅在此读取内存位置列表之外的不同之处会更改相同的内存位置并将它们设置为相同的值。
  • 在函数调用期间动态分配或释放的内存块列在特定的 ACSL 子句中。默认情况下，函数既不分配也不释放内存。

一些副作用，例如更改 FPU 舍入模式，并未在 ACSL 中建模，但可以视为更改全局变量。其他副作用（创建线程、安装信号处理程序）是指 C 语言中超出 ACSL 范围的方面。

ACSL 合约示例：

/*@ requires \valid(((char*)s)+(0..n - 1));
  @ assigns ((char*)s)[0..n - 1] \from c;
  @ assigns \result \from s;
  @ ensures \forall integer i; (0 <= i < n) ==> ((char*)s)[i] == (char) c;
  @ ensures \result == s;
  @*/
void *memset(void *s, int c, size_t n);

作为关于 ACSL 的实际使用和库的实际非正式规范的最后一点，C 语言在封装和规范之间存在折衷。特别是，如果一个库函数修改了一个static变量，这个变量不能从规范中省略，尽管它超出了调用者的范围。

诸如random()不赋值的函数\result \from \nothing，因为这意味着两个连续的调用总是返回相同的结果。另一方面，double sin(double x);可以通过子句描述函数，因为只要参数相同assigns \result \from x;，两次调用就会sin()返回相同的结果（尽管有 FPU 舍入模式。如果将 FPU 舍入模式建模为全局变量，它将是此函数的输入。）

于 2013-04-28T07:22:40.183 回答